Buffered canonical LR machine

This file is the concrete finite-control compilation of the canonical LR table. Its input alphabet is Option T: some a encodes an ordinary terminal and none is a consumed right endmarker. The machine keeps a positive fixed lookahead buffer in its control, so EOF-only reductions never need to test raw input exhaustion.

@[reducible, inline]

abbrev CF_grammar.LRk.Buffered.ReductionCursor {T : Type} (G : CF_grammar T) : Type

Finite cursor used while popping the right-hand side of a reduction.

Equations

• CF_grammar.LRk.Buffered.ReductionCursor G = ((r : CF_grammar.LRk.RuleIndex G.augment) × CF_grammar.LRk.Position G.augment r)

noncomputable instance CF_grammar.LRk.Buffered.instFintypeReductionCursor {T : Type} (G : CF_grammar T) : Fintype (ReductionCursor G)

Equations

• CF_grammar.LRk.Buffered.instFintypeReductionCursor G = Sigma.instFintype

def CF_grammar.LRk.Buffered.ReductionCursor.rule {T : Type} {G : CF_grammar T} (c : ReductionCursor G) : RuleIndex G.augment

Equations

• c.rule = c.fst

def CF_grammar.LRk.Buffered.ReductionCursor.remaining {T : Type} {G : CF_grammar T} (c : ReductionCursor G) : ℕ

Equations

• c.remaining = ↑c.snd

def CF_grammar.LRk.Buffered.fullCursor {T : Type} (G : CF_grammar T) (r : RuleIndex G.augment) : ReductionCursor G

Equations

• CF_grammar.LRk.Buffered.fullCursor G r = ⟨r, ⟨(CF_grammar.LRk.ruleAt G.augment r).2.length, ⋯⟩⟩

def CF_grammar.LRk.Buffered.ReductionCursor.pred {T : Type} {G : CF_grammar T} (c : ReductionCursor G) (_h : 0 < c.remaining) : ReductionCursor G

Equations

• c.pred _h = ⟨c.fst, ⟨↑c.snd - 1, ⋯⟩⟩

def CF_grammar.LRk.Buffered.setBuffer {T : Type} {k : ℕ} (u : Lookahead T k) (n : ℕ) (x : Option T) : Lookahead T k

Replace one slot in a fixed lookahead buffer.

Equations

• CF_grammar.LRk.Buffered.setBuffer u n x i = if ↑i = n then x else u i

def CF_grammar.LRk.Buffered.finishBuffer {T : Type} {k : ℕ} (u : Lookahead T k) (n : ℕ) : Lookahead T k

On consuming the explicit endmarker during preload, preserve the already loaded prefix and pad every remaining slot with EOF.

Equations

• CF_grammar.LRk.Buffered.finishBuffer u n i = if ↑i < n then u i else none

def CF_grammar.LRk.Buffered.shiftBuffer {T : Type} {k : ℕ} (_hk : 0 < k) (u : Lookahead T k) (x : Option T) : Lookahead T k

Shift a positive lookahead buffer left and append one newly read symbol.

Equations

• CF_grammar.LRk.Buffered.shiftBuffer _hk u x i = if h : ↑i + 1 < k then u ⟨↑i + 1, h⟩ else x

def CF_grammar.LRk.Buffered.lastBuffer {T : Type} {k : ℕ} (hk : 0 < k) (u : Lookahead T k) : Option T

Last buffered symbol.

Equations

• CF_grammar.LRk.Buffered.lastBuffer hk u = u ⟨k - 1, ⋯⟩

inductive CF_grammar.LRk.Buffered.Control {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Type

Finite control of the marked-input LR machine.

• load {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (count : Fin (k + 1)) (buffer : Lookahead T k) : Control G k
• parse {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (kernel : KernelState G k) (buffer : Lookahead T k) : Control G k
• refill {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (kernel : KernelState G k) (buffer : Lookahead T k) : Control G k
• pop {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (cursor : ReductionCursor G) (buffer : Lookahead T k) : Control G k
• accept {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} : Control G k
• reject {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} : Control G k

instance CF_grammar.LRk.Buffered.instFintypeControl {T✝ : Type} {inst✝ : Fintype T✝} {G✝ : CF_grammar T✝} {k✝ : ℕ} [Fintype T✝] : Fintype (Control G✝ k✝)

Equations

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

@[reducible, inline]

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

Stack symbols are saved raw canonical kernels; none is the permanent bottom marker.

Equations

• CF_grammar.LRk.Buffered.StackSymbol G k = Option (CF_grammar.LRk.KernelState G k)

noncomputable instance CF_grammar.LRk.Buffered.instFintypeStackSymbol {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Fintype (StackSymbol G k)

Equations

• CF_grammar.LRk.Buffered.instFintypeStackSymbol G k = inferInstance

def CF_grammar.LRk.Buffered.kernelOfTop {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : StackSymbol G k → KernelState G k

Kernel represented by a stack top, interpreting the bottom marker as the initial kernel.

Equations

• CF_grammar.LRk.Buffered.kernelOfTop G k none = CF_grammar.LRk.startKernel G k
• CF_grammar.LRk.Buffered.kernelOfTop G k (some q) = q

def CF_grammar.LRk.Buffered.initialControl {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Control G k

Initial buffered control. The positive-lookahead machine starts with an all-EOF scratch buffer and overwrites it from left to right.

Equations

• CF_grammar.LRk.Buffered.initialControl G k = CF_grammar.LRk.Buffered.Control.load ⟨0, ⋯⟩ (CF_grammar.LRk.eofLookahead T k)

noncomputable def CF_grammar.LRk.Buffered.inputTransition {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (q : Control G k) (x : Option T) (Z : StackSymbol G k) : Option (Control G k × List (StackSymbol G k))

Input-reading transitions. Only preload and refill controls read the marked input; all parser operations are epsilon moves over already buffered symbols.

Equations

• One or more equations did not get rendered due to their size.
• CF_grammar.LRk.Buffered.inputTransition G k hk q x Z = none

noncomputable def CF_grammar.LRk.Buffered.epsilonTransition {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (q : Control G k) (Z : StackSymbol G k) : Option (Control G k × List (StackSymbol G k))

Epsilon transitions implementing table actions and finite reduction pops.

Equations

• One or more equations did not get rendered due to their size.
• CF_grammar.LRk.Buffered.epsilonTransition G k hk q Z = none

noncomputable def CF_grammar.LRk.Buffered.machine {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) : DPDA (Control G k) (Option T) (StackSymbol G k)

The concrete DPDA recognizing the explicitly endmarked canonical parser language.

Equations

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