theorem
Regex.VM.εClosure.pushNext.epsilonFin
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{state' : Fin nfa.nodes.size}
(hn : node = NFA.Node.epsilon ↑state')
:
theorem
Regex.VM.εClosure.pushNext.epsilon
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{state' : ℕ}
(hn : node = NFA.Node.epsilon state')
:
theorem
Regex.VM.εClosure.pushNext.splitFin
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{state₁ state₂ : Fin nfa.nodes.size}
(hn : node = NFA.Node.split ↑state₁ ↑state₂)
:
theorem
Regex.VM.εClosure.pushNext.split
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{state₁ state₂ : ℕ}
(hn : node = NFA.Node.split state₁ state₂)
:
theorem
Regex.VM.εClosure.pushNext.save
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{offset state' : ℕ}
(hn : node = NFA.Node.save offset state')
:
theorem
Regex.VM.εClosure.pushNext.anchor_posFin
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{a : Data.Anchor}
{state' : Fin nfa.nodes.size}
(hn : node = NFA.Node.anchor a ↑state')
(ht : Data.Anchor.test it a = true)
:
theorem
Regex.VM.εClosure.pushNext.anchor_pos
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{a : Data.Anchor}
{state' : ℕ}
(hn : node = NFA.Node.anchor a state')
(ht : Data.Anchor.test it a = true)
:
theorem
Regex.VM.εClosure.pushNext.anchor_negFin
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{a : Data.Anchor}
{state' : Fin nfa.nodes.size}
(hn : node = NFA.Node.anchor a ↑state')
(ht : ¬Data.Anchor.test it a = true)
:
theorem
Regex.VM.εClosure.pushNext.anchor_neg
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{a : Data.Anchor}
{state' : ℕ}
(hn : node = NFA.Node.anchor a state')
(ht : ¬Data.Anchor.test it a = true)
:
theorem
Regex.VM.εClosure.pushNext.done
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
(hn : node = NFA.Node.done)
:
theorem
Regex.VM.εClosure.pushNext.fail
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
(hn : node = NFA.Node.fail)
:
theorem
Regex.VM.εClosure.pushNext.char
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{c : Char}
{state' : ℕ}
(hn : node = NFA.Node.char c state')
:
theorem
Regex.VM.εClosure.pushNext.sparse
{σ : Strategy}
{nfa : NFA}
{it : String.Iterator}
{node : NFA.Node}
{inBounds : node.inBounds nfa.nodes.size}
{update : σ.Update}
{stack : εStack σ nfa}
{cs : Data.Classes}
{state' : ℕ}
(hn : node = NFA.Node.sparse cs state')
:
theorem
Regex.VM.εClosure.pushNext.fun_cases'
(σ : Strategy)
(nfa : NFA)
(it : String.Iterator)
{motive : (node : NFA.Node) → node.inBounds nfa.nodes.size → σ.Update → εStack σ nfa → Prop}
(epsilon :
∀ (update : σ.Update) (stack : εStack σ nfa) (state' : ℕ)
(inBounds : (NFA.Node.epsilon state').inBounds nfa.nodes.size),
motive (NFA.Node.epsilon state') inBounds update stack)
(split :
∀ (update : σ.Update) (stack : εStack σ nfa) (state₁ state₂ : ℕ)
(inBounds : (NFA.Node.split state₁ state₂).inBounds nfa.nodes.size),
motive (NFA.Node.split state₁ state₂) inBounds update stack)
(save :
∀ (update : σ.Update) (stack : εStack σ nfa) (offset state' : ℕ)
(inBounds : (NFA.Node.save offset state').inBounds nfa.nodes.size),
motive (NFA.Node.save offset state') inBounds update stack)
(anchor_pos :
∀ (update : σ.Update) (stack : εStack σ nfa) (a : Data.Anchor) (state' : ℕ)
(inBounds : (NFA.Node.anchor a state').inBounds nfa.nodes.size),
Data.Anchor.test it a = true → motive (NFA.Node.anchor a state') inBounds update stack)
(anchor_neg :
∀ (update : σ.Update) (stack : εStack σ nfa) (a : Data.Anchor) (state' : ℕ)
(inBounds : (NFA.Node.anchor a state').inBounds nfa.nodes.size),
¬Data.Anchor.test it a = true → motive (NFA.Node.anchor a state') inBounds update stack)
(done :
∀ (update : σ.Update) (stack : εStack σ nfa) (inBounds : NFA.Node.done.inBounds nfa.nodes.size),
motive NFA.Node.done inBounds update stack)
(fail :
∀ (update : σ.Update) (stack : εStack σ nfa) (inBounds : NFA.Node.fail.inBounds nfa.nodes.size),
motive NFA.Node.fail inBounds update stack)
(char :
∀ (update : σ.Update) (stack : εStack σ nfa) (c : Char) (state' : ℕ)
(inBounds : (NFA.Node.char c state').inBounds nfa.nodes.size),
motive (NFA.Node.char c state') inBounds update stack)
(sparse :
∀ (update : σ.Update) (stack : εStack σ nfa) (cs : Data.Classes) (state' : ℕ)
(inBounds : (NFA.Node.sparse cs state').inBounds nfa.nodes.size),
motive (NFA.Node.sparse cs state') inBounds update stack)
(node : NFA.Node)
(inBounds : node.inBounds nfa.nodes.size)
(update : σ.Update)
(stack : εStack σ nfa)
:
motive node inBounds update stack
theorem
Regex.VM.εClosure.induct'
(σ : Strategy)
(nfa : NFA)
(wf : nfa.WellFormed)
(it : String.Iterator)
(motive : Option σ.Update → SearchState σ nfa → εStack σ nfa → Prop)
(base : ∀ (matched : Option σ.Update) (next : SearchState σ nfa), motive matched next [])
(visited :
∀ (matched : Option σ.Update) (next : SearchState σ nfa) (update : σ.Update) (state : Fin nfa.nodes.size)
(stack' : εStack σ nfa),
state ∈ next.states → motive matched next stack' → motive matched next ((update, state) :: stack'))
(not_visited :
∀ (matched : Option σ.Update) (next : SearchState σ nfa) (update : σ.Update) (state : Fin nfa.nodes.size)
(stack' : εStack σ nfa),
state ∉ next.states →
let node := nfa[state];
let matched' := if node = NFA.Node.done then matched <|> some update else matched;
let states' := next.states.insert state;
let updates' := if writeUpdate node = true then next.updates.set (↑state) update ⋯ else next.updates;
motive matched' { states := states', updates := updates' } (pushNext σ nfa it node ⋯ update stack') →
motive matched next ((update, state) :: stack'))
(matched : Option σ.Update)
(next : SearchState σ nfa)
(stack : εStack σ nfa)
:
motive matched next stack
theorem
Regex.VM.εClosure.base
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{next : SearchState σ nfa}
:
theorem
Regex.VM.εClosure.visited
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{stack' : εStack σ nfa}
(hmem : state ∈ next.states)
:
theorem
Regex.VM.εClosure.not_visited
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{stack' : εStack σ nfa}
(hmem : state ∉ next.states)
:
εClosure σ nfa wf it matched next ((update, state) :: stack') = εClosure σ nfa wf it (if nfa[state] = NFA.Node.done then matched <|> some update else matched)
{ states := next.states.insert state,
updates := if writeUpdate nfa[state] = true then next.updates.set (↑state) update ⋯ else next.updates }
(pushNext σ nfa it nfa[state] ⋯ update stack')