Canonical compressed relations used by the bounded runner

The physical block layout remembers only that a finite relation denotes its concrete flag block. Completeness also needs the converse normalization fact: because relational composition is associative, every such provenance tree is equal to the canonical right-associated relation compressedFlags.

theorem IndexedGrammar.Aho.CFlag.Denotes.flags_ne_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {R : CFlag g} (h : Denotes g flags R) : flags ≠ []

A denoted compressed relation always represents a nonempty concrete block.

theorem IndexedGrammar.Aho.compressedFlags_append {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (f : g.flag) (fs : List g.flag) (h : g.flag) (hs : List g.flag) : compressedFlags g f (fs ++ h :: hs) = cflagComp g (compressedFlags g f fs) (compressedFlags g h hs)

Canonical compression distributes over concatenation of two nonempty flag blocks.

theorem IndexedGrammar.Aho.CFlag.Denotes.exists_eq_compressedFlags {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {R : CFlag g} (h : Denotes g flags R) : ∃ (f : g.flag) (rest : List g.flag), flags = f :: rest ∧ R = compressedFlags g f rest

Every provenance tree has a canonical nonempty flag-list presentation.

theorem IndexedGrammar.Aho.CFlag.Denotes.eq_compressedFlags {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {f : g.flag} {flags : List g.flag} {R : CFlag g} (h : Denotes g (f :: flags) R) : R = compressedFlags g f flags

Provenance determines the compressed relation uniquely.

Event-free prefixes are unary pop paths

theorem IndexedGrammar.Aho.NFParse.ConsumeRoute.noBinary_of_eventDepths_gt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {parse : g.NFParse A stack w} {k : ℕ} (route : NFParse.ConsumeRoute g parse k) (hevents : ∀ d ∈ parse.eventDepths, k < d) : route.NoBinary

If every productive event of a parse lies strictly below the occurrence selected by a route, that route crosses no binary node. This is the semantic reason an interval between two consecutive event cuts can be represented by one atomic compressed relation.

theorem IndexedGrammar.Aho.exists_popContinuation_of_eventFree_block_with_owners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {block suffix : List g.flag} {w : List T} (parse : g.NFParse A (block ++ suffix) w) {R : CFlag g} (hdenotes : CFlag.Denotes g block R) (hlast : parse.ConsumesAt (block.length - 1)) (hevents : ∀ d ∈ parse.eventDepths, block.length - 1 < d) : ∃ (continuation : PopContinuation block suffix parse R), continuation.rest.nodeCount < parse.nodeCount ∧ (∀ (j : ℕ), continuation.rest.ConsumesAt j ↔ parse.ConsumesAt (block.length + j)) ∧ (∀ (d : ℕ), d ∈ continuation.rest.eventDepths ↔ block.length + d ∈ parse.eventDepths) ∧ ∀ (d : ℕ), continuation.rest.eventOwnerNat d = parse.eventOwnerNat (block.length + d)

A whole first block with no event at or above its last flag has an atomic viable pop continuation. The result works for the relation physically stored by BlockLayout, not only for the syntactically canonical relation, because denotation provenance is unique.

structure IndexedGrammar.Aho.EventCompatible {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (blocks : List (List g.flag)) : Type

Every productive event of parse is aligned with a whole compressed-block boundary.

• boundary (d : ℕ) : d ∈ parse.eventDepths → BlockLayout.Boundary blocks d

Root-relative ghost schedule interfaces

def IndexedGrammar.Aho.scheduleTaskOfParse {T : Type} {g : IndexedGrammar T} {input : List T} {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (pre post : List T) (input_eq : input = pre ++ w ++ post) (mode : TaskMode parse) : ScheduleTask g input

Package an arbitrary concrete parse task at its exact input interval.

Equations

• IndexedGrammar.Aho.scheduleTaskOfParse parse pre post input_eq mode = { A := A, stack := stack, yield := w, parse := parse, pre := pre, post := post, input_eq := input_eq, mode := mode }

def IndexedGrammar.Aho.scheduleWordCursor {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (alpha word : List (ScheduleAtom g input)) : ScheduleCursor g input

Ghost analogue of wordConfig: focus the first continuation atom.

Equations

• IndexedGrammar.Aho.scheduleWordCursor alpha [] = { left := alpha ++ [IndexedGrammar.Aho.ScheduleAtom.dollar], focus := IndexedGrammar.Aho.ScheduleAtom.hash, right := [] }
• IndexedGrammar.Aho.scheduleWordCursor alpha (z :: zs) = { left := alpha ++ [IndexedGrammar.Aho.ScheduleAtom.dollar], focus := z, right := zs }

@[simp]

theorem IndexedGrammar.Aho.scheduleWordCursor_erase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (alpha word : List (ScheduleAtom g input)) : (scheduleWordCursor alpha word).erase = (wordConfig g 0 (List.map ScheduleAtom.workSym alpha) (List.map ScheduleAtom.workSym word)).work

def IndexedGrammar.Aho.scheduleStateOfCursor {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (inputPos : ℕ) (hpos : inputPos ≤ input.length) (cursor : ScheduleCursor g input) (invariant : ScheduleInvariant cursor) : ScheduleState g input

Build a scheduler state once interval arithmetic and the ownership invariant are known.

Equations

• IndexedGrammar.Aho.scheduleStateOfCursor inputPos hpos cursor invariant = { inputPos := inputPos, inputPos_le := hpos, cursor := cursor, invariant := invariant }

structure IndexedGrammar.Aho.IndexOwnerPool {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : Type

The reusable generic-owner bank, partitioned into labels present on persistent indices and labels still free. The bank has exactly 4|input| elements even though labels inhabit the larger Fin (6|input|) carrier used to keep them disjoint from semantic tickets.

• free : List (Fin (10 * input.length))
• all_nodup : (cursor.indexOwners ++ self.free).Nodup
• all_perm : (cursor.indexOwners ++ self.free).Perm (genericOwnerRange g input)

theorem IndexedGrammar.Aho.IndexOwnerPool.free_nodup {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) : pool.free.Nodup

theorem IndexedGrammar.Aho.IndexOwnerPool.free_disjoint {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) : cursor.indexOwners.Disjoint pool.free

theorem IndexedGrammar.Aho.IndexOwnerPool.mem_indices_or_free {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) (owner : Fin (10 * input.length)) (hgeneric : owner ∈ genericOwnerRange g input) : owner ∈ cursor.indexOwners ∨ owner ∈ pool.free

Every label in the generic owner universe is either present or remains free.

theorem IndexedGrammar.Aho.IndexOwnerPool.mem_free_of_not_mem_indices {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) {owner : Fin (10 * input.length)} (hgeneric : owner ∈ genericOwnerRange g input) (howner : owner ∉ cursor.indexOwners) : owner ∈ pool.free

An owner absent from the work tape is available in the exhaustive free pool.

theorem IndexedGrammar.Aho.IndexOwnerPool.mem_genericOwnerRange_of_mem_indices {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) {owner : Fin (10 * input.length)} (howner : owner ∈ cursor.indexOwners) : owner ∈ genericOwnerRange g input

Every persistent index owner comes from the generic pool universe.

theorem IndexedGrammar.Aho.IndexOwnerPool.mem_genericOwnerRange_of_mem_free {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) {owner : Fin (10 * input.length)} (howner : owner ∈ pool.free) : owner ∈ genericOwnerRange g input

Every free label also comes from the generic pool universe.

theorem IndexedGrammar.Aho.IndexOwnerPool.index_count_add_free_length {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) : cursor.indexOwners.length + pool.free.length = 6 * input.length

Exact conservation of the reusable bank.

theorem IndexedGrammar.Aho.IndexOwnerPool.index_count_le {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) : cursor.indexOwners.length ≤ 6 * input.length

The generic bank, rather than the larger ambient owner carrier, bounds persistent indices.

theorem IndexedGrammar.Aho.IndexOwnerPool.index_count_lt_of_free_ne_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) (hfree : pool.free ≠ []) : cursor.indexOwners.length < 6 * input.length

A free reusable label leaves strict room for one more persistent index.

theorem IndexedGrammar.Aho.IndexOwnerPool.exists_free_generic {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) (hfree : pool.free ≠ []) : ∃ owner ∈ pool.free, owner ∈ genericOwnerRange g input

A nonempty free suffix supplies a generic label directly, without attempting to allocate a semantic event ticket.

theorem IndexedGrammar.Aho.IndexOwnerPool.scratchOwner_not_mem_indices {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) (hinput : 0 < input.length) : ProductiveOwnerWindow.scratchOwner hinput ∉ cursor.indexOwners

Scratch is not a reusable generic label and therefore cannot occur on a persistent index described by this pool.

theorem IndexedGrammar.Aho.IndexOwnerPool.transientOwner_not_mem_indices {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (pool : IndexOwnerPool cursor) (hinput : 0 < input.length) : ProductiveOwnerWindow.transientOwner hinput ∉ cursor.indexOwners

Transient is likewise disjoint from every persistent owner described by the generic pool.

def IndexedGrammar.Aho.plainScheduleCursor {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (unused : ¬parse.ConsumesAt 0) (pre post : List T) (input_eq : input = pre ++ w ++ post) (alpha : List (ScheduleAtom g input)) (next : ScheduleAtom g input) (tail : List (ScheduleAtom g input)) : ScheduleCursor g input

Start cursor for a plain parse task.

Equations

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

def IndexedGrammar.Aho.liveScheduleCursor {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (used : parse.ConsumesAt 0) (pre post : List T) (input_eq : input = pre ++ w ++ post) (alpha word : List (ScheduleAtom g input)) : ScheduleCursor g input

Start cursor for a live parse task.

Equations

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