Finite Stack Summaries for Regular Lookahead

Regular lookahead on a pushdown stack can be implemented by storing, with each stack symbol, the DFA transition summary of the suffix below that symbol. If a DFA state type is finite, the summary type σ → σ is finite, so these annotations keep the stack alphabet finite.

def DFA.stackSummary {S σ : Type} (D : DFA S σ) (γ : List S) : σ → σ

The transition function induced by reading an entire stack suffix.

Equations

• D.stackSummary γ s = D.evalFrom s γ

@[simp]

theorem DFA.stackSummary_nil {S σ : Type} (D : DFA S σ) : D.stackSummary [] = id

theorem DFA.stackSummary_append {S σ : Type} (D : DFA S σ) (γ δ : List S) : D.stackSummary (γ ++ δ) = D.stackSummary δ ∘ D.stackSummary γ

def DFA.summaryAbove {S σ : Type} (D : DFA S σ) (below : σ → σ) (γ : List S) : σ → σ

The summary of a block γ placed above a suffix whose summary is below.

Equations

• D.summaryAbove below γ = below ∘ D.stackSummary γ

@[simp]

theorem DFA.summaryAbove_nil {S σ : Type} (D : DFA S σ) (below : σ → σ) : D.summaryAbove below [] = below

theorem DFA.summaryAbove_cons {S σ : Type} (D : DFA S σ) (below : σ → σ) (Z : S) (γ : List S) : D.summaryAbove below (Z :: γ) = D.summaryAbove (D.summaryAbove below γ) [Z]

def DFA.annotateAbove {S σ : Type} (D : DFA S σ) (below : σ → σ) : List S → List (S × (σ → σ))

Annotate a block of stack symbols to be placed above a suffix with known summary. The annotation stored at each symbol is the summary of the suffix below it.

Equations

• D.annotateAbove below [] = []
• D.annotateAbove below (Z :: γ) = (Z, D.summaryAbove below γ) :: D.annotateAbove below γ

@[simp]

theorem DFA.annotateAbove_nil {S σ : Type} (D : DFA S σ) (below : σ → σ) : D.annotateAbove below [] = []

@[simp]

theorem DFA.annotateAbove_cons {S σ : Type} (D : DFA S σ) (below : σ → σ) (Z : S) (γ : List S) : D.annotateAbove below (Z :: γ) = (Z, D.summaryAbove below γ) :: D.annotateAbove below γ

theorem DFA.annotateAbove_map_fst {S σ : Type} (D : DFA S σ) (below : σ → σ) (γ : List S) : List.map Prod.fst (D.annotateAbove below γ) = γ

theorem DFA.annotateAbove_head?_tail_summary {S σ : Type} (D : DFA S σ) (below : σ → σ) (Z : S) (γ : List S) : (D.annotateAbove below (Z :: γ)).head? = some (Z, D.summaryAbove below γ)

The summary stored at the top of a nonempty annotated block is the summary of the block below that top symbol, together with the external suffix summary.