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.