structure Regex.VM.SearchState (σ : Strategy) (nfa : NFA) : Type

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

@[reducible, inline]

abbrev Regex.VM.εStack (σ : Strategy) (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 (σ : Strategy) (nfa : NFA) (it : String.Iterator) (node : NFA.Node) (inBounds : node.inBounds nfa.nodes.size) (update : σ.Update) (stack : εStack σ nfa) : εStack σ nfa

Equations

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

@[irreducible]

def Regex.VM.εClosure (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) (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 it matched next [] = (matched, next)

def Regex.VM.stepChar (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) (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 (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) (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 it current next = Regex.VM.eachStepChar.go σ nfa wf it current 0 ⋯ next

@[irreducible]

def Regex.VM.eachStepChar.go (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) (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 (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) : Option σ.Update

Equations

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

@[irreducible]

def Regex.VM.captureNext.go (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) (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 (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : Nat) (it : String.Iterator) : Option (Buffer bufferSize)

Equations

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