refactor(Core/UD): unify Word features into UD.MorphFeatures

Linglib.lean

@@ -8,7 +8,7 @@ and their interfaces. See README.md for documentation links.
 import Linglib.Features.Dimension
 import Linglib.Features.Gender
 import Linglib.Core.Valence
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Typology.NegativeConcord
 import Linglib.Typology.PolarityItem
 import Linglib.Typology.Negation
@@ -38,7 +38,7 @@ import Linglib.Core.Logic.Team.Closure
 import Linglib.Core.Logic.Team.Definability
 import Linglib.Features.Acceptability
 import Linglib.Semantics.Dynamic.ParameterizedUpdate
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Core.Tree
 import Linglib.Features.Coordination
 import Linglib.Core.Logic.Duality

Linglib/Core/Tree.lean

@@ -1,6 +1,6 @@
 import Mathlib.Data.List.Infix
 import Mathlib.Algebra.Free
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Core.Order.Tree
 
 /-!

Linglib/Core/UD.lean → Linglib/Core/UD/Basic.lean

@@ -326,6 +326,10 @@ structure MorphFeatures where
   definite : Option Definite := none
   degree   : Option Degree   := none
   pronType : Option PronType := none
+  /-- Reflexive (UD `Reflex=Yes`); `false` = feature absent. Distinguishes a reflexive
+      anaphor from a plain personal pronoun; not an agreement feature, so not consulted
+      by `compatible`. -/
+  reflex   : Bool            := false
   person   : Option Person   := none
   verbForm : Option VerbForm := none
   tense    : Option Tense    := none
@@ -338,6 +342,11 @@ structure MorphFeatures where
 /-- Empty feature bundle -/
 def MorphFeatures.empty : MorphFeatures := {}
 
+/-- Is this bundle wh-marked — an interrogative or relative pro-form? Derived from
+    `pronType` (UD has no standalone wh feature; wh-ness *is* `PronType ∈ {Int, Rel}`). -/
+def MorphFeatures.isWh (f : MorphFeatures) : Bool :=
+  f.pronType == some .Int || f.pronType == some .Rel
+
 /-- Check if two feature bundles are compatible (unify where both specified) -/
 def MorphFeatures.compatible (f1 f2 : MorphFeatures) : Bool :=
   (f1.number.isNone   || f2.number.isNone   || f1.number == f2.number) &&
@@ -363,6 +372,7 @@ def MorphFeatures.unify (f1 f2 : MorphFeatures) : Option MorphFeatures :=
       definite := f1.definite <|> f2.definite
       degree   := f1.degree   <|> f2.degree
       pronType := f1.pronType <|> f2.pronType
+      reflex   := f1.reflex   || f2.reflex
       person   := f1.person   <|> f2.person
       verbForm := f1.verbForm <|> f2.verbForm
       tense    := f1.tense    <|> f2.tense

Linglib/Core/Word.lean → Linglib/Core/UD/Word.lean

@@ -1,12 +1,13 @@
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Core.Valence
 
 /-!
 # Word
 [biberauer-roberts-2014] [dryer-1992]
 
 The lexical unit and its building blocks: morphological feature types (aliased
-to Universal Dependencies), the `Features` bundle, and the `Word` structure.
+to Universal Dependencies) and the `Word` structure. A word's morphology is one
+`UD.MorphFeatures` bundle — there is no separate word-level feature record.
 
 ## Provenance
 
@@ -117,41 +118,32 @@ inductive HeadDirection where
   deriving Repr, DecidableEq
 
 -- ============================================================================
--- Feature Bundle and Word
+-- Word
 -- ============================================================================
 
-/-- Feature bundle for words. Uses aliased UD types. -/
-structure Features where
-  wh : Bool := false
-  finite : Bool := true
-  number : Option Number := none
-  person : Option Person := none
-  case_ : Option UD.Case := none
-  /-- Grammatical gender (UD.Gender). Carried on the word so φ-agreement is
-      feature-based, not recovered from surface form. -/
-  gender : Option UD.Gender := none
-  valence : Option Valence := none
-  voice : Option Voice := none
-  vform : Option VForm := none
-  tense : Option Tense := none
-  countable : Option MassCount := none  -- for count vs mass nouns
-  /-- Pronoun type (UD `PronType`: personal, reciprocal, interrogative, …). Carried
-      so a pro-form's binding class is read off its own morphology, not its surface form. -/
-  pronType : Option UD.PronType := none
-  /-- Reflexive morphology (UD `Reflex=Yes`). The one binding-relevant feature `PronType`
-      does not encode; distinguishes a reflexive anaphor from a plain personal pronoun. -/
-  reflex : Bool := false
-  deriving Repr, DecidableEq
+/-- A word: the surface-token interface between the lexicon and token-level engines —
+    surface form, UD category, and UD morphology (one `UD.MorphFeatures` bundle; there is no
+    separate word-level feature record), plus lexical valence, the one non-morphological
+    property a Fragment-free engine reads off the token (DG subcategorization).
 
-/-- A word: form + category + features. -/
+    **Admission rule**: a property belongs on `Word` iff a Fragment-free token-level engine
+    reads it; otherwise it lives on the typed lexical carrier (`Pronoun`, `NounEntry`, …) and
+    is consumed via the capability mixins. Identity caveat: `BEq` is form + category, so
+    homographs collapse; a CoNLL-U `lemma` field is the known fix, deferred until a consumer
+    needs it. -/
 structure Word where
   form : String
   cat : UD.UPOS
-  features : Features := {}
+  features : UD.MorphFeatures := {}
+  /-- Lexical valence (subcategorization frame) — lexical, not UD morphology; read by the
+      DG engine off the token. TODO: migrate off `Word` by having the DG engine consume
+      subcategorization from the lexical carrier via a capability mixin (as binding did for
+      `bindingClass`), leaving `Word` the pure CoNLL-U token. -/
+  valence : Option Valence := none
   deriving Repr
 
 /-- Convenience constructor for a featureless word (form + category only). -/
-def Word.mk' (form : String) (cat : UD.UPOS) : Word := ⟨form, cat, {}⟩
+def Word.mk' (form : String) (cat : UD.UPOS) : Word := { form := form, cat := cat }
 
 /-- The φ-feature subset (person, number, gender) of a word, as a
     `UD.MorphFeatures` bundle. -/
@@ -176,8 +168,8 @@ instance (w1 w2 : Word) : Decidable (Word.Agree w1 w2) := by
 /-- Derive a passive variant: sets voice to passive, valence to intransitive.
     Used to compose with `VerbEntry.toWordPastPart` for passive constructions. -/
 def Word.asPassive (w : Word) : Word :=
-  { w with features := { w.features with
-      valence := some .intransitive, voice := some Voice.passive } }
+  { w with valence := some .intransitive,
+           features := { w.features with voice := some Voice.passive } }
 
 instance : BEq Word where
   beq w1 w2 := w1.form == w2.form && w1.cat == w2.cat

Linglib/Features/Case.lean

@@ -1,7 +1,7 @@
 import Mathlib.Data.Finset.Card
 import Mathlib.Order.Lattice
 import Mathlib.Tactic.DeriveFintype
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 
 /-!
 # Case — Feature Taxonomy

Linglib/Features/Gender.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Features.PrivativePair
 
 /-!

Linglib/Features/Number.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Features.PrivativePair
 
 /-!

Linglib/Features/OntologicalCategory.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Features.Prominence
 
 /-!

Linglib/Features/Person.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD
+import Linglib.Core.UD.Basic
 import Linglib.Features.Prominence
 import Linglib.Features.PrivativePair
 

Linglib/Fragments/Chichewa/Reciprocals.lean

@@ -23,7 +23,8 @@ def reciprocalAffix : MorphRule Bool :=
   { category := .valence
   , value := "reciprocal"
   , formRule := fun stem => stem ++ "an"
-  , featureRule := fun f => { f with valence := some .intransitive }
+  , featureRule := id
+  , valenceRule := fun _ => some .intransitive
   , semEffect := id
   }
 
@@ -32,7 +33,8 @@ def reflexivePrefix : MorphRule Bool :=
   { category := .valence
   , value := "reflexive"
   , formRule := fun stem => "dzi" ++ stem
-  , featureRule := fun f => { f with valence := some .intransitive }
+  , featureRule := id
+  , valenceRule := fun _ => some .intransitive
   , semEffect := id
   }
 

Linglib/Fragments/Dargwa/Agreement.lean

@@ -1,5 +1,5 @@
 import Linglib.Features.Prominence
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Features.Gender
 
 /-!

Linglib/Fragments/Dutch/Nouns.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Semantics.Kinds.NominalMappingParameter
 
 /-!

Linglib/Fragments/English/Auxiliaries.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Semantics.Modality.ModalTypes
 import Linglib.Features.Register
 
@@ -226,7 +226,7 @@ def AuxEntry.toWord (a : AuxEntry) : Word :=
   { form := a.form
   , cat := .AUX
   , features := {
-      finite := true
+      verbForm := some .Fin
       , person := a.person
       , number := a.number
     }

Linglib/Fragments/English/Complementizers.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 
 /-!
 # English Complementizers Lexicon Fragment

Linglib/Fragments/English/Determiners.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Semantics.Quantification.Lexicon
 
 /-!

Linglib/Fragments/English/FunctionWords.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 
 /-!
 # English Miscellaneous Function Words Fragment

Linglib/Fragments/English/Modifiers/Adjectives.lean

@@ -18,7 +18,7 @@ Both share scale type and antonym information, but serve different grammatical f
 
 -/
 
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Features.PropertyDomain
 import Linglib.Morphology.Exponence
 import Linglib.Morphology.DegreeContainment

Linglib/Fragments/English/Nouns.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Features.Gender
 import Linglib.Morphology.Exponence
 import Linglib.Semantics.Kinds.NominalMappingParameter
@@ -189,8 +189,7 @@ def NounEntry.toWordSg (n : NounEntry) : Word :=
   { form := n.formSg
   , cat := if n.proper then .PROPN else .NOUN
   , features := {
-      number := some .sg
-    , countable := if n.proper then none else some n.countable
+      number := some .Sing
     , person := if n.proper then some .third else none
     , gender := n.gender.bind (·.toUDGender)
     }
@@ -202,8 +201,7 @@ def NounEntry.toWordPl (n : NounEntry) : Word :=
   { form := (n.formPl.getD (n.formSg ++ "s"))
   , cat := .NOUN
   , features := {
-      number := some .pl
-    , countable := some n.countable
+      number := some .Plur
     }
   }
 
@@ -216,7 +214,6 @@ def NounEntry.toStem {α : Type} (n : NounEntry) : Morphology.Stem (α → Bool)
   { lemma_ := n.formSg
   , cat := if n.proper then .PROPN else .NOUN
   , baseFeatures := { number := some .Sing
-                    , countable := if n.proper then none else some n.countable
                     , person := if n.proper then some .third else none }
   , paradigm :=
       if n.countable == .count && !n.proper then

Linglib/Fragments/English/NumeralModifiers.lean

@@ -18,7 +18,7 @@ from "up to" (positive), predicting divergent framing effects.
 
 -/
 
-import Linglib.Core.Word
+import Linglib.Core.UD.Word
 import Linglib.Features.PropertyDomain
 import Linglib.Features.Valence
 import Linglib.Semantics.Numerals.Basic