Block denotation for Aho's work tape

Compressed indices must be interpreted as separate visible stack blocks. Flags omitted by a plainPushSkip move are ghost gaps between those blocks: flattening the visible blocks loses the position of such a gap and makes plainPushUse followed by popPlain impossible to justify.

The continues bit is Aho's first/later distinction (IndexMark.later). A continuing block has no hidden gap after it and exposes another live block when popped. A first block may expose an arbitrary hidden gap and therefore returns to a plain nonterminal.

Visible blocks and hidden decorations

structure IndexedGrammar.Aho.BlockDenotation.VisibleBlock {T : Type} (g : IndexedGrammar T) : Type

Concrete ghost information denoted by one compressed-index token.

• flags : List g.flag
• continues : Bool

@[reducible, inline]

abbrev IndexedGrammar.Aho.BlockDenotation.VisibleStack {T : Type} (g : IndexedGrammar T) : Type

Visible block stack, nearest compressed token first.

Equations

• IndexedGrammar.Aho.BlockDenotation.VisibleStack g = List (IndexedGrammar.Aho.BlockDenotation.VisibleBlock g)

def IndexedGrammar.Aho.BlockDenotation.Decorates {T : Type} {g : IndexedGrammar T} : VisibleStack g → List g.flag → Prop

A plain nonterminal may have an arbitrary hidden gap before the first visible block and after every non-continuing block.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.BlockDenotation.Decorates [] x✝ = True

def IndexedGrammar.Aho.BlockDenotation.LiveDecorates {T : Type} {g : IndexedGrammar T} : VisibleStack g → List g.flag → Prop

A live nonterminal starts with the first visible block. Its following gap is controlled by that block's continues bit.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.BlockDenotation.LiveDecorates [] x✝ = False

theorem IndexedGrammar.Aho.BlockDenotation.Decorates.pushHidden {T : Type} {g : IndexedGrammar T} {blocks : VisibleStack g} {actual : List g.flag} (f : g.flag) (h : Decorates blocks actual) : Decorates blocks (f :: actual)

Add one unused flag to the leading hidden gap of a plain stack.

theorem IndexedGrammar.Aho.BlockDenotation.Decorates.pushFirst {T : Type} {g : IndexedGrammar T} {blocks : VisibleStack g} {actual : List g.flag} (f : g.flag) (h : Decorates blocks actual) : LiveDecorates ({ flags := [f], continues := false } :: blocks) (f :: actual)

A first used push turns a decorated plain stack into a live stack with a fresh first block.

theorem IndexedGrammar.Aho.BlockDenotation.LiveDecorates.toDecorates {T : Type} {g : IndexedGrammar T} {blocks : VisibleStack g} {actual : List g.flag} (h : LiveDecorates blocks actual) : Decorates blocks actual

Forget that the first visible block is forced to start at the top of the actual stack.

theorem IndexedGrammar.Aho.BlockDenotation.LiveDecorates.pushLater {T : Type} {g : IndexedGrammar T} {blocks : VisibleStack g} {actual : List g.flag} (f : g.flag) (h : LiveDecorates blocks actual) : LiveDecorates ({ flags := [f], continues := true } :: blocks) (f :: actual)

A later used push creates a fresh continuing block above a live stack.

theorem IndexedGrammar.Aho.BlockDenotation.LiveDecorates.pushCompress {T : Type} {g : IndexedGrammar T} {old : VisibleBlock g} {blocks : VisibleStack g} {actual : List g.flag} (f : g.flag) (h : LiveDecorates (old :: blocks) actual) : LiveDecorates ({ flags := f :: old.flags, continues := old.continues } :: blocks) (f :: actual)

Compressing a new flag into the current visible block preserves its continuation bit and all hidden gaps below it.

theorem IndexedGrammar.Aho.BlockDenotation.LiveDecorates.popPlain {T : Type} {g : IndexedGrammar T} {block : VisibleBlock g} {blocks : VisibleStack g} {actual : List g.flag} (h : LiveDecorates (block :: blocks) actual) : ∃ (rest : List g.flag), actual = block.flags ++ rest ∧ Decorates blocks rest

Pop a first/non-continuing block. The remainder is a plain decorated stack.

theorem IndexedGrammar.Aho.BlockDenotation.LiveDecorates.popLive {T : Type} {g : IndexedGrammar T} {block : VisibleBlock g} {blocks : VisibleStack g} {actual : List g.flag} (hcontinues : block.continues = true) (h : LiveDecorates (block :: blocks) actual) : ∃ (rest : List g.flag), actual = block.flags ++ rest ∧ LiveDecorates blocks rest

Pop a continuing block. Aho's later=true guard exposes a live decorated tail.

Delimiter-free segments

inductive IndexedGrammar.Aho.BlockDenotation.SegmentRep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : VisibleStack g → List (WorkSym g) → VisibleStack g → List g.ISym → Prop

Right-to-left denotation of one delimiter-free segment. Visible indices build a block stack; each nonterminal independently chooses the hidden gaps permitted by its plain/live decoration.

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (inherited : VisibleStack g) : SegmentRep g inherited [] inherited []
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} (a : T) (tail : SegmentRep g inherited xs stack form) : SegmentRep g inherited (WorkSym.terminal a :: xs) stack (ISym.terminal a :: form)
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} (A : g.nt) (actual : List g.flag) (decorates : Decorates stack actual) (tail : SegmentRep g inherited xs stack form) : SegmentRep g inherited (WorkSym.plain A :: xs) stack (ISym.indexed A actual :: form)
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} (A : g.nt) (actual : List g.flag) (decorates : LiveDecorates stack actual) (tail : SegmentRep g inherited xs stack form) : SegmentRep g inherited (WorkSym.live A :: xs) stack (ISym.indexed A actual :: form)
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} (d : IndexMark) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) (tail : SegmentRep g inherited xs stack form) : SegmentRep g inherited (WorkSym.index R d :: xs) ({ flags := flags, continues := d.later } :: stack) form

@[simp]

theorem IndexedGrammar.Aho.BlockDenotation.segmentRep_nil_iff {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {inherited before : VisibleStack g} {form : List g.ISym} : SegmentRep g inherited [] before form ↔ before = inherited ∧ form = []

theorem IndexedGrammar.Aho.BlockDenotation.segmentRep_append_iff {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (xs ys : List (WorkSym g)) {inherited before : VisibleStack g} {form : List g.ISym} : SegmentRep g inherited (xs ++ ys) before form ↔ ∃ (middle : VisibleStack g) (leftForm : List g.ISym) (rightForm : List g.ISym), SegmentRep g inherited ys middle rightForm ∧ SegmentRep g middle xs before leftForm ∧ form = leftForm ++ rightForm

Splitting a segment exposes the intermediate visible block stack and splits its form.

theorem IndexedGrammar.Aho.BlockDenotation.SegmentRep.stack_eq_of_indexFree {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited before : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} (hfree : IndexFree xs) (h : SegmentRep g inherited xs before form) : before = inherited

Index-free segments preserve the visible inherited block stack.

theorem IndexedGrammar.Aho.BlockDenotation.SegmentRep.changeIndexMark {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : VisibleStack g} {xs : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d e : IndexMark} (hlater : d.later = e.later) (h : SegmentRep g inherited (WorkSym.index R d :: xs) stack form) : SegmentRep g inherited (WorkSym.index R e :: xs) stack form

Changing an index mark without changing its first/later bit preserves the denotation.

theorem IndexedGrammar.Aho.BlockDenotation.IndexMark.later_markUsed (d : IndexMark) : d.markUsed.later = d.later

Nested frame layout

@[reducible, inline]

abbrev IndexedGrammar.Aho.BlockDenotation.FrameBoundary {T : Type} (g : IndexedGrammar T) : Type

Equations

• IndexedGrammar.Aho.BlockDenotation.FrameBoundary g = (List (IndexedGrammar.Aho.WorkSym g) × List (IndexedGrammar.Aho.WorkSym g))

def IndexedGrammar.Aho.BlockDenotation.frameLeft {T : Type} (g : IndexedGrammar T) : List (FrameBoundary g) → List (WorkSym g)

Equations

• IndexedGrammar.Aho.BlockDenotation.frameLeft g [] = [IndexedGrammar.Aho.WorkSym.dollar]
• IndexedGrammar.Aho.BlockDenotation.frameLeft g ((pending, snd) :: frames) = IndexedGrammar.Aho.WorkSym.dollar :: pending ++ IndexedGrammar.Aho.BlockDenotation.frameLeft g frames

def IndexedGrammar.Aho.BlockDenotation.frameTail {T : Type} (g : IndexedGrammar T) (frames : List (FrameBoundary g)) : List (WorkSym g)

Equations

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

def IndexedGrammar.Aho.BlockDenotation.CursorLayout {T : Type} (g : IndexedGrammar T) (frames : List (FrameBoundary g)) (current : List (WorkSym g)) (cursor : WorkCursor g) : Prop

Equations

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

inductive IndexedGrammar.Aho.BlockDenotation.NestedRep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : VisibleStack g → List (FrameBoundary g) → List (WorkSym g) → List g.ISym → Prop

• current {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited before : VisibleStack g} {current : List (WorkSym g)} {form : List g.ISym} (segment : SegmentRep g inherited current before form) : NestedRep g inherited [] current form
• frame {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited tailStack pendingStack : VisibleStack g} {pending suffix current : List (WorkSym g)} {frames : List (FrameBoundary g)} {suffixForm pendingForm innerForm : List g.ISym} (suffixRep : SegmentRep g inherited suffix tailStack suffixForm) (pendingRep : SegmentRep g tailStack pending pendingStack pendingForm) (pendingEndsIndex : ∃ (beta : List (WorkSym g)) (R : CFlag g) (d : IndexMark), pending = beta ++ [WorkSym.index R d]) (innerRep : NestedRep g tailStack frames current innerForm) : NestedRep g inherited ((pending, suffix) :: frames) current (innerForm ++ pendingForm ++ suffixForm)

def IndexedGrammar.Aho.BlockDenotation.WorkCursor.Represents {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (cursor : WorkCursor g) (form : List g.ISym) : Prop

Equations

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

def IndexedGrammar.Aho.BlockDenotation.Config.Represents {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (c : Config g) (form : List g.ISym) : Prop

Equations

• IndexedGrammar.Aho.BlockDenotation.Config.Represents c form = IndexedGrammar.Aho.BlockDenotation.WorkCursor.Represents c.work form

Boundary configurations

theorem IndexedGrammar.Aho.BlockDenotation.initialConfig_represents {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : Config.Represents (initialConfig g) [ISym.indexed g.initial []]

theorem IndexedGrammar.Aho.BlockDenotation.finalConfig_represents {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (n : ℕ) : Config.Represents (finalConfig g n) []