Finite canonical LR action table

Canonical parser states are the raw finite kernels stored on the parse stack; their epsilon closure is inspected for actions. Reduction has priority in the total table definition. On reachable states LR(k) uniqueness proves that the arbitrary finite choice of a complete item cannot affect the selected grammar rule.

@[reducible, inline]

abbrev CF_grammar.LRk.KernelState {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Type

Finite raw states of the canonical viable-prefix automaton.

Equations

• CF_grammar.LRk.KernelState G k = Finset (CF_grammar.LRk.Item G.augment k)

def CF_grammar.LRk.EnabledReduction {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) (i : Item G.augment k) : Prop

A complete item enabled in a raw state at the displayed lookahead.

Equations

• CF_grammar.LRk.EnabledReduction G k q u i = (i ∈ CF_grammar.LRk.closure G.augment k q ∧ i.Complete ∧ i.lookahead = u)

noncomputable def CF_grammar.LRk.reductionItem? {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) : Option (Item G.augment k)

Choose one enabled reduction item. The choice is deliberately finite and noncomputable: automata in this repository are mathematical transition functions, and LR(k) uniqueness later proves rule-independence.

Equations

• CF_grammar.LRk.reductionItem? G k q u = if h : ∃ (i : CF_grammar.LRk.Item G.augment k), CF_grammar.LRk.EnabledReduction G k q u i then some (Classical.choose h) else none

theorem CF_grammar.LRk.reductionItem?_eq_some_iff {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) (i : Item G.augment k) : reductionItem? G k q u = some i → EnabledReduction G k q u i

theorem CF_grammar.LRk.reductionItem?_eq_none_iff {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) : reductionItem? G k q u = none ↔ ¬∃ (i : Item G.augment k), EnabledReduction G k q u i

theorem CF_grammar.LRk.exists_reductionItem?_eq_some {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) (h : ∃ (i : Item G.augment k), EnabledReduction G k q u i) : ∃ (i : Item G.augment k), reductionItem? G k q u = some i

def CF_grammar.LRk.ShiftEnabled {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (a : T) : Prop

A terminal is syntactically shift-supported when some closed item has it immediately after the dot. The total table below safely defaults to shifting whenever no semantic reduction is enabled; this predicate remains useful for the usual canonical-item characterization of reachable shifts.

Equations

• CF_grammar.LRk.ShiftEnabled G k q a = ∃ i ∈ CF_grammar.LRk.closure G.augment k q, i.next? = some (symbol.terminal a)

inductive CF_grammar.LRk.TableAction {T : Type} (G : CF_grammar T) : Type

Total finite action selected by a canonical table.

• shift {T : Type} {G : CF_grammar T} : TableAction G
• reduce {T : Type} {G : CF_grammar T} (rule : RuleIndex G.augment) : TableAction G
• accept {T : Type} {G : CF_grammar T} : TableAction G
• error {T : Type} {G : CF_grammar T} : TableAction G

def CF_grammar.LRk.lookaheadHead {T : Type} (k : ℕ) (u : Lookahead T k) : Option T

First buffered symbol, returning EOF for the degenerate zero-lookahead buffer. The final construction uses k+1, so its reachable buffers are always nondegenerate.

Equations

• CF_grammar.LRk.lookaheadHead k u = if h : 0 < k then u ⟨0, h⟩ else none

noncomputable def CF_grammar.LRk.tableAction {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) : TableAction G

Canonical table action. A completed augmented-start item is acceptance; all other completed items are reductions. If there is no reduction, a syntactically enabled terminal is shifted.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CF_grammar.LRk.nextKernel {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (X : symbol T G.augment.nt) : KernelState G k

The raw goto state used after shifting or reducing a grammar symbol.

Equations

• CF_grammar.LRk.nextKernel G k q X = CF_grammar.LRk.goto G.augment k q X

theorem CF_grammar.LRk.tableAction_accept_iff {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) : tableAction G k q u = TableAction.accept ↔ ∃ (i : Item G.augment k), reductionItem? G k q u = some i ∧ i.rule = startRuleIndex G

theorem CF_grammar.LRk.tableAction_reduce_iff {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) (r : RuleIndex G.augment) : tableAction G k q u = TableAction.reduce r ↔ ∃ (i : Item G.augment k), reductionItem? G k q u = some i ∧ i.rule ≠ startRuleIndex G ∧ i.rule = r

theorem CF_grammar.LRk.tableAction_shift_of_none {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (q : KernelState G k) (u : Lookahead T k) {a : T} (hred : reductionItem? G k q u = none) (hhead : lookaheadHead k u = some a) : tableAction G k q u = TableAction.shift

theorem CF_grammar.LRk.reductionItem?_reductionCandidate {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {i : Item G.augment k} (h : reductionItem? G k (scanKernel G k gamma) u = some i) : ReductionCandidate G.augment k gamma u (ruleAt G.augment i.rule)

On a reachable state, every chosen complete item is a semantic reduction candidate at the corresponding scanned prefix.

theorem CF_grammar.LRk.reductionItem?_rule_eq_of_stateReduction {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hLR : G.IsLRk k) {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {r : G.augment.nt × List (symbol T G.augment.nt)} (hr : StateReduction G k gamma u r) : ∃ (i : Item G.augment k), reductionItem? G k (scanKernel G k gamma) u = some i ∧ ruleAt G.augment i.rule = r

If a particular semantic reduction is exposed in a reachable state, the finite table chooses an item naming the same production value.