Compiler

Compile from a regex's high-level intermediate representation (Syntax.Hir) into an NFA state graph (NFA).

structure Compiler.Config : Type

The configuration used for a Thompson NFA compiler.

• unanchored_prefix : Bool

  Whether to compile an unanchored prefix into this NFA.

• unanchored_prefix_simulation : Bool

  Whether to simulate an unanchored prefix with the backtracker.

• fuel : Nat

  Max recurciosn deth in compilation

instance Compiler.instInhabitedConfig : Inhabited Config

Equations

• Compiler.instInhabitedConfig = { default := { unanchored_prefix := true, unanchored_prefix_simulation := false, fuel := 1000 } }

structure Compiler.ThompsonRef : Type

A value that represents the result of compiling a sub-expression of a regex's HIR. Specifically, this represents a sub-graph of the NFA that has an initial state at start and a final state at end.

• start : NFA.Unchecked.StateID
• end : NFA.Unchecked.StateID

instance Compiler.instToStringThompsonRef : ToString ThompsonRef

Equations

• Compiler.instToStringThompsonRef = { toString := fun (s : Compiler.ThompsonRef) => toString "" ++ toString s.start ++ toString ", " ++ toString s.end ++ toString "" }

@[reducible, inline]

abbrev Compiler.States : Type

Equations

• Compiler.States = { a : Array NFA.Unchecked.State // ∀ (i : Nat) (x : i < a.size), a[i].nextOf < a.size }

@[reducible, inline]

abbrev Compiler.States' (states : States) : Type

Equations

• Compiler.States' states = { states' : Compiler.States // states.val.size ≤ states'.val.size }

@[reducible, inline]

abbrev Compiler.StateIDStates (states : States) : Type

Equations

• Compiler.StateIDStates states = { pairs : NFA.Unchecked.StateID × Compiler.States // pairs.fst < pairs.snd.val.size ∧ states.val.size < pairs.snd.val.size }

@[reducible, inline]

abbrev Compiler.StateIDStates' (states states' : States) : Type

Equations

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

@[reducible, inline]

abbrev Compiler.ThompsonRefStates (states : States) : Type

Equations

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

def Compiler.ThompsonRefStates.mk {states : States} (arg1Start arg1End : NFA.Unchecked.StateID) (arg2 : States) (h : arg1Start < arg2.val.size ∧ arg1End < arg2.val.size ∧ states.val.size < arg2.val.size) : ThompsonRefStates states

Equations

• Compiler.ThompsonRefStates.mk arg1Start arg1End arg2 h = ⟨({ start := arg1Start, «end» := arg1End }, arg2), h⟩

def Compiler.ThompsonRefStates.castLt {states states' : States} (t : ThompsonRefStates states) (h : states'.val.size < t.val.snd.val.size) : ThompsonRefStates states'

Equations

• t.castLt h = Compiler.ThompsonRefStates.mk t.val.fst.start t.val.fst.end t.val.snd ⋯

@[reducible, inline]

abbrev Compiler.CompilerM (α : Type) : Type

Equations

• Compiler.CompilerM = StateT (Array Nat) (Except String)

def Compiler.compile (config : Config := default) (flavor : Syntax.Flavor) (expr : Syntax.Hir) : Except String NFA.Checked.NFA

Compile the HIR expression given.

Equations

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