Plain-mode compressed scheduler

Plain tasks consume no inherited stack occurrence. Their binary, irrelevant-push, and terminal moves only rearrange terminal-owned payloads; a relevant push temporarily allocates one productive-event owner and delegates to copy-on-write overlay execution.

@[simp]

theorem IndexedGrammar.Aho.scheduleTaskOfParse_owner_val {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) : ↑(scheduleTaskOfParse parse pre post input_eq mode).owner = pre.length

def IndexedGrammar.Aho.IndexOwnerPool.transport {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {old new : ScheduleCursor g input} (pool : IndexOwnerPool old) (hindices : new.indexOwners = old.indexOwners) : IndexOwnerPool new

Transport a free-owner pool across a cursor change which preserves persistent indices.

Equations

• pool.transport hindices = { free := pool.free, all_nodup := ⋯, all_perm := ⋯ }

@[simp]

theorem IndexedGrammar.Aho.IndexOwnerPool.transport_free {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {old new : ScheduleCursor g input} (pool : IndexOwnerPool old) (hindices : new.indexOwners = old.indexOwners) : (pool.transport hindices).free = pool.free

theorem IndexedGrammar.Aho.plainScheduleRun_terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) : PlainScheduleRun (NFParse.terminal hr hlhs hc hrhs)

Run a terminal constructor in ordinary plain mode.

theorem IndexedGrammar.Aho.plainScheduleRun_binary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B C : g.nt} {stack : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (leftParse : g.NFParse B stack u) (rightParse : g.NFParse C stack v) (leftRuns : OrdinaryScheduleRuns leftParse) (rightRuns : OrdinaryScheduleRuns rightParse) : PlainScheduleRun (NFParse.binary hr hlhs hc hrhs leftParse rightParse)

Split a plain binary task into its two ordered plain children and run them sequentially.

theorem IndexedGrammar.Aho.plainScheduleRun_pushSkip {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (restUnused : ¬rest.ConsumesAt 0) (restRuns : OrdinaryScheduleRuns rest) : PlainScheduleRun (NFParse.push hr hlhs hc hrhs rest)

An irrelevant push merely replaces the plain task by its unary child while preserving the strict parking bound through the unchanged productive window.

theorem IndexedGrammar.Aho.plainScheduleRun_pushUse_of_pool_nonempty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (restUsed : rest.ConsumesAt 0) (restOverlay : OverlayScheduleRun rest) : PlainScheduleRun (NFParse.push hr hlhs hc hrhs rest)

A relevant push allocates the head of the free owner pool and delegates to overlay mode, while preserving the strict parking bound through the nonparking ticket rotation.

theorem IndexedGrammar.Aho.plainScheduleRun_pop_false {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (rest : g.NFParse B stack w) : PlainScheduleRun (NFParse.pop hr hlhs hc hrhs rest)

A concrete pop can never occur in plain mode because it consumes the top inherited flag.

theorem IndexedGrammar.Aho.plainScheduleRun_of_smaller {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (ordinaryIH : ∀ {B : g.nt} {stack' : List g.flag} {yield : List T} (q : g.NFParse B stack' yield), q.nodeCount < parse.nodeCount → OrdinaryScheduleRuns q) (overlayIH : ∀ {B : g.nt} {stack' : List g.flag} {yield : List T} (q : g.NFParse B stack' yield), q.nodeCount < parse.nodeCount → OverlayScheduleRun q) : PlainScheduleRun parse

Ordinary plain mode follows one grammar constructor and delegates every smaller parse task to the ordinary/overlay mutual induction hypotheses.