BoundedBacktracker

An NFA backed bounded backtracker for executing regex searches with capturing groups (BoundedBacktracker.slots).

This regex engine only implements leftmost-first match semantics and only supports leftmost searches. By design, this backtracking regex engine is bounded. This bound is implemented by not visiting any combination of NFA state ID and position in a haystack more than once.

All searches execute in linear time with respect to the size of the regular expression and search text.

def BoundedBacktracker.Array.Ref.mkRef {α β : Type} [Inhabited β] (arr : Array α) : ST.Ref β (Array α)

make reference of array

Equations

• BoundedBacktracker.Array.Ref.mkRef arr = (ST.Prim.mkRef arr (Void.mk default)).val

def BoundedBacktracker.Array.Ref.getRefValue {α β : Type} [Inhabited β] (ref : ST.Ref β (Array α)) : Array α

get array of reference

Equations

• BoundedBacktracker.Array.Ref.getRefValue ref = (ST.Prim.Ref.get ref (Void.mk default)).val

def BoundedBacktracker.Array.Ref.modifyRefValue {α β : Type} [Inhabited β] (ref : ST.Ref β (Array α)) (index : Nat) (value : α) (f : ST.Out β Unit → Bool := fun (x : ST.Out β Unit) => decide True) : ST.Ref β (Array α)

modify array, try to perform the update destructively

Equations

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

structure BoundedBacktracker.CharPos (s : String.Slice) : Type

Char position in a slice of some underlying string.

• pos : s.Pos

  current position

• curr? : Option Char

  char at current position

• prev? : Option Char

  char at previous position

def BoundedBacktracker.CharPos.create (s : String.Slice) («at» : s.Pos) : CharPos s

create a CharPos from s and position «at»

Equations

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

def BoundedBacktracker.CharPos.next {s : String.Slice} (cp : CharPos s) : CharPos s

to next position of cp

Equations

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

inductive BoundedBacktracker.Frame (n : Nat) (s : String.Slice) : Type

Represents a stack frame on the heap while doing backtracking.

• Step {n : Nat} {s : String.Slice} (sid : Fin n) («at» : CharPos s) : Frame n s

  Look for a match starting at sid and the given position in the haystack.

• RestoreCapture {n : Nat} {s : String.Slice} (role : NFA.Capture.Role) (slot : Nat) (pos : Option s.Pos) : Frame n s

  Reset the given slot to the given pos (which might be None).

@[implicit_reducible]

instance BoundedBacktracker.instToStringFrame {n : Nat} {s : String.Slice} : ToString (Frame n s)

Equations

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

@[reducible, inline]

abbrev BoundedBacktracker.Stack (n : Nat) (s : String.Slice) : Type

The stack of frames

Equations

• BoundedBacktracker.Stack n s = List (BoundedBacktracker.Frame n s)

@[inline]

def BoundedBacktracker.Stack.push {n : Nat} {s : String.Slice} (stack : Stack n s) (v : Frame n s) : Stack n s

Push frame to stack

Equations

• stack.push v = v :: stack

@[inline]

def BoundedBacktracker.Stack.pop? {n : Nat} {s : String.Slice} (stack : Stack n s) : Option (Frame n s × Stack n s)

pop head frame from stack

Equations

• BoundedBacktracker.Stack.pop? [] = none
• BoundedBacktracker.Stack.pop? (head :: tail) = some (head, tail)

def BoundedBacktracker.matches (s : String.Slice) («at» : s.Pos) (nfa : NFA.Checked.NFA) (logEnabled : Bool) : Array String × Array (Option { m : String.Slice // m.isSubslice s })

Search for the first match of this regex in the haystack given and return log msgs and the matches of each capture group.

Equations

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