refactor(Studies/Faller2019): build on generalized table substrate

Linglib.lean

@@ -1294,6 +1294,7 @@ import Linglib.Studies.Ostrove2026
 import Linglib.Studies.Allotey2021
 import Linglib.Fragments.Tigrinya.ClausePrefixes
 import Linglib.Studies.FaginHalpern1994
+import Linglib.Studies.Faller2019
 import Linglib.Studies.FillmoreKayOConnor1988
 import Linglib.Studies.GoldbergShirtz2025
 import Linglib.Studies.KayFillmore1999
@@ -2041,7 +2042,6 @@ import Linglib.Discourse.Centering.Instances.InformationStatus
 -- Theories: Discourse — SDRT
 import Linglib.Discourse.Rhetorical.Defs
 import Linglib.Discourse.Rhetorical.RightFrontier
--- Theories: Discourse — Faller/Murray illocutionary operators
 -- Theories: Interfaces — Centering ↔ DRT bridge
 import Linglib.Discourse.Centering.DRSExpr
 -- Theories: Dynamic Semantics

Linglib/Discourse/Commitment/Table.lean

@@ -12,7 +12,8 @@ commitment slates, and a common ground.
 ## Main definitions
 
 * `Item A W` — speaker, addressee, mood, alternatives.
-* `DiscourseState A W` — ⟨table, dc, cg⟩.
+* `DiscourseState A W I` — ⟨table, dc, cg⟩, polymorphic in the
+  table-element type `I` (full model: `I := Item A W`).
 * `DiscourseState.IsStable` — empty-table predicate.
 * `pushItem`, `popItem`, `addCommit`, `addToCG` — primitive updates.
 
@@ -40,104 +41,108 @@ structure Item (A W : Type*) where
       polar question, the answer set for wh-questions. -/
   alternatives : List (W → Prop)
 
-/-- The discourse structure (DS) of @cite{farkas-bruce-2010}. -/
-structure DiscourseState (A W : Type*) where
+/-- The discourse structure (DS) of @cite{farkas-bruce-2010}, polymorphic
+    in the table-element type `I` (full model: `I := Item A W`). -/
+structure DiscourseState (A W I : Type*) where
   /-- Stack of unresolved items, head = most recent. -/
-  table : List (Item A W)
+  table : List I
   /-- Per-agent discourse commitments. -/
   dc : A → TaggedSlate W
   /-- The common ground. -/
   cg : CG W
 
 namespace DiscourseState
-variable {A W : Type*}
+variable {A W I : Type*}
 
 /-- Initial state: empty table, empty commitments, trivial CG. -/
-def empty : DiscourseState A W :=
+def empty : DiscourseState A W I :=
   ⟨[], fun _ => TaggedSlate.empty, CG.empty⟩
 
-instance : Inhabited (DiscourseState A W) := ⟨empty⟩
+instance : Inhabited (DiscourseState A W I) := ⟨empty⟩
 
 /-- The state is stable when the table is empty. -/
-def IsStable (s : DiscourseState A W) : Prop := s.table.isEmpty = true
+def IsStable (s : DiscourseState A W I) : Prop := s.table.isEmpty = true
 
-instance (s : DiscourseState A W) : Decidable s.IsStable :=
+instance (s : DiscourseState A W I) : Decidable s.IsStable :=
   inferInstanceAs (Decidable (_ = _))
 
 /-- Worlds compatible with the common ground. -/
-def contextSet (s : DiscourseState A W) : Set W := s.cg.contextSet
+def contextSet (s : DiscourseState A W I) : Set W := s.cg.contextSet
 
 /-! ### Primitive updates -/
 
-def pushItem (s : DiscourseState A W) (i : Item A W) : DiscourseState A W :=
+def pushItem (s : DiscourseState A W I) (i : I) : DiscourseState A W I :=
   { s with table := i :: s.table }
 
-def popItem (s : DiscourseState A W) : DiscourseState A W :=
+def popItem (s : DiscourseState A W I) : DiscourseState A W I :=
   { s with table := s.table.tail }
 
-def addToCG (s : DiscourseState A W) (p : W → Prop) : DiscourseState A W :=
+def addToCG (s : DiscourseState A W I) (p : W → Prop) : DiscourseState A W I :=
   { s with cg := s.cg.add p }
 
 /-- Add `(p, src, force)` to agent `a`'s slate. Defaults: self-generated,
     doxastic — the standard assertion-driven cell. -/
-def addCommit [DecidableEq A] (s : DiscourseState A W) (a : A)
+def addCommit [DecidableEq A] (s : DiscourseState A W I) (a : A)
     (p : W → Prop)
     (src : CommitmentSource := .selfGenerated)
-    (force : CommitmentForce := .doxastic) : DiscourseState A W :=
+    (force : CommitmentForce := .doxastic) : DiscourseState A W I :=
   { s with dc := Function.update s.dc a ((s.dc a).add p src force) }
 
 /-! ### Basic theorems -/
 
-@[simp] theorem empty_table : (empty : DiscourseState A W).table = [] := rfl
+@[simp] theorem empty_table : (empty : DiscourseState A W I).table = [] := rfl
 @[simp] theorem empty_dc (a : A) :
-    (empty : DiscourseState A W).dc a = TaggedSlate.empty := rfl
-@[simp] theorem empty_cg : (empty : DiscourseState A W).cg = CG.empty := rfl
-@[simp] theorem empty_isStable : (empty : DiscourseState A W).IsStable := rfl
+    (empty : DiscourseState A W I).dc a = TaggedSlate.empty := rfl
+@[simp] theorem empty_cg : (empty : DiscourseState A W I).cg = CG.empty := rfl
+@[simp] theorem empty_isStable : (empty : DiscourseState A W I).IsStable := rfl
 
-@[simp] theorem pushItem_table (s : DiscourseState A W) (i : Item A W) :
+@[simp] theorem pushItem_table (s : DiscourseState A W I) (i : I) :
     (s.pushItem i).table = i :: s.table := rfl
-@[simp] theorem pushItem_dc (s : DiscourseState A W) (i : Item A W) :
+@[simp] theorem pushItem_dc (s : DiscourseState A W I) (i : I) :
     (s.pushItem i).dc = s.dc := rfl
-@[simp] theorem pushItem_cg (s : DiscourseState A W) (i : Item A W) :
+@[simp] theorem pushItem_cg (s : DiscourseState A W I) (i : I) :
     (s.pushItem i).cg = s.cg := rfl
 
-@[simp] theorem popItem_table (s : DiscourseState A W) :
+@[simp] theorem popItem_table (s : DiscourseState A W I) :
     s.popItem.table = s.table.tail := rfl
-@[simp] theorem popItem_dc (s : DiscourseState A W) : s.popItem.dc = s.dc := rfl
-@[simp] theorem popItem_cg (s : DiscourseState A W) : s.popItem.cg = s.cg := rfl
+@[simp] theorem popItem_dc (s : DiscourseState A W I) : s.popItem.dc = s.dc := rfl
+@[simp] theorem popItem_cg (s : DiscourseState A W I) : s.popItem.cg = s.cg := rfl
 
-@[simp] theorem addToCG_cg (s : DiscourseState A W) (p : W → Prop) :
+@[simp] theorem addToCG_cg (s : DiscourseState A W I) (p : W → Prop) :
     (s.addToCG p).cg = s.cg.add p := rfl
-@[simp] theorem addToCG_table (s : DiscourseState A W) (p : W → Prop) :
+@[simp] theorem addToCG_table (s : DiscourseState A W I) (p : W → Prop) :
     (s.addToCG p).table = s.table := rfl
-@[simp] theorem addToCG_dc (s : DiscourseState A W) (p : W → Prop) :
+@[simp] theorem addToCG_dc (s : DiscourseState A W I) (p : W → Prop) :
     (s.addToCG p).dc = s.dc := rfl
 
-@[simp] theorem addCommit_table [DecidableEq A] (s : DiscourseState A W)
+@[simp] theorem addCommit_table [DecidableEq A] (s : DiscourseState A W I)
     (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) :
     (s.addCommit a p src force).table = s.table := rfl
-@[simp] theorem addCommit_cg [DecidableEq A] (s : DiscourseState A W)
+@[simp] theorem addCommit_cg [DecidableEq A] (s : DiscourseState A W I)
     (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) :
     (s.addCommit a p src force).cg = s.cg := rfl
 
-@[simp] theorem addCommit_dc_self [DecidableEq A] (s : DiscourseState A W)
+@[simp] theorem addCommit_dc_self [DecidableEq A] (s : DiscourseState A W I)
     (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) :
     (s.addCommit a p src force).dc a = (s.dc a).add p src force := by
   simp [addCommit]
 
-@[simp] theorem addCommit_dc_of_ne [DecidableEq A] (s : DiscourseState A W)
+@[simp] theorem addCommit_dc_of_ne [DecidableEq A] (s : DiscourseState A W I)
     {a b : A} (h : b ≠ a) (p : W → Prop)
     (src : CommitmentSource) (force : CommitmentForce) :
     (s.addCommit a p src force).dc b = s.dc b := by
   simp [addCommit, Function.update_of_ne h]
 
-theorem pushItem_not_isStable (s : DiscourseState A W) (i : Item A W) :
+theorem pushItem_not_isStable (s : DiscourseState A W I) (i : I) :
     ¬ (s.pushItem i).IsStable := by
   simp [IsStable]
 
 end DiscourseState
 
-instance {A W : Type*} : HasContextSet (DiscourseState A W) W where
+instance {A W I : Type*} : HasContextSet (DiscourseState A W I) W where
   toContextSet := DiscourseState.contextSet
 
+/-- The full Farkas-Bruce model: the table holds rich speech-act `Item`s. -/
+abbrev ItemState (A W : Type*) := DiscourseState A W (Item A W)
+
 end Discourse.Commitment.Table