Initial item of an augmented grammar

The fresh-start rule is the head of the augmented grammar's rule list. This file records its finite rule index and the canonical item [S' -> . S, EOF^k], and proves the semantic validity of the initial item closure.

def CF_grammar.LRk.startRuleIndex {T : Type} (G : CF_grammar T) : RuleIndex G.augment

The rule-list index of the distinguished augmentation rule.

Equations

• CF_grammar.LRk.startRuleIndex G = ⟨0, ⋯⟩

@[simp]

theorem CF_grammar.LRk.ruleAt_startRuleIndex {T : Type} (G : CF_grammar T) : ruleAt G.augment (startRuleIndex G) = G.augmentStartRule

def CF_grammar.LRk.startItem {T : Type} (G : CF_grammar T) (k : ℕ) : Item G.augment k

The canonical kernel item [S' -> . S, EOF^k].

Equations

• CF_grammar.LRk.startItem G k = ⟨CF_grammar.LRk.startRuleIndex G, (⟨0, ⋯⟩, CF_grammar.LRk.eofLookahead T k)⟩

@[simp]

theorem CF_grammar.LRk.startItem_rule {T : Type} (G : CF_grammar T) (k : ℕ) : (startItem G k).rule = startRuleIndex G

@[simp]

theorem CF_grammar.LRk.startItem_position {T : Type} (G : CF_grammar T) (k : ℕ) : ↑(startItem G k).position = 0

@[simp]

theorem CF_grammar.LRk.startItem_lookahead {T : Type} (G : CF_grammar T) (k : ℕ) : (startItem G k).lookahead = eofLookahead T k

@[simp]

theorem CF_grammar.LRk.startItem_before {T : Type} (G : CF_grammar T) (k : ℕ) : (startItem G k).before = []

@[simp]

theorem CF_grammar.LRk.startItem_next {T : Type} (G : CF_grammar T) (k : ℕ) : (startItem G k).next? = some (symbol.nonterminal (some G.initial))

@[simp]

theorem CF_grammar.LRk.observe_nil {T : Type} (k : ℕ) : observe k [] = eofLookahead T k

theorem CF_grammar.LRk.startItem_valid {T : Type} (G : CF_grammar T) (k : ℕ) : Valid G.augment k [] (startItem G k)

The fresh-start item is semantically valid before scanning any grammar symbol.

def CF_grammar.LRk.startKernel {T : Type} (G : CF_grammar T) (k : ℕ) : Finset (Item G.augment k)

The raw kernel of the canonical viable-prefix automaton.

Equations

• CF_grammar.LRk.startKernel G k = {CF_grammar.LRk.startItem G k}

theorem CF_grammar.LRk.startClosure_valid {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) {i : Item G.augment k} (hi : i ∈ closure G.augment k (startKernel G k)) : Valid G.augment k [] i

Every item in the epsilon closure of the start kernel is valid at the empty prefix.