Pop certificates and continuations

Compressed pop paths, parse continuations, and rule certificates used by the scheduler.

Rule certificates used by the scheduler

Canonical compression of a nonempty augmented-pop path

inductive IndexedGrammar.Aho.PopPath {T : Type} (g : IndexedGrammar T) : g.nt → List g.flag → g.nt → Prop

A nonempty top-to-bottom sequence of augmented flag pops. This is the semantic object extracted from a maximal unary portion of the concrete parse before one productive event.

• one {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (edge : AugPop g f A B) : PopPath g A [f] B
• cons {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {f : g.flag} {flags : List g.flag} (edge : AugPop g f A B) (rest : PopPath g B flags C) : PopPath g A (f :: flags) C

theorem IndexedGrammar.Aho.augPop_preNeutral {T : Type} {g : IndexedGrammar T} {A X Y : g.nt} {f : g.flag} (hneutral : Neutral g A X) (hpop : AugPop g f X Y) : AugPop g f A Y

Neutral prefixes may be absorbed into the newly pre-saturated augmented pop relation.

noncomputable def IndexedGrammar.Aho.compressedFlags {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (f : g.flag) : List g.flag → CFlag g

Compress a syntactically nonempty concrete flag string.

Equations

• IndexedGrammar.Aho.compressedFlags g f [] = IndexedGrammar.Aho.cflagBase g f
• IndexedGrammar.Aho.compressedFlags g f (f' :: flags) = IndexedGrammar.Aho.cflagComp g (IndexedGrammar.Aho.cflagBase g f) (IndexedGrammar.Aho.compressedFlags g f' flags)

theorem IndexedGrammar.Aho.PopPath.preNeutral {T : Type} {g : IndexedGrammar T} {A X Y : g.nt} {flags : List g.flag} (hneutral : Neutral g A X) (path : PopPath g X flags Y) : PopPath g A flags Y

Absorb a neutral prefix into the first edge of a nonempty compressed pop path.

theorem IndexedGrammar.Aho.PopPath.flags_ne_nil {T : Type} {g : IndexedGrammar T} {A B : g.nt} {flags : List g.flag} (path : PopPath g A flags B) : flags ≠ []

A pop path's flag string is nonempty.

theorem IndexedGrammar.Aho.PopPath.denotes_compressedFlags {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {flags : List g.flag} (path : PopPath g A flags B) : ∃ (f : g.flag) (rest : List g.flag), flags = f :: rest ∧ CFlag.Denotes g flags (compressedFlags g f rest)

The canonical compressed relation denotes exactly the path's concrete flag string.

theorem IndexedGrammar.Aho.PopPath.compressedFlags_edge {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {flags : List g.flag} (path : PopPath g A flags B) : ∃ (f : g.flag) (rest : List g.flag), flags = f :: rest ∧ compressedFlags g f rest A B = true

The endpoints of a pop path form an edge of its canonical compressed relation.

theorem IndexedGrammar.Aho.PopPath.compressedFlags_nonempty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {flags : List g.flag} (path : PopPath g A flags B) : ∃ (f : g.flag) (rest : List g.flag), flags = f :: rest ∧ (compressedFlags g f rest).Nonempty

Hence the compressed block accepted by a pop path is nonempty, as required by livePushCompress.

theorem IndexedGrammar.Aho.PopPath.derives {T : Type} {g : IndexedGrammar T} {A B : g.nt} {flags : List g.flag} (path : PopPath g A flags B) (suffix : List g.flag) : g.Derives [ISym.indexed A (flags ++ suffix)] [ISym.indexed B suffix]

A pop path consumes its whole concrete block above every suffix.

theorem IndexedGrammar.Aho.PopPath.uncons {T : Type} {g : IndexedGrammar T} {A C : g.nt} {f f' : g.flag} {flags : List g.flag} (path : PopPath g A (f :: f' :: flags) C) : ∃ (B : g.nt), AugPop g f A B ∧ PopPath g B (f' :: flags) C

Split the first edge from a path known to contain at least two concrete flags.

theorem IndexedGrammar.Aho.consumeRoute_factor_noBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : NFParse.ConsumeRoute g p k) (hroute : route.NoBinary) : ∃ (X : g.nt) (Y : g.nt), Neutral g A X ∧ PopPath g X (List.take (k + 1) stack) Y

A route containing no binary event factors into a neutral prefix followed by a compressed pop path for exactly the inherited occurrences down through its target.

theorem IndexedGrammar.Aho.consumeRoute_popContinuation_noBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : NFParse.ConsumeRoute g p k) (hroute : route.NoBinary) : ∃ (Y : g.nt) (suffix : List g.flag) (rest : g.NFParse Y suffix w), suffix = List.drop (k + 1) stack ∧ PopPath g A (List.take (k + 1) stack) Y ∧ rest.nodeCount < p.nodeCount

Strengthened binary-free factorization retaining the residual concrete parse. The resulting compressed path starts at the current nonterminal (the neutral prefix is absorbed into its first pre-saturated pop edge), and the residual parse is strictly smaller.

theorem IndexedGrammar.Aho.compressedFlags_nonempty_of_consumeRoute_noBinary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {p : g.NFParse A (f :: stack) w} {k : ℕ} (route : NFParse.ConsumeRoute g p k) (hroute : route.NoBinary) : ∃ (f₀ : g.flag) (flags : List g.flag), List.take (k + 1) (f :: stack) = f₀ :: flags ∧ (compressedFlags g f₀ flags).Nonempty

Therefore a binary-free route always yields a nonempty canonical compressed relation for the followed inherited prefix.

Parse continuations after a compressed pop

structure IndexedGrammar.Aho.PopContinuation {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} (flags suffix : List g.flag) {w : List T} (p : g.NFParse A (flags ++ suffix) w) (R : CFlag g) : Type

PopContinuation p R is the exact semantic witness needed to consume the compressed block R: an edge of R reaches a nonterminal which still has a concrete parse of the same terminal yield over the unrepresented suffix. The scheduler may follow this witness even when it differs from the unary choices made inside p; indexed-grammar nondeterminism only requires one accepting continuation.

• next : g.nt
• rest : g.NFParse self.next suffix w
• edge : R A self.next = true

theorem IndexedGrammar.Aho.exists_popContinuation_of_noBinary_route {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {f : g.flag} {flags suffix : List g.flag} {w : List T} (parse : g.NFParse A (f :: flags ++ suffix) w) (route : NFParse.ConsumeRoute g parse flags.length) (hroute : route.NoBinary) : ∃ (continuation : PopContinuation (f :: flags) suffix parse (compressedFlags g f flags)), continuation.rest.nodeCount < parse.nodeCount

A binary-free route to the last occurrence of a visible block produces an immediate viable continuation for that whole block. Its residual parse is strictly smaller.

def IndexedGrammar.Aho.PopContinuation.ofPop {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {suffix : 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 suffix w) : PopContinuation [f] suffix (NFParse.pop hr hlhs hc hrhs rest) (cflagBase g f)

A concrete top-pop parse constructor gives an immediate continuation for the base compressed flag.

Equations

• IndexedGrammar.Aho.PopContinuation.ofPop hr hlhs hc hrhs rest = { next := B, rest := rest, edge := ⋯ }

def IndexedGrammar.Aho.PopContinuation.ofPopPath {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {flags suffix : List g.flag} {w : List T} (parse : g.NFParse A (f :: flags ++ suffix) w) (path : PopPath g A (f :: flags) B) (rest : g.NFParse B suffix w) : PopContinuation (f :: flags) suffix parse (compressedFlags g f flags)

A canonical PopPath followed by a parse of the residual stack gives a compressed-pop continuation.

Equations

• IndexedGrammar.Aho.PopContinuation.ofPopPath parse path rest = { next := B, rest := rest, edge := ⋯ }

theorem IndexedGrammar.Aho.PopContinuation.relation_nonempty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {flags suffix : List g.flag} {w : List T} {parse : g.NFParse A (flags ++ suffix) w} {R : CFlag g} (continuation : PopContinuation flags suffix parse R) : R.Nonempty

A viable compressed continuation witnesses the nonemptiness side condition used when a new flag is compressed into that block.

theorem IndexedGrammar.Aho.PopContinuation.composite_popPlain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {A : g.nt} {flags suffix : List g.flag} {w : List T} {parse : g.NFParse A (flags ++ suffix) w} {R : CFlag g} (continuation : PopContinuation flags suffix parse R) (d : IndexMark) (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (hfree : IndexFree beta) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } } { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.plain continuation.next, right := WorkSym.close :: gamma } }

Execute a viable compressed continuation and enter a plain residual task.

theorem IndexedGrammar.Aho.PopContinuation.composite_popLive {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {A : g.nt} {flags suffix : List g.flag} {w : List T} {parse : g.NFParse A (flags ++ suffix) w} {R : CFlag g} (continuation : PopContinuation flags suffix parse R) (d : IndexMark) (hlater : d.later = true) (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (hfree : IndexFree beta) : CompositeStep g input { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } } { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.live continuation.next, right := WorkSym.close :: gamma } }

Execute a viable compressed continuation and enter a live residual task.

theorem IndexedGrammar.Aho.augBinary_of_nfparse_binary {T : Type} {g : IndexedGrammar 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) : AugBinary g A B C

The binary constructor of an NFParse supplies the corresponding augmented binary edge.

theorem IndexedGrammar.Aho.augPush_of_nfparse_push {T : Type} {g : IndexedGrammar 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) : AugPush g A B f

The push constructor of an NFParse supplies the corresponding augmented push edge.

theorem IndexedGrammar.Aho.augTerminal_of_nfparse_terminal {T : Type} {g : IndexedGrammar T} {A : g.nt} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) : AugTerminal g A a

The terminal constructor of an NFParse supplies the corresponding augmented terminal edge.

theorem IndexedGrammar.Aho.cflagBase_edge_of_nfparse_pop {T : Type} {g : IndexedGrammar 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) : cflagBase g f A B = true

A concrete top-pop rule is an edge of the base compressed flag used by the machine.