Finite canonical LR(k) items

This file supplies the finite data used by the canonical viable-prefix automaton. Productions are represented by positions in the grammar's rule list, rather than by their (possibly infinitely typed) nonterminals. Thus the item and parser-state types are finite without imposing a Fintype instance on the grammar's nonterminal type.

@[reducible, inline]

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

A production occurrence in the finite rule list.

Equations

• CF_grammar.LRk.RuleIndex G = Fin G.rules.length

def CF_grammar.LRk.ruleAt {T : Type} (G : CF_grammar T) (i : RuleIndex G) : G.nt × List (symbol T G.nt)

The production represented by a rule-list index.

Equations

• CF_grammar.LRk.ruleAt G i = G.rules.get i

@[simp]

theorem CF_grammar.LRk.ruleAt_mem {T : Type} (G : CF_grammar T) (i : RuleIndex G) : ruleAt G i ∈ G.rules

@[reducible, inline]

abbrev CF_grammar.LRk.Position {T : Type} (G : CF_grammar T) (i : RuleIndex G) : Type

A dot position in a production, including the completed position just past the right-hand side.

Equations

• CF_grammar.LRk.Position G i = Fin ((CF_grammar.LRk.ruleAt G i).2.length + 1)

@[reducible, inline]

abbrev CF_grammar.LRk.Lookahead (T : Type) (k : ℕ) : Type

Exactly k symbols of terminal lookahead. none is the explicit end-of-input marker; after the first none, all semantically reachable lookaheads are also none. Keeping the ambient function type unrestricted makes finiteness immediate, while well-formedness is enforced by the semantic relations below.

Equations

• CF_grammar.LRk.Lookahead T k = (Fin k → Option T)

def CF_grammar.LRk.observe {T : Type} (k : ℕ) (w : List T) : Lookahead T k

Observe the first k terminals of a suffix, padding with the explicit EOF marker.

Equations

• CF_grammar.LRk.observe k w i = w[↑i]?

def CF_grammar.LRk.eofLookahead (T : Type) (k : ℕ) : Lookahead T k

The all-EOF lookahead.

Equations

• CF_grammar.LRk.eofLookahead T k x✝ = none

def CF_grammar.LRk.prependLookahead {T : Type} (k : ℕ) (z : List T) (u : Lookahead T k) : Lookahead T k

Prefix a finite terminal word to a padded lookahead.

Equations

• CF_grammar.LRk.prependLookahead k z u i = if h : ↑i < z.length then z[↑i]? else u ⟨↑i - z.length, ⋯⟩

@[simp]

theorem CF_grammar.LRk.observe_append {T : Type} (k : ℕ) (z s : List T) : observe k (z ++ s) = prependLookahead k z (observe k s)

@[reducible, inline]

abbrev CF_grammar.LRk.Item {T : Type} (G : CF_grammar T) (k : ℕ) : Type

A canonical LR item [A → α · β, u].

The first component identifies the production, the second its dot position, and the third the padded terminal lookahead.

Equations

• CF_grammar.LRk.Item G k = ((i : CF_grammar.LRk.RuleIndex G) × CF_grammar.LRk.Position G i × CF_grammar.LRk.Lookahead T k)

noncomputable instance CF_grammar.LRk.instFintypeItem {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Fintype (Item G k)

Equations

• CF_grammar.LRk.instFintypeItem G k = Sigma.instFintype

def CF_grammar.LRk.Item.rule {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : RuleIndex G

The production index of an item.

Equations

• i.rule = i.fst

def CF_grammar.LRk.Item.position {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : Position G i.rule

The dot position of an item.

Equations

• i.position = i.snd.1

def CF_grammar.LRk.Item.lookahead {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : Lookahead T k

The terminal lookahead of an item.

Equations

• i.lookahead = i.snd.2

def CF_grammar.LRk.Item.before {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : List (symbol T G.nt)

Symbols before the dot.

Equations

• i.before = List.take (↑i.position) (CF_grammar.LRk.ruleAt G i.rule).2

def CF_grammar.LRk.Item.after {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : List (symbol T G.nt)

Symbols at and after the dot.

Equations

• i.after = List.drop (↑i.position) (CF_grammar.LRk.ruleAt G i.rule).2

def CF_grammar.LRk.Item.next? {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : Option (symbol T G.nt)

The symbol immediately after the dot, if any.

Equations

• i.next? = (CF_grammar.LRk.ruleAt G i.rule).2[↑i.position]?

def CF_grammar.LRk.Item.Complete {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : Prop

An item is complete when its dot is just past the right-hand side.

Equations

• i.Complete = (↑i.position = (CF_grammar.LRk.ruleAt G i.rule).2.length)

def CF_grammar.LRk.Advances {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) (X : symbol T G.nt) (j : Item G k) : Prop

Relational dot advancement. A relational presentation avoids dependent casts between the position types while retaining a finite decidable relation.

Equations

• CF_grammar.LRk.Advances i X j = (j.rule = i.rule ∧ ↑j.position = ↑i.position + 1 ∧ i.next? = some X ∧ j.lookahead = i.lookahead)

def CF_grammar.LRk.Item.afterNext {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) : List (symbol T G.nt)

The right-hand suffix after the nonterminal immediately following an item's dot.

Equations

• i.afterNext = List.drop 1 i.after

def CF_grammar.LRk.CanFollow {T : Type} (G : CF_grammar T) (k : ℕ) (beta : List (symbol T G.nt)) (u v : Lookahead T k) : Prop

A lookahead v can follow a just-opened nonterminal when the remaining sentential suffix is beta and the enclosing item has lookahead u.

This semantic FIRST_k relation is deliberately stated with rightmost derivations. It is a finite decidable table by classical choice because its arguments range over the finite item universe.

Equations

• CF_grammar.LRk.CanFollow G k beta u v = ∃ (z : List T), G.DerivesRightmost beta (List.map symbol.terminal z) ∧ CF_grammar.LRk.prependLookahead k z u = v

def CF_grammar.LRk.ClosureStep {T : Type} (G : CF_grammar T) (k : ℕ) (i j : Item G k) : Prop

One epsilon-closure edge between canonical items.

Equations

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

noncomputable def CF_grammar.LRk.closure {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) : Finset (Item G k)

Epsilon closure of a finite item set.

Equations

• CF_grammar.LRk.closure G k I = {j : CF_grammar.LRk.Item G k | ∃ i ∈ I, Relation.ReflTransGen (CF_grammar.LRk.ClosureStep G k) i j}

@[simp]

theorem CF_grammar.LRk.mem_closure {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) (j : Item G k) : j ∈ closure G k I ↔ ∃ i ∈ I, Relation.ReflTransGen (ClosureStep G k) i j

theorem CF_grammar.LRk.subset_closure {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) : I ⊆ closure G k I

@[simp]

theorem CF_grammar.LRk.closure_closure {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) : closure G k (closure G k I) = closure G k I

noncomputable def CF_grammar.LRk.goto {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) (X : symbol T G.nt) : Finset (Item G k)

Canonical goto on one grammar symbol.

Equations

• CF_grammar.LRk.goto G k I X = {j : CF_grammar.LRk.Item G k | ∃ i ∈ CF_grammar.LRk.closure G k I, CF_grammar.LRk.Advances i X j}

@[simp]

theorem CF_grammar.LRk.mem_goto {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (I : Finset (Item G k)) (X : symbol T G.nt) (j : Item G k) : j ∈ goto G k I X ↔ ∃ i ∈ closure G k I, Advances i X j