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.

instance Compiler.instInhabitedConfig : Inhabited Config

Equations

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

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 "" }

def Compiler.nextOfLt (r : Array NFA.Unchecked.State) : Prop

the next StateID of all states in array arr is less than size of arr.

Equations

• Compiler.nextOfLt r = ∀ (i : Nat) (x : i < r.size), r[i].nextOf < r.size