Documentation

Linglib.Syntax.Case.Spatial

Spatial cases #

A spatial case combines a localization with a direction, as Pantcheva decomposes them: the interior, surface and exterior series of Finnish, Hungarian and Daghestanian local cases each cross a localization with Place, Goal and Source. The general locative, allative, ablative and perlative express a direction with no localization. Blake's types of case (Table 2.7) place the spatial cases among the semantic cases, apart from the grammatical ones.

Main definitions #

Main results #

Implementation notes #

Blake names the nominative, accusative, ergative, genitive and dative as grammatical cases; Case.kind adds the absolutive, the oblique, the partitive and the vocative to them. The terminative is a delimited goal, Pantcheva's up to.

References #

source
def Case.dirOf :
Case → Option Spatial.Path.Direction

The direction a spatial case expresses, if any, determinable even where the localization is not (localizationOf).

Equations
Instances For
    source
    def Case.shape? :
    Case → Option Spatial.Path.Shape

    The shape of the paths a directional case expresses. The illative, allative and sublative are cofinal, the elative, ablative and delative coinitial, the perlative transitive, and the terminative terminative.

    Equations
    Instances For
      source
      theorem Case.dirOf_eq_of_shape?_eq {c : Case} {s : Spatial.Path.Shape} (h : c.shape? = some s) :
      c.dirOf = some s.direction

      A directional case's shape has the case's direction.

      source
      def Case.toCase :
      Spatial.Localization → Spatial.Path.Direction → Option Case

      Build a spatial case from its Localization × Direction decomposition — the constructor direction spatial-case fragments consume. The 3 × 3 localization-specific cells; route is localization-neutral in these inventories (none).

      Equations
      Instances For
        source
        def Case.localizationOf :
        Case → Option Spatial.Localization

        The localization a case expresses, under the spatial reading. The exterior series is ade, all and abl, Finnish's external local cases; all and abl also serve as the general allative and ablative, with no localization, a use this decomposition does not separate. The general locative loc has no localization.

        Equations
        Instances For
          source
          def Case.spatialDecomp (c : Case) :
          Option (Spatial.Localization × Spatial.Path.Direction)

          Analyze a spatial case into Localization × Direction, where both are determinable (lossy on localization-conflated cells; the faithful inverse of toCase on the 3 × 3 localization-specific cells).

          Equations
          Instances For
            source
            theorem Case.spatialDecomp_toCase (r : Spatial.Localization) (d : Spatial.Path.Direction) :
            (toCase r d).bind spatialDecomp = Option.map (fun (x : Case) => (r, d)) (toCase r d)

            toCase and spatialDecomp are inverse on the localization-specific cells — the decomposition round-trips where localization is not conflated. (route is localization-neutral, hence none on both sides.)

            source
            def Case.ofDir :
            Spatial.Path.Direction → Case

            ofDir d is the case that expresses d with no localization, the general locative, allative, ablative or perlative.

            Equations
            Instances For
              source
              @[simp]
              theorem Case.dirOf_ofDir (d : Spatial.Path.Direction) :
              (ofDir d).dirOf = some d
              source
              theorem Case.ofDir_injective :
              Function.Injective ofDir

              Types of case #

              source
              inductive Case.Kind :
              Type

              A case is grammatical, encoding a syntactic relation, or semantic, and a semantic case is spatial when it encodes location, source, destination or path.

              • grammatical : Kind

                A grammatical case is a core case, the genitive or the dative.

              • spatial : Kind

                A spatial case encodes location, source, destination or path, alone or with another notion.

              • semantic : Kind

                A semantic case that is not spatial, such as the instrumental and the comitative.

              Instances For
                source
                @[instance_reducible]
                instance Case.instDecidableEqKind :
                DecidableEq Kind
                Equations
                source
                def Case.instReprKind.repr :
                Kind → ℕ → Std.Format
                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance Case.instReprKind :
                  Repr Kind
                  Equations
                  source
                  @[instance_reducible]
                  instance Case.instFintypeKind :
                  Fintype Kind
                  Equations
                  source
                  def Case.kind :
                  Case → Kind

                  The type of a case value.

                  Equations
                  Instances For
                    source
                    theorem Case.kind_eq_spatial_iff (c : Case) :
                    c.kind = Kind.spatial ↔ c.dirOf.isSome = true