def Regex.Backtracker.StackEntry.materialize {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (entryH : StackEntry HistoryStrategy nfa startIdx maxIdx) : StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx

Equations

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

def Regex.Backtracker.materializeStack {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)) : List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx)

Equations

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

@[simp]

theorem Regex.Backtracker.materializeStack.nil {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} : materializeStack [] = []

@[simp]

theorem Regex.Backtracker.materializeStack.cons {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} {entryH : StackEntry HistoryStrategy nfa startIdx maxIdx} {stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)} : materializeStack (entryH :: stackH) = entryH.materialize :: materializeStack stackH

def Regex.Backtracker.materializeResultAux {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (resultH : Option (List (ℕ × String.Pos)) × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : Option (Buffer bufferSize) × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)

Equations

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

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

Equations

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

theorem Regex.Backtracker.captureNextAux.pushNext.refines {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx bufferSize : ℕ} {stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)} {stackB : List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx)} {updateH : HistoryStrategy.Update} {updateB : (BufferStrategy bufferSize).Update} {state : Fin nfa.nodes.size} {it : Data.BoundedIterator startIdx maxIdx} (refEntry : { update := updateH, state := state, it := it }.materialize = { update := updateB, state := state, it := it }) (refStack : materializeStack stackH = stackB) : materializeStack (pushNext HistoryStrategy nfa wf startIdx maxIdx stackH updateH state it) = pushNext (BufferStrategy bufferSize) nfa wf startIdx maxIdx stackB updateB state it

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

theorem Regex.Backtracker.captureNext.go.refines {maxIdx : ℕ} (nfa : NFA) (wf : nfa.WellFormed) (startIdx bufferSize : ℕ) (bit : Data.BoundedIterator startIdx maxIdx) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : materializeResult (go HistoryStrategy nfa wf startIdx maxIdx bit visited) = go (BufferStrategy bufferSize) nfa wf startIdx maxIdx bit visited

theorem Regex.Backtracker.captureNext.refines (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : ℕ) (it : String.Iterator) : materializeResult (captureNext HistoryStrategy nfa wf it) = captureNext (BufferStrategy bufferSize) nfa wf it