NFA

A byte oriented Thompson non-deterministic finite automaton (Checked.NFA), see also Tagged NFA.

@[reducible, inline]

abbrev NFA.PatternID : Type

The identifier of a regex pattern, represented by a Nat

Equations

• NFA.PatternID = Nat

inductive NFA.Capture.Role : Type

• Start : Role
• End : Role

instance NFA.Capture.instBEqRole : BEq Role

Equations

• NFA.Capture.instBEqRole = { beq := NFA.Capture.beqRole✝ }

def NFA.Capture.toString : Role → String

Equations

• NFA.Capture.toString NFA.Capture.Role.Start = toString "Start"
• NFA.Capture.toString NFA.Capture.Role.End = toString "End"

instance NFA.Capture.instToStringRole : ToString Role

Equations

• NFA.Capture.instToStringRole = { toString := NFA.Capture.toString }

inductive NFA.Look : Type

The high-level intermediate representation for a look-around assertion.

• Start : Look

  Match the beginning of text.

• End : Look

  Match the end of text.

• EndWithOptionalLF : Look

  Match the end of text (before optional newline).

• StartLF : Look

  Match the beginning of a line or the beginning of text.

• EndLF : Look

  Match of a line or the end of text.

• StartCRLF : Look

  Match the beginning of a line or the beginning of text.

• EndCRLF : Look

  Match of a line or the end of text.

• WordUnicode : Look

  Match a Unicode-aware word boundary.

• WordUnicodeNegate : Look

  Match a Unicode-aware negation of a word boundary.

• WordStartUnicode : Look

  Match the start of a Unicode word boundary.

• WordEndUnicode : Look

  Match the end of a Unicode word boundary.

• WordStartHalfUnicode : Look

  Match the start half of a Unicode word boundary.

• WordEndHalfUnicode : Look

  Match the end half of a Unicode word boundary.

• PreviousMatch : Look

  Match the end of the previous match or start of string

• ClearMatches : Look

  Clear matches

instance NFA.instBEqLook : BEq Look

Equations

• NFA.instBEqLook = { beq := NFA.beqLook✝ }

def NFA.Look.toString : Look → String

Equations

• NFA.Look.Start.toString = toString "Start"
• NFA.Look.End.toString = toString "End"
• NFA.Look.EndWithOptionalLF.toString = toString "EndWithOptionalLF"
• NFA.Look.StartLF.toString = toString "StartLF"
• NFA.Look.EndLF.toString = toString "EndLF"
• NFA.Look.StartCRLF.toString = toString "StartCRLF"
• NFA.Look.EndCRLF.toString = toString "EndCRLF"
• NFA.Look.WordUnicode.toString = toString "WordUnicode"
• NFA.Look.WordUnicodeNegate.toString = toString "WordUnicodeNegate"
• NFA.Look.WordStartUnicode.toString = toString "WordStartUnicode"
• NFA.Look.WordEndUnicode.toString = toString "WordEndUnicode"
• NFA.Look.WordStartHalfUnicode.toString = toString "WordStartHalfUnicode"
• NFA.Look.WordEndHalfUnicode.toString = toString "WordEndHalfUnicode"
• NFA.Look.PreviousMatch.toString = toString "PreviousMatch"
• NFA.Look.ClearMatches.toString = toString "ClearMatches"

instance NFA.instToStringLook : ToString Look

Equations

• NFA.instToStringLook = { toString := NFA.Look.toString }

@[reducible, inline]

abbrev NFA.Unchecked.StateID : Type

The identifier of a finite automaton state, represented by a Nat. The identifier may refer to a non existing state.

Equations

• NFA.Unchecked.StateID = Nat

inductive NFA.Unchecked.EatMode : Type

• Until : StateID → EatMode

  Eat frames until State found

• ToLast : StateID → EatMode

  Eat frames inclusive last occurunce of State.

instance NFA.Unchecked.instBEqEatMode : BEq EatMode

Equations

• NFA.Unchecked.instBEqEatMode = { beq := NFA.Unchecked.beqEatMode✝ }

def NFA.Unchecked.EatMode.toString : EatMode → String

Equations

• (NFA.Unchecked.EatMode.Until sid).toString = toString "Until " ++ toString sid ++ toString ""
• (NFA.Unchecked.EatMode.ToLast sid).toString = toString "ToLast " ++ toString sid ++ toString ""

def NFA.Unchecked.EatMode.nextOf (m : EatMode) : Nat

Equations

• (NFA.Unchecked.EatMode.Until sid).nextOf = sid
• (NFA.Unchecked.EatMode.ToLast sid).nextOf = sid

instance NFA.Unchecked.instToStringEatMode : ToString EatMode

Equations

• NFA.Unchecked.instToStringEatMode = { toString := NFA.Unchecked.EatMode.toString }

structure NFA.Unchecked.Transition : Type

A single transition to another state. This transition may only be followed if the current char in the haystack falls in the inclusive range of chars specified.

• start : UInt32

  The inclusive start of the char range.

• end : UInt32

  The inclusive end of the char range.

• next : StateID

  The identifier of the state to transition to.

instance NFA.Unchecked.instBEqTransition : BEq Transition

Equations

• NFA.Unchecked.instBEqTransition = { beq := NFA.Unchecked.beqTransition✝ }

def NFA.Unchecked.Transition.matches (trans : Transition) (c : Char) : Bool

check if c falls in the inclusive range of chars specified in Transition trans

Equations

• trans.matches c = (decide (trans.start ≤ c.val) && decide (c.val ≤ trans.end))

inductive NFA.Unchecked.State : Type

A state in an NFA.

• Empty (next : StateID) : State

  An empty state whose only purpose is to forward the automaton to another state via an unconditional epsilon transition.

• NextChar (offset : Nat) (next : StateID) : State

  use next char

• Fail : State

  Fail, force backtrack

• Eat (mode : EatMode) (next : StateID) : State

  remove Frame.Step in stack

• ChangeFrameStep («from» to : StateID) : State

  change Frame.Step in stack and force backtrack

• RemoveFrameStep (sid : StateID) : State

  remove Frame.Step in stack and force backtrack

• BackRef (n : Nat) (case_insensitive : Bool) (sid : StateID) : State

  A state with a single transition may only be followed if the currunt chars match the backrefence to the capturung group.

• ByteRange (trans : Transition) : State

  A state with a single transition that can only be taken if the current input symbol is in a particular range of chars.

• SparseTransitions (transitions : Array Transition) : State

  A sequence of transitions used to represent a sparse state.

• Look (look : NFA.Look) (next : StateID) : State

  A conditional epsilon transition satisfied via some sort of look-around.

• Union (alternates : Array StateID) : State

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via earlier transitions are preferred over later transitions.

• UnionReverse (alternates : Array StateID) : State

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via later transitions are preferred over earlier transitions.

• BinaryUnion (alt1 alt2 : StateID) : State

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture (role : Capture.Role) (next : StateID) (pattern_id : PatternID) (group_index slot : Nat) : State

  An empty state that records a capture location. slot in this context refers to the specific capture group slot offset that is being recorded. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• Match (pattern_id : PatternID) : State

  A match state. There is at least one such occurrence of this state for each regex that can match that is in this NFA.

instance NFA.Unchecked.instBEqState : BEq State

Equations

• NFA.Unchecked.instBEqState = { beq := NFA.Unchecked.beqState✝ }

def NFA.Unchecked.State.toString : State → String

Equations

• One or more equations did not get rendered due to their size.
• (NFA.Unchecked.State.Empty next).toString = toString "State.Empty => " ++ toString next ++ toString ""
• (NFA.Unchecked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next ++ toString ""
• NFA.Unchecked.State.Fail.toString = toString "State.Fail"
• (NFA.Unchecked.State.Eat s n).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString n ++ toString ""
• (NFA.Unchecked.State.ChangeFrameStep «from» to).toString = toString "State.ChangeFrameStep from " ++ toString «from» ++ toString " to " ++ toString to ++ toString ""
• (NFA.Unchecked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid ++ toString ""
• (NFA.Unchecked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next ++ toString ""
• (NFA.Unchecked.State.BinaryUnion alt1 alt2).toString = toString "State.BinaryUnion(" ++ toString alt1 ++ toString ", " ++ toString alt2 ++ toString ")"
• (NFA.Unchecked.State.Match pattern_id).toString = toString "State.Match (" ++ toString pattern_id ++ toString ")"

def NFA.Unchecked.State.nextOf (s : State) : Nat

Equations

• (NFA.Unchecked.State.Empty next).nextOf = next
• (NFA.Unchecked.State.NextChar offset next).nextOf = next
• NFA.Unchecked.State.Fail.nextOf = 0
• (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.Until s_2) next).nextOf = Nat.max s_2 next
• (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.ToLast s_2) next).nextOf = Nat.max s_2 next
• (NFA.Unchecked.State.ChangeFrameStep f t).nextOf = Nat.max f t
• (NFA.Unchecked.State.RemoveFrameStep next).nextOf = next
• (NFA.Unchecked.State.BackRef n case_insensitive next).nextOf = next
• (NFA.Unchecked.State.ByteRange trans).nextOf = trans.next
• (NFA.Unchecked.State.SparseTransitions trans).nextOf = List.maxD 0 (Array.map (fun (x : NFA.Unchecked.Transition) => x.next) trans).toList
• (NFA.Unchecked.State.Look look next).nextOf = next
• (NFA.Unchecked.State.Union alts).nextOf = List.maxD 0 alts.toList
• (NFA.Unchecked.State.UnionReverse alts).nextOf = List.maxD 0 alts.toList
• (NFA.Unchecked.State.BinaryUnion alt1 alt2).nextOf = Nat.max alt1 alt2
• (NFA.Unchecked.State.Capture role next pattern_id group_index slot).nextOf = next
• (NFA.Unchecked.State.Match pattern_id).nextOf = 0

instance NFA.Unchecked.instToStringState : ToString State

Equations

• NFA.Unchecked.instToStringState = { toString := NFA.Unchecked.State.toString }

def NFA.Unchecked.toSlots (states : Array State) : Array (Nat × Nat)

Array of (slot, group) pairs of captures.

Equations

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

structure NFA.Unchecked.NFA : Type

A char oriented Thompson non-deterministic finite automaton (NFA).

• states : Array State
• slots : Array (Nat × Nat)
• start_anchored : StateID
• start_unanchored : StateID

def NFA.Unchecked.NFA.toString (nfa : NFA) : String

Equations

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

instance NFA.instToStringNFA : ToString Unchecked.NFA

Equations

• NFA.instToStringNFA = { toString := NFA.Unchecked.NFA.toString }

inductive NFA.Checked.EatMode (n : Nat) : Type

• Until {n : Nat} : Fin n → EatMode n

  Eat frames until State found

• ToLast {n : Nat} : Fin n → EatMode n

  Eat frames inclusive last occurunce of State.

def NFA.Checked.EatMode.toString {n : Nat} : EatMode n → String

Equations

• (NFA.Checked.EatMode.Until sid).toString = toString "Until " ++ toString sid ++ toString ""
• (NFA.Checked.EatMode.ToLast sid).toString = toString "ToLast " ++ toString sid ++ toString ""

instance NFA.Checked.instToStringEatMode {n : Nat} : ToString (EatMode n)

Equations

• NFA.Checked.instToStringEatMode = { toString := NFA.Checked.EatMode.toString }

structure NFA.Checked.Transition (n : Nat) : Type

A single transition to another state. This transition may only be followed if the current char in the haystack falls in the inclusive range of chars specified.

• start : Nat

  The inclusive start of the char range.

• end : Nat

  The inclusive end of the char range.

• next : Fin n

  The identifier of the state to transition to.

def NFA.Checked.Transition.matches {n : Nat} (trans : Transition n) (c : Char) : Bool

check if c falls in the inclusive range of chars specified in Transition trans

Equations

• trans.matches c = (decide (trans.start ≤ ↑c.val.toFin) && decide (↑c.val.toFin ≤ trans.end))

inductive NFA.Checked.State (n : Nat) : Type

A state in an NFA, the elements of Fin n refer to existing states in the NFA.

• Empty {n : Nat} (next : Fin n) : State n

  An empty state whose only purpose is to forward the automaton to another state via an unconditional epsilon transition.

• NextChar {n : Nat} (offset : Nat) (next : Fin n) : State n

  use netx char

• Fail {n : Nat} : State n

  Fail, force backtracking

• Eat {n : Nat} (mode : EatMode n) (next : Fin n) : State n

  remove Frame.Step in stack

• ChangeFrameStep {n : Nat} (fr to : Fin n) : State n

  change Frame.Step in stack and force backtracking

• RemoveFrameStep {n : Nat} (sid : Fin n) : State n

  remove Frame.Step in stack and force backtrack

• BackRef {n : Nat} (b : Nat) (case_insensitive : Bool) (sid : Fin n) : State n

  A state with a single transition may only be followed if the current chars match the backrefence to the capturung group.

• ByteRange {n : Nat} (trans : Transition n) : State n

  A state with a single transition that can only be taken if the current input symbol is in a particular range of chars.

• SparseTransitions {n : Nat} (transitions : Array (Transition n)) : State n

  A sequence of transitions used to represent a sparse state.

• Look {n : Nat} (look : NFA.Look) (next : Fin n) : State n

  A conditional epsilon transition satisfied via some sort of look-around.

• Union {n : Nat} (alternates : Array (Fin n)) : State n

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via earlier transitions are preferred over later transitions.

• UnionReverse {n : Nat} (alternates : Array (Fin n)) : State n

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via later transitions are preferred over earlier transitions.

• BinaryUnion {n : Nat} (alt1 alt2 : Fin n) : State n

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture {n : Nat} (role : Capture.Role) (next : Fin n) (pattern_id : PatternID) (group_index slot : Nat) : State n

  An empty state that records a capture location. slot in this context refers to the specific capture group slot offset that is being recorded. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• Match {n : Nat} (pattern_id : PatternID) : State n

  A match state. There is at least one such occurrence of this state for each regex that can match that is in this NFA.

instance NFA.Checked.instBEqState {n : Nat} : BEq (State n)

Equations

• NFA.Checked.instBEqState = { beq := NFA.Checked.beq'✝ }

def NFA.Checked.State.toString {n : Nat} : State n → String

Equations

• One or more equations did not get rendered due to their size.
• (NFA.Checked.State.Empty next).toString = toString "State.Empty => " ++ toString next ++ toString ""
• (NFA.Checked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next ++ toString ""
• NFA.Checked.State.Fail.toString = toString "State.Fail"
• (NFA.Checked.State.Eat s next).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString next ++ toString ""
• (NFA.Checked.State.ChangeFrameStep f t).toString = toString "State.ChangeFrameStep from " ++ toString f ++ toString " to " ++ toString t ++ toString ""
• (NFA.Checked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid ++ toString ""
• (NFA.Checked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next ++ toString ""
• (NFA.Checked.State.BinaryUnion alt1 alt2).toString = toString "State.BinaryUnion (" ++ toString alt1 ++ toString ", " ++ toString alt2 ++ toString ")"
• (NFA.Checked.State.Match pattern_id).toString = toString "State.Match (" ++ toString pattern_id ++ toString ")"

instance NFA.Checked.instToStringState {n : Nat} : ToString (State n)

Equations

• NFA.Checked.instToStringState = { toString := fun (s : NFA.Checked.State n) => s.toString }

def NFA.Checked.Slots.Valid (slots : Array (Nat × Nat)) : Bool

Valid slot arrays have even size and consist of groups with two slots at consecutive positions.

Equations

• NFA.Checked.Slots.Valid slots = (decide (slots.size % 2 = 0) && decide (List.map (fun (i : Nat) => (i, i.div 2)) (List.range slots.size) = slots.toList))

structure NFA.Checked.NFA : Type

A char oriented Thompson non-deterministic finite automaton (NFA) with n states

• n : Nat

  number of states

• states : Array (State self.n)

  states of the NFA

• groups : Array Nat

  capture groups which may match with a empty string

• slots : Array (Nat × Nat)

  Array of (slot, group) pairs of captures

• unanchored_prefix_in_backtrack : Bool

  simulate a unanchored prefix by the backtracker

• isEq : self.n = self.states.size

  assertion that n equals size of states

• slotsValid : Slots.Valid self.slots = true

  slots are valid

instance NFA.Checked.instInhabitedNFA : Inhabited NFA

Equations

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

instance NFA.Checked.instCoeFinNSizeStateStates {nfa : NFA} : Coe (Fin nfa.n) (Fin nfa.states.size)

Equations

• NFA.Checked.instCoeFinNSizeStateStates = { coe := fun (n : Fin nfa.n) => Fin.castLE ⋯ n }

def NFA.Checked.toString (nfa : NFA) : String

Equations

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

instance NFA.Checked.instToStringNFA : ToString NFA

Equations

• NFA.Checked.instToStringNFA = { toString := NFA.Checked.toString }

def NFA.toCkecked (nfa : Unchecked.NFA) (groups : Array Nat) (hall : ∀ (i : Nat) (h : i < nfa.states.size), nfa.states[i].nextOf < nfa.states.size) : Except String Checked.NFA

transform Unchecked.NFA to Checked.NFA

Equations

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

structure Regex : Type

A compiled regular expression for searching Unicode haystacks.

• nfa : NFA.Checked.NFA

instance instToStringRegex : ToString Regex

Equations

• instToStringRegex = { toString := fun (m : Regex) => toString "" ++ toString m.nfa ++ toString "" }