Boundary row scans

Exact finite scans recognizing the initialized and accepting padded-row formats.

Exact finite scans for initialization and final rows

inductive IndexedGrammar.Aho.BoundaryScanState : Type

Three states suffice for the fixed first-block / blank-tail row formats.

• first : BoundaryScanState
• tail : BoundaryScanState
• dead : BoundaryScanState

instance IndexedGrammar.Aho.instDecidableEqBoundaryScanState : DecidableEq BoundaryScanState

Equations

• IndexedGrammar.Aho.instDecidableEqBoundaryScanState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance IndexedGrammar.Aho.instFintypeBoundaryScanState : Fintype BoundaryScanState

Equations

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

def IndexedGrammar.Aho.initialFirstCell {T : Type} (g : IndexedGrammar T) (a : T) : RowCell g

The canonical initialized cell at the first input position.

Equations

• IndexedGrammar.Aho.initialFirstCell g a = IndexedGrammar.Aho.RowCell.run { input := a, consumed := false, block := IndexedGrammar.Aho.initialBlock g }

def IndexedGrammar.Aho.initialTailCell {T : Type} (g : IndexedGrammar T) (a : T) : RowCell g

A canonical blank-tail initialized cell.

Equations

• IndexedGrammar.Aho.initialTailCell g a = IndexedGrammar.Aho.RowCell.run { input := a, consumed := false, block := IndexedGrammar.Aho.blankBlock g }

def IndexedGrammar.Aho.finalFirstCell {T : Type} (g : IndexedGrammar T) (a : T) : RowCell g

The canonical final cell at the first input position.

Equations

• IndexedGrammar.Aho.finalFirstCell g a = IndexedGrammar.Aho.RowCell.run { input := a, consumed := true, block := IndexedGrammar.Aho.finalBlock g }

def IndexedGrammar.Aho.finalTailCell {T : Type} (g : IndexedGrammar T) (a : T) : RowCell g

A canonical blank-tail final cell.

Equations

• IndexedGrammar.Aho.finalTailCell g a = IndexedGrammar.Aho.RowCell.run { input := a, consumed := true, block := IndexedGrammar.Aho.blankBlock g }

noncomputable def IndexedGrammar.Aho.initScanCell {T : Type} (g : IndexedGrammar T) : BoundaryScanState → RowCell g → RowCell g → BoundaryScanState

Cell transition for the exact synchronized initialization scan.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.initScanCell g state old new = IndexedGrammar.Aho.BoundaryScanState.dead

noncomputable def IndexedGrammar.Aho.evalInitScan {T : Type} (g : IndexedGrammar T) : BoundaryScanState → List (RowCell g) → List (RowCell g) → BoundaryScanState

Run the synchronized initialization scan; unequal row lengths reject.

Equations

• IndexedGrammar.Aho.evalInitScan g x✝ [] [] = x✝
• IndexedGrammar.Aho.evalInitScan g x✝ (old :: olds) (new :: news) = IndexedGrammar.Aho.evalInitScan g (IndexedGrammar.Aho.initScanCell g x✝ old new) olds news
• IndexedGrammar.Aho.evalInitScan g x✝² x✝¹ x✝ = IndexedGrammar.Aho.BoundaryScanState.dead

noncomputable def IndexedGrammar.Aho.finalScanCell {T : Type} (g : IndexedGrammar T) : BoundaryScanState → RowCell g → BoundaryScanState

Cell transition for the exact regular final-row scan.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.finalScanCell g state cell = IndexedGrammar.Aho.BoundaryScanState.dead

noncomputable def IndexedGrammar.Aho.evalFinalScan {T : Type} (g : IndexedGrammar T) : BoundaryScanState → List (RowCell g) → BoundaryScanState

Run the final-row scan.

Equations

• IndexedGrammar.Aho.evalFinalScan g x✝ [] = x✝
• IndexedGrammar.Aho.evalFinalScan g x✝ (cell :: row) = IndexedGrammar.Aho.evalFinalScan g (IndexedGrammar.Aho.finalScanCell g x✝ cell) row

theorem IndexedGrammar.Aho.evalInitScan_iff_paddedInitStep {T : Type} (g : IndexedGrammar T) (old new : List (RowCell g)) : evalInitScan g BoundaryScanState.first old new = BoundaryScanState.tail ↔ PaddedInitStep g old new

The initialization scanner recognizes exactly PaddedInitStep.

theorem IndexedGrammar.Aho.evalFinalScan_iff_finalRow {T : Type} (g : IndexedGrammar T) (row : List (RowCell g)) : evalFinalScan g BoundaryScanState.first row = BoundaryScanState.tail ↔ FinalRow g row

The final scanner recognizes exactly FinalRow.