Parse routes for Aho scheduling

Structural parse measures and canonical routes to consumed stack occurrences.

def IndexedGrammar.NFParse.nodeCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} : g.NFParse A stack w → ℕ

Number of constructors in a concrete parse. The direct scheduler decreases the sum of these counts on every grammar-facing composite step.

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).nodeCount = left.nodeCount + right.nodeCount + 1
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).nodeCount = rest.nodeCount + 1
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).nodeCount = rest.nodeCount + 1
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).nodeCount = 1

@[simp]

theorem IndexedGrammar.NFParse.nodeCount_pos {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : 0 < p.nodeCount

theorem IndexedGrammar.NFParse.nodeCount_cast_stack {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack stack' : List g.flag} {w : List T} (p : g.NFParse A stack w) (h : stack = stack') : (h ▸ p).nodeCount = p.nodeCount

Transporting only the stack index of a parse does not change its constructor count.

theorem IndexedGrammar.NFParse.consumesAt_of_consumesAt_succ {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (k : ℕ) : p.ConsumesAt (k + 1) → p.ConsumesAt k

If a concrete parse consumes stack occurrence k + 1, it also consumes occurrence k. Operationally, a derivation cannot reach a deeper stack occurrence without first popping the one immediately above it.

theorem IndexedGrammar.NFParse.consumesAt_mono {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {i j : ℕ} (hij : i ≤ j) (hj : p.ConsumesAt j) : p.ConsumesAt i

Consumption is downward closed in the stack-position order.

theorem IndexedGrammar.NFParse.not_consumesAt_of_not_consumesAt_zero {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (hzero : ¬p.ConsumesAt 0) (k : ℕ) : ¬p.ConsumesAt k

If the top inherited occurrence is unused, every deeper inherited occurrence is unused too. This is the branch in which the scheduler may safely erase the inherited stack and run a plain task.

theorem IndexedGrammar.NFParse.consumesAt_lt_stack_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {k : ℕ} (hk : p.ConsumesAt k) : k < stack.length

A parse can only consume an occurrence which is actually present in its inherited stack.

theorem IndexedGrammar.NFParse.not_consumesAt_of_stack_nil {T : Type} {g : IndexedGrammar T} {A : g.nt} {w : List T} (p : g.NFParse A [] w) (k : ℕ) : ¬p.ConsumesAt k

In particular, a task with empty inherited stack is necessarily plain.

Chosen routes to consumed stack occurrences

inductive IndexedGrammar.NFParse.ConsumeRoute {T : Type} (g : IndexedGrammar T) {A : g.nt} {stack : List g.flag} {w : List T} : g.NFParse A stack w → ℕ → Type

A data-carrying choice of one branch leading to the pop which consumes stack occurrence k. Every binary node crossed by such a route contributes a nonempty off-path yield interval; those intervals are the owners of uncompressed index blocks.

• binaryLeft {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} {k : ℕ} (route : ConsumeRoute g left k) : ConsumeRoute g (binary hr hlhs hc hrhs left right) k
• binaryRight {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} {k : ℕ} (route : ConsumeRoute g right k) : ConsumeRoute g (binary hr hlhs hc hrhs left right) k
• popHere {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} : ConsumeRoute g (pop hr hlhs hc hrhs rest) 0
• popTail {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} {k : ℕ} (route : ConsumeRoute g rest k) : ConsumeRoute g (pop hr hlhs hc hrhs rest) (k + 1)
• 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} {k : ℕ} (route : ConsumeRoute g rest (k + 1)) : ConsumeRoute g (NFParse.push hr hlhs hc hrhs rest) k

def IndexedGrammar.NFParse.ConsumeRoute.toConsumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} : ∀ (a : ConsumeRoute g p k), p.ConsumesAt k

Forget the chosen route and recover the proposition-valued consumption fact.

Equations

• ⋯ = ⋯

theorem IndexedGrammar.NFParse.ConsumeRoute.nonempty_of_consumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (k : ℕ) (used : p.ConsumesAt k) : Nonempty (ConsumeRoute g p k)

Every proposition-valued consumption fact admits a concrete route.

theorem IndexedGrammar.NFParse.ConsumeRoute.nonempty_iff_consumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (k : ℕ) : Nonempty (ConsumeRoute g p k) ↔ p.ConsumesAt k

Consumption and existence of a chosen route are equivalent.

noncomputable def IndexedGrammar.NFParse.ConsumeRoute.ofConsumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (k : ℕ) (used : p.ConsumesAt k) : ConsumeRoute g p k

Choose a route from a known consumption fact.

Equations

• IndexedGrammar.NFParse.ConsumeRoute.ofConsumesAt p k used = Classical.choice ⋯

Disjoint terminal owners along a consumption route

def IndexedGrammar.NFParse.ConsumeRoute.embedLeft {α : Type} (u v : List α) : Fin u.length → Fin (u ++ v).length

Embed a position in a left child yield into the concatenated parent yield.

Equations

• IndexedGrammar.NFParse.ConsumeRoute.embedLeft u v i = ⟨↑i, ⋯⟩

def IndexedGrammar.NFParse.ConsumeRoute.embedRight {α : Type} (u v : List α) : Fin v.length → Fin (u ++ v).length

Embed a position in a right child yield into the concatenated parent yield.

Equations

• IndexedGrammar.NFParse.ConsumeRoute.embedRight u v i = ⟨u.length + ↑i, ⋯⟩

theorem IndexedGrammar.NFParse.ConsumeRoute.embedLeft_injective {α : Type} (u v : List α) : Function.Injective (embedLeft u v)

theorem IndexedGrammar.NFParse.ConsumeRoute.embedRight_injective {α : Type} (u v : List α) : Function.Injective (embedRight u v)

def IndexedGrammar.NFParse.ConsumeRoute.barrierOwners {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} : ConsumeRoute g p k → List (Fin w.length)

At a binary event, charge the fresh block to the first terminal position of the child not followed by the consumption route. Recursively chosen barriers lie inside the followed child, so all of these owners are distinct.

Equations

• route.binaryLeft.barrierOwners = ⟨u.length, ⋯⟩ :: List.map (IndexedGrammar.NFParse.ConsumeRoute.embedLeft u v) route.barrierOwners
• route.binaryRight.barrierOwners = ⟨0, ⋯⟩ :: List.map (IndexedGrammar.NFParse.ConsumeRoute.embedRight u v) route.barrierOwners
• IndexedGrammar.NFParse.ConsumeRoute.popHere.barrierOwners = []
• route.popTail.barrierOwners = route.barrierOwners
• route.push.barrierOwners = route.barrierOwners

theorem IndexedGrammar.NFParse.ConsumeRoute.barrierOwners_nodup {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.barrierOwners.Nodup

Off-path owners selected at distinct binary events on one route are pairwise distinct.

theorem IndexedGrammar.NFParse.ConsumeRoute.barrierOwners_length_le {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.barrierOwners.length ≤ w.length

Consequently the number of productive barriers on any one consumption route is bounded by the terminal yield length.

def IndexedGrammar.NFParse.ConsumeRoute.NoBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} : ConsumeRoute g p k → Prop

A route has no productive barrier exactly when it reaches its pop using only unary push/pop constructors.

Equations

• route.binaryLeft.NoBinary = False
• route.binaryRight.NoBinary = False
• IndexedGrammar.NFParse.ConsumeRoute.popHere.NoBinary = True
• route.popTail.NoBinary = route.NoBinary
• route.push.NoBinary = route.NoBinary

@[simp]

theorem IndexedGrammar.NFParse.ConsumeRoute.noBinary_iff_barrierOwners_nil {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.NoBinary ↔ route.barrierOwners = []