def Regex.VM.SearchState.materialize {s : String} {nfa : NFA} {bufferSize : ℕ} (stateH : SearchState (HistoryStrategy s) nfa) : SearchState (BufferStrategy s bufferSize) nfa

Equations

• stateH.materialize = { states := stateH.states, updates := Vector.map (Regex.Strategy.materializeUpdates bufferSize) stateH.updates }

@[simp]

theorem Regex.VM.SearchState.materialize_states {s : String} {nfa : NFA} {bufferSize : ℕ} {stateH : SearchState (HistoryStrategy s) nfa} : stateH.materialize.states = stateH.states

def Regex.VM.εStack.materialize {s : String} {nfa : NFA} {bufferSize : ℕ} (stackH : εStack (HistoryStrategy s) nfa) : εStack (BufferStrategy s bufferSize) nfa

Equations

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

@[simp]

theorem Regex.VM.εStack.materialize.nil {s : String} {nfa : NFA} {bufferSize : ℕ} : materialize [] = []

@[simp]

theorem Regex.VM.εStack.materialize.cons {s : String} {nfa : NFA} {bufferSize : ℕ} {stackH : εStack (HistoryStrategy s) nfa} {entry : (HistoryStrategy s).Update × Fin nfa.nodes.size} : materialize (entry :: stackH) = (Strategy.materializeUpdates bufferSize entry.1, entry.2) :: stackH.materialize

def Regex.VM.materializeResult {s : String} {nfa : NFA} {bufferSize : ℕ} (resultH : Option (HistoryStrategy s).Update × SearchState (HistoryStrategy s) nfa) : Option (BufferStrategy s bufferSize).Update × SearchState (BufferStrategy s bufferSize) nfa

Equations

• Regex.VM.materializeResult resultH = (Option.map (Regex.Strategy.materializeUpdates bufferSize) resultH.1, resultH.2.materialize)

theorem Regex.VM.εClosure.pushNext.refines {s : String} {nfa : NFA} {bufferSize : ℕ} {pos : s.ValidPos} {stackH : εStack (HistoryStrategy s) nfa} {stackB : εStack (BufferStrategy s bufferSize) nfa} {state : Fin nfa.nodes.size} {update : List (ℕ × s.ValidPos)} {buffer : Vector s.ValidPosPlusOne bufferSize} (wf : nfa.WellFormed) (h₁ : Strategy.materializeUpdates bufferSize update = buffer) (h₂ : stackH.materialize = stackB) : (pushNext (HistoryStrategy s) nfa pos nfa[state] ⋯ update stackH).materialize = pushNext (BufferStrategy s bufferSize) nfa pos nfa[state] ⋯ buffer stackB

theorem Regex.VM.εClosure.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} {matchedH : Option (List (ℕ × s.ValidPos))} {matchedB : Option (Buffer s bufferSize)} {nextH : SearchState (HistoryStrategy s) nfa} {nextB : SearchState (BufferStrategy s bufferSize) nfa} {stackH : εStack (HistoryStrategy s) nfa} {stackB : εStack (BufferStrategy s bufferSize) nfa} (resultB : Option (BufferStrategy s bufferSize).Update × SearchState (BufferStrategy s bufferSize) nfa) (resultH : Option (HistoryStrategy s).Update × SearchState (HistoryStrategy s) nfa) (h : εClosure (BufferStrategy s bufferSize) nfa wf pos matchedB nextB stackB = resultB) (h' : εClosure (HistoryStrategy s) nfa wf pos matchedH nextH stackH = resultH) (refMatched : Option.map (Strategy.materializeUpdates bufferSize) matchedH = matchedB) (refState : nextH.materialize = nextB) (refStack : stackH.materialize = stackB) : materializeResult resultH = resultB

theorem Regex.VM.stepChar.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} {ne : pos ≠ s.endValidPos} {nextH : SearchState (HistoryStrategy s) nfa} {nextB : SearchState (BufferStrategy s bufferSize) nfa} {currentUpdatesH : Vector (HistoryStrategy s).Update nfa.nodes.size} {currentUpdatesB : Vector (BufferStrategy s bufferSize).Update nfa.nodes.size} {state : Fin nfa.nodes.size} (resultB : Option (BufferStrategy s bufferSize).Update × SearchState (BufferStrategy s bufferSize) nfa) (resultH : Option (HistoryStrategy s).Update × SearchState (HistoryStrategy s) nfa) (h : stepChar (BufferStrategy s bufferSize) nfa wf pos ne currentUpdatesB nextB state = resultB) (h' : stepChar (HistoryStrategy s) nfa wf pos ne currentUpdatesH nextH state = resultH) (refUpdates : Vector.map (Strategy.materializeUpdates bufferSize) currentUpdatesH = currentUpdatesB) (refState : nextH.materialize = nextB) : materializeResult resultH = resultB

theorem Regex.VM.eachStepChar.go.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} {ne : pos ≠ s.endValidPos} {nextH : SearchState (HistoryStrategy s) nfa} {nextB : SearchState (BufferStrategy s bufferSize) nfa} {currentH : SearchState (HistoryStrategy s) nfa} {currentB : SearchState (BufferStrategy s bufferSize) nfa} {i : ℕ} {hleB : i ≤ currentB.states.count} {hleH : i ≤ currentH.states.count} (resultB : Option (BufferStrategy s bufferSize).Update × SearchState (BufferStrategy s bufferSize) nfa) (resultH : Option (HistoryStrategy s).Update × SearchState (HistoryStrategy s) nfa) (h : go (BufferStrategy s bufferSize) nfa wf pos ne currentB i hleB nextB = resultB) (h' : go (HistoryStrategy s) nfa wf pos ne currentH i hleH nextH = resultH) (refCurrent : currentH.materialize = currentB) (refNext : nextH.materialize = nextB) : materializeResult resultH = resultB

theorem Regex.VM.eachStepChar.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} {ne : pos ≠ s.endValidPos} {nextH : SearchState (HistoryStrategy s) nfa} {nextB : SearchState (BufferStrategy s bufferSize) nfa} {currentH : SearchState (HistoryStrategy s) nfa} {currentB : SearchState (BufferStrategy s bufferSize) nfa} (resultB : Option (BufferStrategy s bufferSize).Update × SearchState (BufferStrategy s bufferSize) nfa) (resultH : Option (HistoryStrategy s).Update × SearchState (HistoryStrategy s) nfa) (h : eachStepChar (BufferStrategy s bufferSize) nfa wf pos ne currentB nextB = resultB) (h' : eachStepChar (HistoryStrategy s) nfa wf pos ne currentH nextH = resultH) (refCurrent : currentH.materialize = currentB) (refNext : nextH.materialize = nextB) : materializeResult resultH = resultB

theorem Regex.VM.captureNext.go.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} {matchedH : Option (List (ℕ × s.ValidPos))} {matchedB : Option (Buffer s bufferSize)} {nextH : SearchState (HistoryStrategy s) nfa} {nextB : SearchState (BufferStrategy s bufferSize) nfa} {currentH : SearchState (HistoryStrategy s) nfa} {currentB : SearchState (BufferStrategy s bufferSize) nfa} {resultB : Option (BufferStrategy s bufferSize).Update} {resultH : Option (HistoryStrategy s).Update} (h : go (BufferStrategy s bufferSize) nfa wf pos matchedB currentB nextB = resultB) (h' : go (HistoryStrategy s) nfa wf pos matchedH currentH nextH = resultH) (refMatched : Option.map (Strategy.materializeUpdates bufferSize) matchedH = matchedB) (refCurrent : currentH.materialize = currentB) (refNext : nextH.materialize = nextB) : Option.map (Strategy.materializeUpdates bufferSize) resultH = resultB

theorem Regex.VM.captureNext.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {bufferSize : ℕ} {pos : s.ValidPos} : Option.map (Strategy.materializeUpdates bufferSize) (captureNext (HistoryStrategy s) nfa wf pos) = captureNext (BufferStrategy s bufferSize) nfa wf pos