LanglibProductive-owner provenance for compressed layouts #
EventCompatible records only that every event depth is a physical block boundary. It does
not say which productive node owns a selected block, and a binary child can inherit a parent
block whose endpoint belongs only to its sibling. EventOwnedLayout adds exactly that local
provenance: every owner is either the canonical owner of its cumulative endpoint in the current
parse, or lies outside the current parse's productive-owner window. The latter alternative is
what makes the ledger stable under binary descent.
def
IndexedGrammar.Aho.blockOwnerAt
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{blocks : List (List g.flag)}
(owners : List (Fin (10 * input.length)))
(hlen : owners.length = blocks.length)
(i : Fin blocks.length)
:
Read the owner aligned with a block index.
Equations
- IndexedGrammar.Aho.blockOwnerAt owners hlen i = owners.get ⟨↑i, ⋯⟩
Instances For
def
IndexedGrammar.Aho.OutsideProductiveWindow
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(owner : Fin (10 * input.length))
:
An inherited owner belongs to a disjoint productive subtree when it lies outside the current parse's contiguous owner window.
Equations
- IndexedGrammar.Aho.OutsideProductiveWindow window owner = (↑owner < window.base ∨ window.base + parse.productiveCount ≤ ↑owner)
Instances For
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.scratchOwner_outside
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hinput : 0 < input.length)
:
OutsideProductiveWindow window (scratchOwner hinput)
The distinguished persistent scratch owner is outside every productive window.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.transientOwner_outside
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hinput : 0 < input.length)
:
OutsideProductiveWindow window (transientOwner hinput)
The distinguished collision owner is outside every productive window.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.genericOwner_outside
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{owner : Fin (10 * input.length)}
(howner : owner ∈ genericOwnerRange g input)
:
OutsideProductiveWindow window owner
Every reusable generic label lies beyond every primary productive-owner window.
structure
IndexedGrammar.Aho.EventOwnedLayout
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
Semantic owner refinement of EventCompatible.
At every nonempty physical block endpoint, either the aligned owner is the canonical current event owner, or it is inherited from a disjoint productive window. Binary children use the second case for cuts contributed only by their sibling.
- compatible : EventCompatible parse blocks
- owner_at (i : Fin blocks.length) : (∃ (hd : blockEndpoint blocks i ∈ parse.eventDepths), blockOwnerAt owners ⋯ i = window.eventOwner (blockEndpoint blocks i) hd) ∨ OutsideProductiveWindow window (blockOwnerAt owners ⋯ i)
Instances For
@[simp]
theorem
IndexedGrammar.Aho.EventOwnedLayout.blockEndpoint_cons_succ
{T : Type}
{g : IndexedGrammar T}
(block : List g.flag)
(blocks : List (List g.flag))
(i : Fin blocks.length)
:
@[simp]
theorem
IndexedGrammar.Aho.EventOwnedLayout.blockOwnerAt_cons_succ
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{block : List g.flag}
{blocks : List (List g.flag)}
(owner : Fin (10 * input.length))
(owners : List (Fin (10 * input.length)))
(hlen : (owner :: owners).length = (block :: blocks).length)
(i : Fin blocks.length)
:
@[simp]
theorem
IndexedGrammar.Aho.EventOwnedLayout.blockEndpoint_cons_zero
{T : Type}
{g : IndexedGrammar T}
(block : List g.flag)
(blocks : List (List g.flag))
:
@[simp]
theorem
IndexedGrammar.Aho.EventOwnedLayout.blockOwnerAt_cons_zero
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{block : List g.flag}
{blocks : List (List g.flag)}
(owner : Fin (10 * input.length))
(owners : List (Fin (10 * input.length)))
(hlen : (owner :: owners).length = (block :: blocks).length)
:
def
IndexedGrammar.Aho.EventOwnedLayout.tail
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
(ledger : EventOwnedLayout parse window (block :: blocks) (owner :: owners))
(compatible : EventCompatible residual blocks)
(endpoint_pos : ∀ (i : Fin blocks.length), 0 < blockEndpoint blocks i)
(outside : ∀ (o : Fin (10 * input.length)), OutsideProductiveWindow window o → OutsideProductiveWindow residualWindow o)
(owner_shift :
∀ (i : Fin blocks.length) (hd : block.length + blockEndpoint blocks i ∈ parse.eventDepths),
∃ (hd' : blockEndpoint blocks i ∈ residual.eventDepths),
window.eventOwner (block.length + blockEndpoint blocks i) hd = residualWindow.eventOwner (blockEndpoint blocks i) hd')
:
EventOwnedLayout residual residualWindow blocks owners
Remove the first block while transporting endpoint-event ownership through a unary or atomic-pop continuation. The caller supplies precisely the semantic shift of endpoint owners; the concrete list alignment is handled here.
Equations
Instances For
def
IndexedGrammar.Aho.EventOwnedLayout.cons
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{nextParse : g.NFParse B stack' w}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow parse}
{nextWindow : ProductiveOwnerWindow nextParse}
(ledger : EventOwnedLayout parse window blocks owners)
(compatible : EventCompatible nextParse (block :: blocks))
(block_pos : 0 < block.length)
(head_owner :
(∃ (hd : block.length ∈ nextParse.eventDepths), owner = nextWindow.eventOwner block.length hd) ∨ OutsideProductiveWindow nextWindow owner)
(outside : ∀ (o : Fin (10 * input.length)), OutsideProductiveWindow window o → OutsideProductiveWindow nextWindow o)
(owner_shift :
∀ (i : Fin blocks.length) (hd : blockEndpoint blocks i ∈ parse.eventDepths),
∃ (hd' : block.length + blockEndpoint blocks i ∈ nextParse.eventDepths),
window.eventOwner (blockEndpoint blocks i) hd = nextWindow.eventOwner (block.length + blockEndpoint blocks i) hd')
:
EventOwnedLayout nextParse nextWindow (block :: blocks) (owner :: owners)
Prepend a new physical block while transporting every old endpoint by the new block's length. The head's provenance is explicit, so this constructor supports both a canonical fresh event owner and an owner inherited from outside the new window.
Equations
Instances For
theorem
IndexedGrammar.Aho.EventOwnedLayout.outside_pushChild
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{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}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{owner : Fin (10 * input.length)}
(hout : OutsideProductiveWindow window owner)
:
OutsideProductiveWindow window.pushChild owner
Unary push windows have the same interval as their parents.
def
IndexedGrammar.Aho.EventOwnedLayout.pushFresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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)}
{owners : List (Fin (10 * input.length))}
{newOwner : Fin (10 * input.length)}
{window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest)}
(ledger : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks owners)
(head_owner :
(∃ (h₁ : 1 ∈ rest.eventDepths), newOwner = window.pushChild.eventOwner 1 h₁) ∨ OutsideProductiveWindow window.pushChild newOwner)
:
Specialized fresh-block transport for a unary push. The new head may be either a canonical depth-one event block or an inherited owner outside the child window.
Equations
- ledger.pushFresh head_owner = ledger.cons ledger.compatible.pushFresh ⋯ head_owner ⋯ ⋯
Instances For
def
IndexedGrammar.Aho.EventOwnedLayout.pushCompress
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest)}
(hdepthOne : 1 ∉ rest.eventDepths)
(ledger : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window (block :: blocks) owners)
:
EventOwnedLayout rest window.pushChild ((f :: block) :: blocks) owners
Specialized fused-head transport for a unary push. No owner is allocated: all old positive endpoints and their owners shift together by one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IndexedGrammar.Aho.EventOwnedLayout.atomicPopTail
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow parse}
(ledger : EventOwnedLayout parse window (block :: blocks) (owner :: owners))
(compatible : EventCompatible residual blocks)
(endpoint_pos : ∀ (i : Fin blocks.length), 0 < blockEndpoint blocks i)
(hproductive : residual.productiveCount = parse.productiveCount)
(hevents : ∀ (d : ℕ), d ∈ residual.eventDepths ↔ block.length + d ∈ parse.eventDepths)
(howners : ∀ (d : ℕ), residual.eventOwnerNat d = parse.eventOwnerNat (block.length + d))
:
EventOwnedLayout residual (window.transport hproductive) blocks owners
Transport a tail ledger through an atomic whole-block pop. This consumes exactly the owner
shift furnished by exists_popContinuation_of_eventFree_block_with_owners.
Equations
- ledger.atomicPopTail compatible endpoint_pos hproductive hevents howners = ledger.tail compatible endpoint_pos ⋯ ⋯
Instances For
theorem
IndexedGrammar.Aho.EventOwnedLayout.eventOwner_not_mem_owners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{window : ProductiveOwnerWindow parse}
{blocks : List (List g.flag)}
{owners : List (Fin (10 * input.length))}
(ledger : EventOwnedLayout parse window blocks owners)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hdiff : ∀ (i : Fin blocks.length), d ≠ blockEndpoint blocks i)
:
window.eventOwner d hd ∉ owners
A canonical event owner whose depth differs from every represented endpoint is absent from the layout's complete owner list. Outside-window inherited owners cannot collide with it.
theorem
IndexedGrammar.Aho.EventOwnedLayout.outside_binaryLeft
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{owner : Fin (10 * input.length)}
(hout : OutsideProductiveWindow window owner)
:
OutsideProductiveWindow window.binaryLeft owner
Owners outside a parent window are outside its left binary subwindow.
theorem
IndexedGrammar.Aho.EventOwnedLayout.outside_binaryRight
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{owner : Fin (10 * input.length)}
(hout : OutsideProductiveWindow window owner)
:
OutsideProductiveWindow window.binaryRight owner
Owners outside a parent window are outside its right binary subwindow.
def
IndexedGrammar.Aho.EventOwnedLayout.binaryLeft
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
(ledger : EventOwnedLayout (NFParse.binary hr hlhs hc hrhs left right) window blocks owners)
:
EventOwnedLayout left window.binaryLeft blocks owners
Restrict an owner ledger to the left binary child. Parent endpoints belonging only to the right child become inherited owners outside the left productive window.
Equations
- ledger.binaryLeft = { compatible := ledger.compatible.binaryLeft, owners_length := ⋯, endpoint_pos := ⋯, owner_at := ⋯ }
Instances For
def
IndexedGrammar.Aho.EventOwnedLayout.binaryRight
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{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)}
{owners : List (Fin (10 * input.length))}
{window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right)}
(ledger : EventOwnedLayout (NFParse.binary hr hlhs hc hrhs left right) window blocks owners)
:
EventOwnedLayout right window.binaryRight blocks owners
Restrict an owner ledger to the right binary child. Parent endpoints selected from the left child become inherited owners outside the right productive window.
Equations
- ledger.binaryRight = { compatible := ledger.compatible.binaryRight, owners_length := ⋯, endpoint_pos := ⋯, owner_at := ⋯ }