Concrete parser-stack representation

The DPDA stores canonical kernels rather than grammar symbols. For every symbol in a canonical parser stack it stores the kernel reached after the corresponding prefix, with the current kernel on top and none as a permanent bottom marker.

noncomputable def CF_grammar.LRk.Buffered.stackRep {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) : List (StackSymbol G k)

Complete concrete stack representing a grammar-symbol parser stack.

Equations

• CF_grammar.LRk.Buffered.stackRep G k gamma = List.map some (List.map (CF_grammar.LRk.scanKernel G k) gamma.inits.tail).reverse ++ [none]

@[simp]

theorem CF_grammar.LRk.Buffered.stackRep_nil {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : stackRep G k [] = [none]

@[simp]

theorem CF_grammar.LRk.Buffered.stackRep_append_singleton {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) (X : symbol T G.augment.nt) : stackRep G k (gamma ++ [X]) = some (scanKernel G k (gamma ++ [X])) :: stackRep G k gamma

theorem CF_grammar.LRk.Buffered.stackRep_top {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) : ∃ (Z : StackSymbol G k) (rest : List (StackSymbol G k)), stackRep G k gamma = Z :: rest ∧ kernelOfTop G k Z = scanKernel G k gamma

The represented stack is always nonempty, and its top denotes the current canonical kernel (with none denoting the initial kernel).

theorem CF_grammar.LRk.Buffered.stackRep_append_frames {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma delta : List (symbol T G.augment.nt)) : ∃ (frames : List (StackSymbol G k)), frames.length = delta.length ∧ (∀ Z ∈ frames, Z ≠ none) ∧ stackRep G k (gamma ++ delta) = frames ++ stackRep G k gamma

Appending delta grammar symbols adds exactly delta.length non-bottom frames above the representation of the old prefix.