def Regex.Backtracker.StackEntry.materialize {s : String} {nfa : NFA} {startPos : s.ValidPos} {bufferSize : ℕ} (entryH : StackEntry (HistoryStrategy s) nfa startPos) : StackEntry (BufferStrategy s bufferSize) nfa startPos

Equations

• entryH.materialize = { update := Regex.Strategy.materializeUpdates bufferSize entryH.update, state := entryH.state, pos := entryH.pos }

def Regex.Backtracker.materializeStack {s : String} {nfa : NFA} {startPos : s.ValidPos} {bufferSize : ℕ} (stackH : List (StackEntry (HistoryStrategy s) nfa startPos)) : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)

Equations

• Regex.Backtracker.materializeStack stackH = List.map Regex.Backtracker.StackEntry.materialize stackH

@[simp]

theorem Regex.Backtracker.materializeStack.nil {s : String} {nfa : NFA} {startPos : s.ValidPos} {bufferSize : ℕ} : materializeStack [] = []

@[simp]

theorem Regex.Backtracker.materializeStack.cons {s : String} {nfa : NFA} {startPos : s.ValidPos} {bufferSize : ℕ} {entryH : StackEntry (HistoryStrategy s) nfa startPos} {stackH : List (StackEntry (HistoryStrategy s) nfa startPos)} : materializeStack (entryH :: stackH) = entryH.materialize :: materializeStack stackH

def Regex.Backtracker.materializeResultAux {s : String} {nfa : NFA} {startPos : s.ValidPos} {bufferSize : ℕ} (resultH : Option (List (ℕ × s.ValidPos)) × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)

Equations

• Regex.Backtracker.materializeResultAux resultH = (Option.map (Regex.Strategy.materializeUpdates bufferSize) resultH.1, resultH.2)

def Regex.Backtracker.materializeResult {s : String} {bufferSize : ℕ} (resultH : Option (List (ℕ × s.ValidPos))) : Option (Buffer s bufferSize)

Equations

• Regex.Backtracker.materializeResult resultH = Option.map (Regex.Strategy.materializeUpdates bufferSize) resultH

theorem Regex.Backtracker.captureNextAux.pushNext.refines {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {bufferSize : ℕ} {stackH : List (StackEntry (HistoryStrategy s) nfa startPos)} {stackB : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)} {updateH : (HistoryStrategy s).Update} {updateB : (BufferStrategy s bufferSize).Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} (refEntry : { update := updateH, state := state, pos := pos }.materialize = { update := updateB, state := state, pos := pos }) (refStack : materializeStack stackH = stackB) : materializeStack (pushNext (HistoryStrategy s) nfa wf startPos stackH updateH state pos) = pushNext (BufferStrategy s bufferSize) nfa wf startPos stackB updateB state pos

theorem Regex.Backtracker.captureNextAux.refines {s : String} (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (bufferSize : ℕ) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) {stackH : List (StackEntry (HistoryStrategy s) nfa startPos)} {stackB : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)} (refStack : materializeStack stackH = stackB) : materializeResultAux (captureNextAux (HistoryStrategy s) nfa wf startPos visited stackH) = captureNextAux (BufferStrategy s bufferSize) nfa wf startPos visited stackB

theorem Regex.Backtracker.captureNext.go.refines {s : String} (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (bufferSize : ℕ) (bvpos : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : materializeResult (go (HistoryStrategy s) nfa wf startPos bvpos visited) = go (BufferStrategy s bufferSize) nfa wf startPos bvpos visited

theorem Regex.Backtracker.captureNext.refines {s : String} (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : ℕ) (pos : s.ValidPos) : materializeResult (captureNext (HistoryStrategy s) nfa wf pos) = captureNext (BufferStrategy s bufferSize) nfa wf pos