structure Regex.VM.SearchState {s : String} (σ : Strategy s) (nfa : NFA) : Type

• states : Data.SparseSet nfa.nodes.size
• updates : Vector σ.Update nfa.nodes.size

@[reducible, inline]

abbrev Regex.VM.εStack {s : String} (σ : Strategy s) (nfa : NFA) : Type

Equations

• Regex.VM.εStack σ nfa = List (σ.Update × Fin nfa.nodes.size)

@[inline]

def Regex.VM.εClosure.writeUpdate (node : NFA.Node) : Bool

As an optimization, we write the updates to the buffer only when the state is done, a character, or a sparse state.

Equations

• Regex.VM.εClosure.writeUpdate Regex.NFA.Node.done = true
• Regex.VM.εClosure.writeUpdate (Regex.NFA.Node.char c next) = true
• Regex.VM.εClosure.writeUpdate (Regex.NFA.Node.sparse cs next) = true
• Regex.VM.εClosure.writeUpdate node = false

@[inline]

def Regex.VM.εClosure.pushNext {s : String} (σ : Strategy s) (nfa : NFA) (p : s.ValidPos) (node : NFA.Node) (inBounds : node.inBounds nfa.nodes.size) (update : σ.Update) (stack : εStack σ nfa) : εStack σ nfa

Equations

• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.epsilon state') inBounds_2 update stack = (update, ⟨state', inBounds_2⟩) :: stack
• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.split state₁ state₂) inBounds_2 update stack = (update, ⟨state₁, ⋯⟩) :: (update, ⟨state₂, ⋯⟩) :: stack
• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.save offset state') inBounds_2 update stack = (σ.write update offset p, ⟨state', inBounds_2⟩) :: stack
• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.anchor a state') inBounds_2 update stack = if Regex.Data.Anchor.test p a = true then (update, ⟨state', inBounds_2⟩) :: stack else stack
• Regex.VM.εClosure.pushNext σ nfa p Regex.NFA.Node.done inBounds_2 update stack = stack
• Regex.VM.εClosure.pushNext σ nfa p Regex.NFA.Node.fail inBounds_2 update stack = stack
• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.char c next) inBounds_2 update stack = stack
• Regex.VM.εClosure.pushNext σ nfa p (Regex.NFA.Node.sparse cs next) inBounds_2 update stack = stack

@[irreducible]

def Regex.VM.εClosure {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) (matched : Option σ.Update) (next : SearchState σ nfa) (stack : εStack σ nfa) : Option σ.Update × SearchState σ nfa

Visit all ε-transitions from the states in the stack, updating next.states when the new state is .done, .char, or .sparse. Returns .some updates if a .done state is reached, meaning a match is found.

Equations

• One or more equations did not get rendered due to their size.
• Regex.VM.εClosure σ nfa wf p matched next [] = (matched, next)

def Regex.VM.stepChar {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) (ne : p ≠ s.endValidPos) (currentUpdates : Vector σ.Update nfa.nodes.size) (next : SearchState σ nfa) (state : Fin nfa.nodes.size) : Option σ.Update × SearchState σ nfa

If the given state can make a transition on the current character of it, make the transition and traverse ε-closures from the resulting state.

Equations

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

def Regex.VM.eachStepChar {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) (ne : p ≠ s.endValidPos) (current next : SearchState σ nfa) : Option σ.Update × SearchState σ nfa

For all states in current, make a transition on the current character of it and traverse ε-closures from the resulting states.

Equations

• Regex.VM.eachStepChar σ nfa wf p ne current next = Regex.VM.eachStepChar.go σ nfa wf p ne current 0 ⋯ next

@[irreducible]

def Regex.VM.eachStepChar.go {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) (ne : p ≠ s.endValidPos) (current : SearchState σ nfa) (i : Nat) (hle : i ≤ current.states.count) (next : SearchState σ nfa) : Option σ.Update × SearchState σ nfa

Equations

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

def Regex.VM.captureNext {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) : Option σ.Update

Equations

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

@[irreducible]

def Regex.VM.captureNext.go {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (p : s.ValidPos) (matched : Option σ.Update) (current next : SearchState σ nfa) : Option σ.Update

Equations

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

def Regex.VM.captureNextBuf {s : String} (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : Nat) (p : s.ValidPos) : Option (Buffer s bufferSize)

Equations

• Regex.VM.captureNextBuf nfa wf bufferSize p = Regex.VM.captureNext (Regex.BufferStrategy s bufferSize) nfa wf p