LanglibProductive-owner provenance for open frames #
Selected blocks which cross an atomic pop leave their index in the stable prefix and put a
matching close atom in the continuation. Relative to the current parse, each open frame is
either inherited from outside the active productive window or is the canonical owner of one
of the current parse's productive events. This file records that provenance independently of
the runner.
It also records the purely syntactic invariant that persistent indices in the cursor prefix
are a permutation of all currently open frame owners. The latter is deliberately stated up
to permutation: opening nested frames places the selected index and its close marker in
opposite traversal orders.
def
IndexedGrammar.Aho.EventOwnedFrame
{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))
:
One open frame is either inherited from outside the active productive window or owns a canonical event of the current parse.
Equations
- IndexedGrammar.Aho.EventOwnedFrame parse window owner = (IndexedGrammar.Aho.OutsideProductiveWindow window owner ∨ ∃ (event : ↥parse.eventDepths), owner = window.eventOwner ↑event ⋯)
Instances For
structure
IndexedGrammar.Aho.EventOwnedFrames
{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)
(owners : List (Fin (10 * input.length)))
:
Productive provenance for every currently open frame owner.
- owner_at (owner : Fin (10 * input.length)) : owner ∈ owners → EventOwnedFrame parse window owner
Instances For
theorem
IndexedGrammar.Aho.EventOwnedFrames.nil
{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}
:
EventOwnedFrames parse window []
The empty frame stack has canonical provenance.
theorem
IndexedGrammar.Aho.EventOwnedFrames.cons
{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}
{owners : List (Fin (10 * input.length))}
{owner : Fin (10 * input.length)}
(head : EventOwnedFrame parse window owner)
(tail : EventOwnedFrames parse window owners)
:
EventOwnedFrames parse window (owner :: owners)
Add a frame whose provenance is already known.
theorem
IndexedGrammar.Aho.EventOwnedFrames.transport
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames parse window owners)
(shift :
∀ (owner : Fin (10 * input.length)),
EventOwnedFrame parse window owner → EventOwnedFrame residual residualWindow owner)
:
EventOwnedFrames residual residualWindow owners
Transport all frame classifications through an arbitrary change of active parse/window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.perm
{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}
{owners owners' : List (Fin (10 * input.length))}
(frames : EventOwnedFrames parse window owners)
(hperm : owners'.Perm owners)
:
EventOwnedFrames parse window owners'
Frame provenance is insensitive to the traversal order of the open-frame ledger.
theorem
IndexedGrammar.Aho.EventOwnedFrames.eventOwner_not_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}
{d : ℕ}
(hd : d ∈ parse.eventDepths)
:
¬OutsideProductiveWindow window (window.eventOwner d hd)
A canonical event owner lies inside its productive window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.first_owner
{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}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners : List (Fin (10 * input.length))}
(layout : EventOwnedLayout parse window (block :: blocks) (owner :: owners))
:
(∃ (hd : block.length ∈ parse.eventDepths), owner = window.eventOwner block.length hd) ∨ OutsideProductiveWindow window owner
The first aligned block owner is either canonical at the first block endpoint or inherited from outside the active window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.atomicPop
{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}
{window : ProductiveOwnerWindow parse}
{residualWindow : ProductiveOwnerWindow residual}
{block : List g.flag}
{blocks : List (List g.flag)}
{owner : Fin (10 * input.length)}
{owners frameOwners : List (Fin (10 * input.length))}
(layout : EventOwnedLayout parse window (block :: blocks) (owner :: owners))
(frames : EventOwnedFrames parse window frameOwners)
(outside :
∀ (candidate : Fin (10 * input.length)),
OutsideProductiveWindow window candidate → OutsideProductiveWindow residualWindow candidate)
(owner_shift :
∀ (hd : block.length ∈ parse.eventDepths),
∃ (hd0 : 0 ∈ residual.eventDepths), window.eventOwner block.length hd = residualWindow.eventOwner 0 hd0)
(frame_shift :
∀ (event : ↥parse.eventDepths),
∃ (residualEvent : ↥residual.eventDepths), window.eventOwner ↑event ⋯ = residualWindow.eventOwner ↑residualEvent ⋯)
:
EventOwnedFrames residual residualWindow (owner :: frameOwners)
Open the first aligned block as a frame after an atomic pop. The selected local endpoint becomes residual depth zero, while every existing canonical frame follows the continuation's event-owner transport.
theorem
IndexedGrammar.Aho.EventOwnedFrames.outside_transport
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{residual : g.NFParse B stack' w'}
(window : ProductiveOwnerWindow parse)
(hcount : residual.productiveCount = parse.productiveCount)
{owner : Fin (10 * input.length)}
(hout : OutsideProductiveWindow window owner)
:
OutsideProductiveWindow (window.transport hcount) owner
Outside-window ownership is unchanged by an equal-productive-count window transport.
theorem
IndexedGrammar.Aho.EventOwnedFrames.pop
{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 = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
{window : ProductiveOwnerWindow (NFParse.pop hr hlhs hc hrhs rest)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.pop hr hlhs hc hrhs rest) window owners)
:
EventOwnedFrames rest (window.transport ⋯) owners
Transport every framed event through the one-position event shift of a concrete pop.
theorem
IndexedGrammar.Aho.EventOwnedFrames.push
{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)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.push hr hlhs hc hrhs rest) window owners)
:
EventOwnedFrames rest window.pushChild owners
Every framed event of a push follows its canonical child preimage.
theorem
IndexedGrammar.Aho.EventOwnedFrames.zero_outside_binaryLeft
{T : Type}
{g : IndexedGrammar T}
{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))
(hd : 0 ∈ (NFParse.binary hr hlhs hc hrhs left right).eventDepths)
:
OutsideProductiveWindow window.binaryLeft (window.eventOwner 0 hd)
The binary root owner lies strictly before the left child's productive window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.zero_outside_binaryRight
{T : Type}
{g : IndexedGrammar T}
{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))
(hd : 0 ∈ (NFParse.binary hr hlhs hc hrhs left right).eventDepths)
:
OutsideProductiveWindow window.binaryRight (window.eventOwner 0 hd)
The binary root owner lies strictly before the right child's productive window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.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)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.binary hr hlhs hc hrhs left right) window owners)
:
EventOwnedFrames left window.binaryLeft owners
A parent frame restricts to the matching left event, or becomes outside the left window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.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)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.binary hr hlhs hc hrhs left right) window owners)
:
EventOwnedFrames right window.binaryRight owners
A parent frame restricts to the matching right event, or becomes outside the right window.
structure
IndexedGrammar.Aho.PrefixFrameLedger
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
:
Prefix indices and open-frame owners are the same finite ledger, up to traversal order.
- owners_perm : (List.filterMap ScheduleAtom.indexOwner? cursor.left).Perm cursor.frameOwners
Instances For
theorem
IndexedGrammar.Aho.PrefixFrameLedger.of_empty
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(hleft : List.filterMap ScheduleAtom.indexOwner? cursor.left = [])
(hframes : cursor.frameOwners = [])
:
PrefixFrameLedger cursor
A cursor with no prefix indices and no open frames has an empty ledger.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.prefix_length_eq_frameCount
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : PrefixFrameLedger cursor)
:
The ledger equates prefix-index count with open-frame count.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : PrefixFrameLedger old)
(hprefix : (List.filterMap ScheduleAtom.indexOwner? new.left).Perm (List.filterMap ScheduleAtom.indexOwner? old.left))
(hframes : new.frameOwners.Perm old.frameOwners)
:
Transport a prefix/frame ledger across arbitrary owner permutations.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.insert
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : PrefixFrameLedger old)
(owner : Fin (10 * input.length))
(hprefix :
(List.filterMap ScheduleAtom.indexOwner? new.left).Perm (owner :: List.filterMap ScheduleAtom.indexOwner? old.left))
(hframes : new.frameOwners.Perm (owner :: old.frameOwners))
:
Insert one matched prefix index and open frame. The hypotheses are phrased as permutations so runner-specific zipper rearrangements remain outside this generic API.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.remove
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : PrefixFrameLedger old)
(owner : Fin (10 * input.length))
(hprefix :
(List.filterMap ScheduleAtom.indexOwner? old.left).Perm (owner :: List.filterMap ScheduleAtom.indexOwner? new.left))
(hframes : old.frameOwners.Perm (owner :: new.frameOwners))
:
Remove one matched prefix index and frame.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.eventOwner_not_mem_indexOwners
{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}
{cursor : ScheduleCursor g input}
{blocks : List (List g.flag)}
{owners outsideOwners : List (Fin (10 * input.length))}
(prefixLedger : PrefixFrameLedger cursor)
(layout : EventOwnedLayout parse window blocks owners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hright : List.filterMap ScheduleAtom.indexOwner? cursor.right = owners ++ outsideOwners)
(houtside : ∀ owner ∈ outsideOwners, OutsideProductiveWindow window owner)
{d : ℕ}
(hd : d ∈ parse.eventDepths)
(hframeFresh : window.eventOwner d hd ∉ cursor.frameOwners)
(hdiff : ∀ (i : Fin blocks.length), d ≠ blockEndpoint blocks i)
:
window.eventOwner d hd ∉ cursor.indexOwners
Complete cursor-level freshness from the three owner ledgers. Prefix indices are open frames, selected right-side indices are governed by the event layout, and every remaining right-side index is explicitly outside the active productive window.