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 Compiler.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.instInhabitedThompsonRef : Inhabited Compiler.ThompsonRef

Equations

• Compiler.instInhabitedThompsonRef = { default := { start := 0, «end» := 0 } }

instance Compiler.instToStringThompsonRef : ToString Compiler.ThompsonRef

Equations

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

@[reducible, inline]

abbrev Compiler.CompilerM (α : Type) : Type

Equations

• Compiler.CompilerM = StateT (Array NFA.Unchecked.State) (Except String)

def Compiler.compile (config : Compiler.Config := default) (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.