def
Regex.VM.SearchState.materialize
{nfa : NFA}
{bufferSize : ℕ}
(stateH : SearchState HistoryStrategy nfa)
:
SearchState (BufferStrategy bufferSize) nfa
Equations
- stateH.materialize = { states := stateH.states, updates := Vector.map (Regex.Strategy.materializeUpdates bufferSize) stateH.updates }
Instances For
@[simp]
theorem
Regex.VM.SearchState.materialize_states
{nfa : NFA}
{bufferSize : ℕ}
{stateH : SearchState HistoryStrategy nfa}
:
def
Regex.VM.εStack.materialize
{nfa : NFA}
{bufferSize : ℕ}
(stackH : εStack HistoryStrategy nfa)
:
εStack (BufferStrategy bufferSize) nfa
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem
Regex.VM.εStack.materialize.cons
{nfa : NFA}
{bufferSize : ℕ}
{stackH : εStack HistoryStrategy nfa}
{entry : HistoryStrategy.Update × Fin nfa.nodes.size}
:
materialize (entry :: stackH) = (Strategy.materializeUpdates bufferSize entry.1, entry.2) :: stackH.materialize
def
Regex.VM.materializeResult
{nfa : NFA}
{bufferSize : ℕ}
(resultH : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
:
Equations
- Regex.VM.materializeResult resultH = (Option.map (Regex.Strategy.materializeUpdates bufferSize) resultH.1, resultH.2.materialize)
Instances For
theorem
Regex.VM.εClosure.pushNext.refines
{nfa : NFA}
{bufferSize : ℕ}
{it : String.Iterator}
{stackH : εStack HistoryStrategy nfa}
{stackB : εStack (BufferStrategy bufferSize) nfa}
{state : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
{buffer : Vector (Option String.Pos) bufferSize}
(wf : nfa.WellFormed)
(h₁ : Strategy.materializeUpdates bufferSize update = buffer)
(h₂ : stackH.materialize = stackB)
:
(pushNext HistoryStrategy nfa it nfa[state] ⋯ update stackH).materialize = pushNext (BufferStrategy bufferSize) nfa it nfa[state] ⋯ buffer stackB
theorem
Regex.VM.εClosure.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{matchedH : Option (List (ℕ × String.Pos))}
{matchedB : Option (Buffer bufferSize)}
{nextH : SearchState HistoryStrategy nfa}
{nextB : SearchState (BufferStrategy bufferSize) nfa}
{stackH : εStack HistoryStrategy nfa}
{stackB : εStack (BufferStrategy bufferSize) nfa}
(resultB : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(resultH : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : εClosure (BufferStrategy bufferSize) nfa wf it matchedB nextB stackB = resultB)
(h' : εClosure HistoryStrategy nfa wf it matchedH nextH stackH = resultH)
(refMatched : Option.map (Strategy.materializeUpdates bufferSize) matchedH = matchedB)
(refState : nextH.materialize = nextB)
(refStack : stackH.materialize = stackB)
:
theorem
Regex.VM.stepChar.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{nextH : SearchState HistoryStrategy nfa}
{nextB : SearchState (BufferStrategy bufferSize) nfa}
{currentUpdatesH : Vector HistoryStrategy.Update nfa.nodes.size}
{currentUpdatesB : Vector (BufferStrategy bufferSize).Update nfa.nodes.size}
{state : Fin nfa.nodes.size}
(resultB : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(resultH : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : stepChar (BufferStrategy bufferSize) nfa wf it currentUpdatesB nextB state = resultB)
(h' : stepChar HistoryStrategy nfa wf it currentUpdatesH nextH state = resultH)
(refUpdates : Vector.map (Strategy.materializeUpdates bufferSize) currentUpdatesH = currentUpdatesB)
(refState : nextH.materialize = nextB)
:
theorem
Regex.VM.eachStepChar.go.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{nextH : SearchState HistoryStrategy nfa}
{nextB : SearchState (BufferStrategy bufferSize) nfa}
{currentH : SearchState HistoryStrategy nfa}
{currentB : SearchState (BufferStrategy bufferSize) nfa}
{i : ℕ}
{hleB : i ≤ currentB.states.count}
{hleH : i ≤ currentH.states.count}
(resultB : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(resultH : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : go (BufferStrategy bufferSize) nfa wf it currentB i hleB nextB = resultB)
(h' : go HistoryStrategy nfa wf it currentH i hleH nextH = resultH)
(refCurrent : currentH.materialize = currentB)
(refNext : nextH.materialize = nextB)
:
theorem
Regex.VM.eachStepChar.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{nextH : SearchState HistoryStrategy nfa}
{nextB : SearchState (BufferStrategy bufferSize) nfa}
{currentH : SearchState HistoryStrategy nfa}
{currentB : SearchState (BufferStrategy bufferSize) nfa}
(resultB : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(resultH : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : eachStepChar (BufferStrategy bufferSize) nfa wf it currentB nextB = resultB)
(h' : eachStepChar HistoryStrategy nfa wf it currentH nextH = resultH)
(refCurrent : currentH.materialize = currentB)
(refNext : nextH.materialize = nextB)
:
theorem
Regex.VM.captureNext.go.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{matchedH : Option (List (ℕ × String.Pos))}
{matchedB : Option (Buffer bufferSize)}
{nextH : SearchState HistoryStrategy nfa}
{nextB : SearchState (BufferStrategy bufferSize) nfa}
{currentH : SearchState HistoryStrategy nfa}
{currentB : SearchState (BufferStrategy bufferSize) nfa}
{resultB : Option (BufferStrategy bufferSize).Update}
{resultH : Option HistoryStrategy.Update}
(h : go (BufferStrategy bufferSize) nfa wf it matchedB currentB nextB = resultB)
(h' : go HistoryStrategy nfa wf it matchedH currentH nextH = resultH)
(refMatched : Option.map (Strategy.materializeUpdates bufferSize) matchedH = matchedB)
(refCurrent : currentH.materialize = currentB)
(refNext : nextH.materialize = nextB)
:
theorem
Regex.VM.captureNext.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
:
Option.map (Strategy.materializeUpdates bufferSize) (captureNext HistoryStrategy nfa wf it) = captureNext (BufferStrategy bufferSize) nfa wf it