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 s.start ++ toString ", " ++ toString s.end }

inductive Compiler.NextOfLt : Array NFA.Unchecked.State → Prop

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

• mk {r : Array NFA.Unchecked.State} (h : ∀ (i : Nat) (x : i < r.size), r[i].nextOf < r.size) : NextOfLt r

theorem Compiler.NextOfLt.forall {r : Array NFA.Unchecked.State} : NextOfLt r → ∀ (i : Nat) (x : i < r.size), r[i].nextOf < r.size

theorem Compiler.NextOfLt.iff {r : Array NFA.Unchecked.State} : NextOfLt r ↔ ∀ (i : Nat) (x : i < r.size), r[i].nextOf < r.size