LanglibExact scheduler moves #
Invariant-ready constructors for each composite machine transition and stack-layout boundary.
Exact composite-move constructors #
theorem
IndexedGrammar.Aho.composite_plainPushUse_at
{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.live B,
right := WorkSym.index (cflagBase g f) IndexMark.firstPending :: beta } }
Starting the first relevant stack block.
theorem
IndexedGrammar.Aho.composite_liveBinaryBoth_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
{A B C : g.nt}
(hbinary : AugBinary g A B C)
(inputPos : ℕ)
(alpha : List (WorkSym g))
(Z : WorkSym g)
(beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := Z :: beta } }
{ inputPos := inputPos,
work :=
{ left := markProductivePrefix alpha ++ [WorkSym.dollar], focus := WorkSym.live B,
right := WorkSym.live C :: Z :: beta } }
A live binary task whose two children both consume the represented stack.
theorem
IndexedGrammar.Aho.composite_liveBinaryLeft_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
{A B C : g.nt}
(hbinary : AugBinary g A B C)
(inputPos : ℕ)
(alpha : List (WorkSym g))
(Z : WorkSym g)
(beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := Z :: beta } }
{ inputPos := inputPos,
work :=
{ left := markProductivePrefix alpha ++ [WorkSym.dollar], focus := WorkSym.live B,
right := WorkSym.plain C :: Z :: beta } }
A live binary task whose left child alone consumes the represented stack.
theorem
IndexedGrammar.Aho.composite_liveBinaryRight_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
{A B C : g.nt}
(hbinary : AugBinary g A B C)
(inputPos : ℕ)
(alpha : List (WorkSym g))
(Z : WorkSym g)
(beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := Z :: beta } }
{ inputPos := inputPos,
work :=
{ left := markProductivePrefix alpha ++ [WorkSym.dollar], focus := WorkSym.plain B,
right := WorkSym.live C :: Z :: beta } }
A live binary task whose right child alone consumes the represented stack.
theorem
IndexedGrammar.Aho.composite_livePushFresh_at
{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 : List (WorkSym g))
(Z : WorkSym g)
(beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := Z :: beta } }
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar], focus := WorkSym.live B,
right := WorkSym.index (cflagBase g f) IndexMark.laterPending :: Z :: beta } }
Introduce a fresh relevant flag block above an already-live continuation.
theorem
IndexedGrammar.Aho.composite_livePushCompress_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
{A B : g.nt}
{f : g.flag}
(R : CFlag g)
(d : IndexMark)
(hpush : AugPush g A B f)
(hne : (cflagComp g (cflagBase g f) R).Nonempty)
(inputPos : ℕ)
(alpha beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos,
work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := WorkSym.index R d :: beta } }
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar], focus := WorkSym.live B,
right := WorkSym.index (cflagComp g (cflagBase g f) R) d :: beta } }
Compress a new pushed flag into the adjacent represented block.
theorem
IndexedGrammar.Aho.composite_popPlain_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(R : CFlag g)
(d : IndexMark)
{A B : g.nt}
(hedge : R A B = true)
(inputPos : ℕ)
(alpha beta gamma : List (WorkSym g))
(hfree : IndexFree beta)
:
CompositeStep g input
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } }
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar],
focus := WorkSym.plain B, right := WorkSym.close :: gamma } }
Consume a represented block and continue with a plain task in a fresh frame.
theorem
IndexedGrammar.Aho.composite_popLive_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(R : CFlag g)
(d : IndexMark)
{A B : g.nt}
(hedge : R A B = true)
(hlater : d.later = true)
(inputPos : ℕ)
(alpha beta gamma : List (WorkSym g))
(hfree : IndexFree beta)
:
CompositeStep g input
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } }
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar],
focus := WorkSym.live B, right := WorkSym.close :: gamma } }
Consume a represented block and continue with a live task in a fresh frame.
theorem
IndexedGrammar.Aho.composite_popPlainErase_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(R : CFlag g)
(d : IndexMark)
{A B : g.nt}
(hedge : R A B = true)
(inputPos : ℕ)
(alpha gamma : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos,
work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := WorkSym.index R d :: gamma } }
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain B, right := gamma } }
Consume an adjacent compressed block and discard its token before entering a plain residual task. The adjacency is what makes deletion ownership-safe: no pending sibling lies between the active task and the selected block.
theorem
IndexedGrammar.Aho.composite_popLiveErase_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(R : CFlag g)
(d : IndexMark)
{A B : g.nt}
(hedge : R A B = true)
(hlater : d.later = true)
(inputPos : ℕ)
(alpha gamma : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos,
work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := WorkSym.index R d :: gamma } }
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live B, right := gamma } }
Unframed adjacent pop whose residual task still consumes a represented suffix.
theorem
IndexedGrammar.Aho.composite_eraseIndex_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(R : CFlag g)
(d : IndexMark)
(herase : d.erasable = true)
(inputPos : ℕ)
(alpha : List (WorkSym g))
(Z : WorkSym g)
(beta : List (WorkSym g))
:
CompositeStep g input
{ inputPos := inputPos,
work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.index R d, right := Z :: beta } }
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta } }
Remove an erasable represented block and expose its continuation.
theorem
IndexedGrammar.Aho.composite_returnFrame_at
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
(input : List T)
(inputPos : ℕ)
(alpha : List (WorkSym g))
(Z : WorkSym g)
(beta gamma : List (WorkSym g))
(hZ : Z ≠ WorkSym.dollar)
(hfree : DollarFree beta)
:
CompositeStep g input
{ inputPos := inputPos,
work :=
{ left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } }
{ inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } }
Close a completed pop frame and reactivate its saved continuation.
Singleton visible-stack layouts #
The first, unbounded, completeness runner uses one compressed token for every inherited flag
which is actually consumed. Compression is only needed later for the linear accounting. A
layout records the index-free (but possibly close-containing) gaps between those singleton
tokens. The additional dollar-free fact is exactly what is needed when a completed pop frame
returns through such a gap.
theorem
IndexedGrammar.Aho.IndexFree.append
{T : Type}
{g : IndexedGrammar T}
{xs ys : List (WorkSym g)}
(hxs : IndexFree xs)
(hys : IndexFree ys)
:
theorem
IndexedGrammar.Aho.DollarFree.append
{T : Type}
{g : IndexedGrammar T}
{xs ys : List (WorkSym g)}
(hxs : DollarFree xs)
(hys : DollarFree ys)
:
DollarFree (xs ++ ys)
- nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (tail : List (WorkSym g)) : SingletonLayout g [] tail tail
- cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {f : g.flag} {flags : List g.flag} {beta tail tail' : List (WorkSym g)} {d : IndexMark} (indexFree : IndexFree beta) (dollarFree : DollarFree beta) (later : flags ≠ [] → d.later = true) (rest : SingletonLayout g flags tail tail') : SingletonLayout g (f :: flags) (beta ++ WorkSym.index (cflagBase g f) d :: tail) (beta ++ WorkSym.index (cflagBase g f) d.markUsed :: tail')
Instances For
theorem
IndexedGrammar.Aho.SingletonLayout.idempotent
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{flags : List g.flag}
{word used : List (WorkSym g)}
(layout : SingletonLayout g flags word used)
:
SingletonLayout g flags used used
Once all selected tokens have been used, selecting them again leaves the physical word unchanged.
theorem
IndexedGrammar.Aho.SingletonLayout.prepend
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{flags : List g.flag}
{word used : List (WorkSym g)}
(pref : List (WorkSym g))
(hindex : IndexFree pref)
(hdollar : DollarFree pref)
(layout : SingletonLayout g flags word used)
:
SingletonLayout g flags (pref ++ word) (pref ++ used)
Ordinary control symbols may be inserted before the first selected token. In particular,
this is how a pending binary sibling or a crossed close is included in a pop gap.
theorem
IndexedGrammar.Aho.SingletonLayout.splitTake
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{flags : List g.flag}
{word used : List (WorkSym g)}
(n : ℕ)
(layout : SingletonLayout g flags word used)
:
∃ (middle : List (WorkSym g)), SingletonLayout g (List.take n flags) word middle ∧ SingletonLayout g flags middle used
Restrict a layout to its first n selected flags. The remaining physical tokens become
part of the arbitrary unselected tail.
theorem
IndexedGrammar.Aho.SingletonLayout.splitAll
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{flags : List g.flag}
{word used : List (WorkSym g)}
(layout : SingletonLayout g flags word used)
:
Selecting the whole visible prefix reaches the all-used endpoint and leaves an idempotent layout there.
theorem
IndexedGrammar.Aho.SingletonLayout.idempotentTake
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{flags : List g.flag}
{word used : List (WorkSym g)}
(n : ℕ)
(layout : SingletonLayout g flags word used)
:
SingletonLayout g (List.take n flags) used used
Any prefix of an all-used layout is itself an identity layout. This is used when one binary child has already consumed the whole visible prefix and the other child consumes only part.
Maximal consumed prefixes #
theorem
IndexedGrammar.Aho.NFParse.exists_consumedPrefix
{T : Type}
{g : IndexedGrammar T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(p : g.NFParse A stack w)
(n : ℕ)
(hboundary : ¬p.ConsumesAt n)
:
∃ m ≤ n, (∀ k < m, p.ConsumesAt k) ∧ ¬p.ConsumesAt m
Before a known unused boundary, consumption consists of an initial segment.