structure DepGrammar.LexEntry : Type

A lexical entry: word form + category + features + argument structure. Uses the shared Features bundle from Core/Basic.lean. The inv field is DG-specific (auxiliary inversion state).

• form : String
• cat : UD.UPOS
• features : Features
• argStr : ArgStr
• inv : Bool

instance DepGrammar.instReprLexEntry : Repr LexEntry

Equations

• DepGrammar.instReprLexEntry = { reprPrec := DepGrammar.instReprLexEntry.repr }

def DepGrammar.instReprLexEntry.repr : LexEntry → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def DepGrammar.argStr_Aux : ArgStr

Auxiliary verb (non-inverted): subject left, main verb right

Equations

• One or more equations did not get rendered due to their size.

def DepGrammar.argStr_AuxInv : ArgStr

Auxiliary verb (inverted): subject right, main verb right

Equations

• One or more equations did not get rendered due to their size.

structure DepGrammar.LexRule : Type

A lexical rule transforms one lexical entry into another

• name : String
• applies : LexEntry → Bool

  Condition for the rule to apply

• transform : LexEntry → LexEntry

  Transform the entry

def DepGrammar.auxInversionRule : LexRule

Auxiliary Inversion Rule: V+aux,-inv → V+aux,+inv The subject moves from left to right position

Equations

• One or more equations did not get rendered due to their size.

def DepGrammar.passiveRule : LexRule

Passive Rule: VN → V+passive Object is removed (promoted to subject), by-phrase added as optional

Equations

• One or more equations did not get rendered due to their size.

def DepGrammar.applyRule (rule : LexRule) (entry : LexEntry) : Option LexEntry

Apply a lexical rule if it matches

Equations

• DepGrammar.applyRule rule entry = if rule.applies entry = true then some (rule.transform entry) else none

def DepGrammar.deriveEntries (rules : List LexRule) (entry : LexEntry) : List LexEntry

Apply all applicable rules to generate derived entries

Equations

• DepGrammar.deriveEntries rules entry = entry :: List.filterMap (fun (x : DepGrammar.LexRule) => DepGrammar.applyRule x entry) rules