LanglibTransporting canonical event boundaries through parse constructors #
These lemmas isolate the block-boundary bookkeeping used by the compressed runner. They do
not construct machine steps: they only transport EventCompatible across binary children and
the singleton/fused block layouts created by pop and push moves.
def
IndexedGrammar.Aho.EventCompatible.binaryLeft
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{blocks : List (List g.flag)}
(compatible : EventCompatible (NFParse.binary hr hlhs hc hrhs left right) blocks)
:
EventCompatible left blocks
A binary parent's compatible partition is compatible with its left child.
Equations
- compatible.binaryLeft = { boundary := fun (d : ℕ) (hd : d ∈ left.eventDepths) => compatible.boundary d ⋯ }
Instances For
def
IndexedGrammar.Aho.EventCompatible.binaryRight
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{blocks : List (List g.flag)}
(compatible : EventCompatible (NFParse.binary hr hlhs hc hrhs left right) blocks)
:
EventCompatible right blocks
A binary parent's compatible partition is compatible with its right child.
Equations
- compatible.binaryRight = { boundary := fun (d : ℕ) (hd : d ∈ right.eventDepths) => compatible.boundary d ⋯ }
Instances For
def
IndexedGrammar.Aho.EventCompatible.binary
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
{blocks : List (List g.flag)}
(leftCompatible : EventCompatible left blocks)
(rightCompatible : EventCompatible right blocks)
:
EventCompatible (NFParse.binary hr hlhs hc hrhs left right) blocks
Compatible binary children combine into a compatible parent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventCompatible.tailOfShift
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B : g.nt}
{parentStack residualStack : List g.flag}
{parentYield residualYield : List T}
{parent : g.NFParse A parentStack parentYield}
{residual : g.NFParse B residualStack residualYield}
{block : List g.flag}
{blocks : List (List g.flag)}
(hblock : block ≠ [])
(compatible : EventCompatible parent (block :: blocks))
(shift : ∀ d ∈ residual.eventDepths, block.length + d ∈ parent.eventDepths)
:
EventCompatible residual blocks
Generic whole-block pop transport. A caller only has to show that every residual event depth shifts upward by the concrete length of the removed first block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventCompatible.popTail
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
{blocks : List (List g.flag)}
(compatible : EventCompatible (NFParse.pop hr hlhs hc hrhs rest) ([f] :: blocks))
:
EventCompatible rest blocks
A structural pop removes its singleton first block and exposes a compatible residual parse.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventCompatible.popCons
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
{blocks : List (List g.flag)}
(compatible : EventCompatible rest blocks)
:
EventCompatible (NFParse.pop hr hlhs hc hrhs rest) ([f] :: blocks)
Conversely, prefixing the popped flag as a singleton block makes the pop parent compatible.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventCompatible.pushFresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
{blocks : List (List g.flag)}
(compatible : EventCompatible (NFParse.push hr hlhs hc hrhs rest) blocks)
:
EventCompatible rest ([f] :: blocks)
A fresh singleton block above the old partition is compatible with the pushed child.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventCompatible.pushExtendHead
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
{block : List g.flag}
{blocks : List (List g.flag)}
(hdepthOne : 1 ∉ rest.eventDepths)
(compatible : EventCompatible (NFParse.push hr hlhs hc hrhs rest) (block :: blocks))
:
EventCompatible rest ((f :: block) :: blocks)
If the pushed child has no event at depth one, the new flag may be fused into the existing first block while preserving all event boundaries.
Equations
- One or more equations did not get rendered due to their size.