Parse-directed scheduler execution

Ordinary parse execution and the unbounded semantic completeness theorem.

Ordinary parse-directed execution

def IndexedGrammar.Aho.wordConfig {T : Type} (g : IndexedGrammar T) (inputPos : ℕ) (alpha word : List (WorkSym g)) : Config g

Focus the first symbol of a nonempty continuation word. The empty fallback is convenient for total statements; every use in the live runner is proved nonempty by its layout.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.wordConfig g inputPos alpha (z :: zs) = { inputPos := inputPos, work := { left := alpha ++ [IndexedGrammar.Aho.WorkSym.dollar], focus := z, right := zs } }

def IndexedGrammar.Aho.StablePrefix {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) : Prop

Productive moves leave an already stable frame prefix unchanged. Initial and freshly opened pop frames are stable.

Equations

• IndexedGrammar.Aho.StablePrefix alpha = (IndexedGrammar.Aho.markProductivePrefix alpha = alpha)

@[simp]

theorem IndexedGrammar.Aho.stablePrefix_nil {T : Type} (g : IndexedGrammar T) : StablePrefix []

theorem IndexedGrammar.Aho.stablePrefix_append_usedIndex {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) (R : CFlag g) (d : IndexMark) : StablePrefix (alpha ++ [WorkSym.index R d.markUsed])

theorem IndexedGrammar.Aho.SingletonLayout.input_ne_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {word used : List (WorkSym g)} (layout : SingletonLayout g flags word used) (hne : flags ≠ []) : word ≠ []

theorem IndexedGrammar.Aho.SingletonLayout.output_ne_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {word used : List (WorkSym g)} (layout : SingletonLayout g flags word used) (hne : flags ≠ []) : used ≠ []

Stable-context constructors for the elementary moves

theorem IndexedGrammar.Aho.composite_plainBinary_stable {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {A B C : g.nt} (hbinary : AugBinary g A B C) (inputPos : ℕ) (alpha beta : List (WorkSym g)) (hstable : StablePrefix alpha) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain B, right := WorkSym.plain C :: beta } }

theorem IndexedGrammar.Aho.composite_plainTerminal_stable {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {A : g.nt} {a : T} (hterminal : AugTerminal g A a) (inputPos : ℕ) (alpha beta : List (WorkSym g)) (hstable : StablePrefix alpha) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.terminal a, right := beta } }

theorem IndexedGrammar.Aho.composite_plainPushSkip_stable {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {A B : g.nt} {f : g.flag} (hpush : AugPush g A B f) (inputPos : ℕ) (alpha beta : List (WorkSym g)) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain B, right := beta } }

theorem IndexedGrammar.Aho.composite_matchTerminal_at {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) (a : T) (inputPos : ℕ) (alpha : List (WorkSym g)) (Z : WorkSym g) (beta : List (WorkSym g)) (hinput : input[inputPos]? = some a) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.terminal a, right := Z :: beta } } { inputPos := inputPos + 1, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta } }

theorem IndexedGrammar.Aho.NFParse.singleton_runs {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) : (¬parse.ConsumesAt 0 → ∀ (pre post : List T) (alpha : List (WorkSym g)) (next : WorkSym g) (tail : List (WorkSym g)), StablePrefix alpha → Relation.ReflTransGen (CompositeStep g (pre ++ w ++ post)) { inputPos := pre.length, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := next :: tail } } (wordConfig g (pre ++ w).length alpha (next :: tail))) ∧ ∀ (visible hidden : List g.flag) (word used : List (WorkSym g)), stack = visible ++ hidden → visible ≠ [] → (∀ k < visible.length, parse.ConsumesAt k) → ¬parse.ConsumesAt visible.length → SingletonLayout g visible word used → ∀ (pre post : List T) (alpha : List (WorkSym g)), StablePrefix alpha → Relation.ReflTransGen (CompositeStep g (pre ++ w ++ post)) { inputPos := pre.length, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := word } } (wordConfig g (pre ++ w).length alpha used)

Mutual plain/live execution statement used by the singleton scheduler. A plain task uses none of its inherited stack. A live task uses exactly the nonempty prefix visible; its singleton layout may cross close markers but not another selected index or an open $. Every selected token is used at the endpoint.

theorem IndexedGrammar.Aho.complete_of_nfparse {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : Relation.ReflTransGen (CompositeStep g input) (initialConfig g) (finalConfig g input.length)

Every concrete normal-form parse has an ordinary accepting run of Aho's composite machine. This is the unconditional semantic completeness theorem; the later accounting refinement only strengthens the same construction with a uniform work bound.