Langlib

Langlib.Grammars.Indexed.NormalForm.Aho.Scheduler.Runners.Overlay.Binary

Binary events in a copy-on-write overlay #

At a binary fork the complete adjacent overlay becomes shared by the two children. We can therefore forget its branch-local classification, run the existing protected binary scheduler on AdjacentOverlayLayout.toProtected, and then erase the marked private indices one at a time.

theorem IndexedGrammar.Aho.overlayScheduleRun_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]) (leftParse : g.NFParse B stack u) (rightParse : g.NFParse C stack v) (leftRuns : OrdinaryScheduleRuns leftParse) (rightRuns : OrdinaryScheduleRuns rightParse) :
OverlayScheduleRun (NFParse.binary hr hlhs hc hrhs leftParse rightParse)

Seal an arbitrary nonempty overlay at a binary fork, reuse the protected binary runner on the resulting full block layout, and erase every private marked index before returning to the protected base endpoint.