LR Parser Semantics

This file defines the table-driven parser side of LR parsing. It is intentionally separate from Langlib.Grammars.LR.Definition, which contains the grammar-side LR(k) predicate.

The definitions here are the parser object that the LR(k)-to-DPDA direction will use: a deterministic action/goto table, stack configurations, and the induced one-step parser transition.

As elsewhere in this development, a context-free rule is a pair rule : N × List (symbol T N) whose first component rule.1 is the left-hand nonterminal and whose second component rule.2 is the right-hand output string.

inductive LR.Action (T N State : Type) : Type

Parser action selected by the current parser state and one lookahead symbol.

The lookahead will be none exactly at end-of-input.

• shift {T N State : Type} (next : State) : Action T N State
• reduce {T N State : Type} (rule : N × List (symbol T N)) : Action T N State
• accept {T N State : Type} : Action T N State
• error {T N State : Type} : Action T N State

structure LR.Parser (T N State : Type) : Type

A deterministic LR parsing table.

action q lookahead decides whether to shift, reduce, accept, or reject. goto q A is consulted after reducing to the nonterminal A.

• initial : State
• action : State → Option T → Action T N State
• goto : State → N → Option State

@[reducible, inline]

abbrev LR.Parser.StackEntry (T N State : Type) : Type

A parser stack entry stores the grammar symbol and the state reached after placing that symbol on the stack. The top of the stack is the head of the list.

Equations

• LR.Parser.StackEntry T N State = (symbol T N × State)

structure LR.Parser.Config (T N State : Type) : Type

LR parser configurations.

• input : List T
• stack : List (StackEntry T N State)

def LR.Parser.initialConfig {T N State : Type} (w : List T) : Config T N State

Initial parser configuration on an input word.

Equations

• LR.Parser.initialConfig w = { input := w, stack := [] }

def LR.Parser.stateOfStack {T N State : Type} (p : Parser T N State) (stack : List (StackEntry T N State)) : State

The current parser state: either the state stored at the top of the stack or the parser's initial state when the stack is empty.

Equations

• p.stateOfStack [] = p.initial
• p.stateOfStack ((fst, q) :: tail) = q

def LR.Parser.topSymbols {T N State : Type} (n : ℕ) (stack : List (StackEntry T N State)) : List (symbol T N)

The grammar symbols stored in the top n parser-stack entries.

Equations

• LR.Parser.topSymbols n stack = List.map Prod.fst (List.take n stack)

def LR.Parser.reduce? {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] (rule : N × List (symbol T N)) (input : List T) (stack : List (StackEntry T N State)) : Option (Config T N State)

Perform a reduce action, if the top stack symbols match the rule's right-hand side and the goto table is defined.

Equations

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

def LR.Parser.step? {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] (c : Config T N State) : Option (Config T N State)

One deterministic parser transition, if any.

Equations

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

def LR.Parser.Step {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] (c d : Config T N State) : Prop

Relational view of one parser transition.

Equations

• p.Step c d = (p.step? c = some d)

@[reducible, inline]

abbrev LR.Parser.Reaches {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] : Config T N State → Config T N State → Prop

Reflexive-transitive closure of parser steps.

Equations

• p.Reaches = Relation.ReflTransGen p.Step

def LR.Parser.Accepts {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] (w : List T) : Prop

A parser accepts an input word when it reaches an end-of-input configuration whose action is accept.

Equations

• p.Accepts w = ∃ (c : LR.Parser.Config T N State), p.Reaches (LR.Parser.initialConfig w) c ∧ c.input = [] ∧ p.action (p.stateOfStack c.stack) none = LR.Action.accept

def LR.Parser.language {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] : Language T

The language accepted by a table-driven LR parser.

Equations

• p.language = setOf p.Accepts

theorem LR.Parser.step_functional {T N State : Type} (p : Parser T N State) [DecidableEq T] [DecidableEq N] {c d₁ d₂ : Config T N State} (h₁ : p.Step c d₁) (h₂ : p.Step c d₂) : d₁ = d₂

The parser transition is deterministic because it is defined by a function.