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: NFA.Capture.Role
• End: NFA.Capture.Role

instance NFA.Capture.instBEqRole : BEq NFA.Capture.Role

Equations

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

def NFA.Capture.toString : NFA.Capture.Role → String

Equations

• NFA.Capture.toString x = match x with | NFA.Capture.Role.Start => toString "Start" | NFA.Capture.Role.End => toString "End"

instance NFA.Capture.instToStringRole : ToString NFA.Capture.Role

Equations

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

inductive NFA.Look : Type

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

• Start: NFA.Look

  Match the beginning of text.

• End: NFA.Look

  Match the end of text.

• EndWithOptionalLF: NFA.Look

  Match the end of text (before optional newline).

• StartLF: NFA.Look

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

• EndLF: NFA.Look

  Match of a line or the end of text.

• StartCRLF: NFA.Look

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

• EndCRLF: NFA.Look

  Match of a line or the end of text.

• WordUnicode: NFA.Look

  Match a Unicode-aware word boundary.

• WordUnicodeNegate: NFA.Look

  Match a Unicode-aware negation of a word boundary.

• WordStartUnicode: NFA.Look

  Match the start of a Unicode word boundary.

• WordEndUnicode: NFA.Look

  Match the end of a Unicode word boundary.

• WordStartHalfUnicode: NFA.Look

  Match the start half of a Unicode word boundary.

• WordEndHalfUnicode: NFA.Look

  Match the end half of a Unicode word boundary.

• PreviousMatch: NFA.Look

  Match the end of the previous match or start of string

• ClearMatches: NFA.Look

  Clear matches

def NFA.Look.toString : NFA.Look → String

Equations

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

instance NFA.instToStringLook : ToString NFA.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: NFA.Unchecked.StateID → NFA.Unchecked.EatMode

  Eat frames until State found

• ToLast: NFA.Unchecked.StateID → NFA.Unchecked.EatMode

  Eat frames inclusive last occurunce of State.

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

Equations

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

instance NFA.Unchecked.instToStringEatMode : ToString NFA.Unchecked.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 : NFA.Unchecked.StateID

  The identifier of the state to transition to.

def NFA.Unchecked.Transition.matches (trans : NFA.Unchecked.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: NFA.Unchecked.StateID → NFA.Unchecked.State

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

• NextChar: Nat → NFA.Unchecked.StateID → NFA.Unchecked.State

  use next char

• Fail: NFA.Unchecked.State

  Fail, force backtrack

• Eat: NFA.Unchecked.EatMode → NFA.Unchecked.StateID → NFA.Unchecked.State

  remove Frame.Step in stack

• ChangeFrameStep: NFA.Unchecked.StateID → NFA.Unchecked.StateID → NFA.Unchecked.State

  change Frame.Step in stack and force backtrack

• RemoveFrameStep: NFA.Unchecked.StateID → NFA.Unchecked.State

  remove Frame.Step in stack and force backtrack

• BackRef: Nat → Bool → NFA.Unchecked.StateID → NFA.Unchecked.State

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

• ByteRange: NFA.Unchecked.Transition → NFA.Unchecked.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: Array NFA.Unchecked.Transition → NFA.Unchecked.State

  A sequence of transitions used to represent a sparse state.

• Look: NFA.Look → NFA.Unchecked.StateID → NFA.Unchecked.State

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

• Union: Array NFA.Unchecked.StateID → NFA.Unchecked.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: Array NFA.Unchecked.StateID → NFA.Unchecked.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: NFA.Unchecked.StateID → NFA.Unchecked.StateID → NFA.Unchecked.State

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture: NFA.Capture.Role → NFA.Unchecked.StateID → NFA.PatternID → Nat → Nat → NFA.Unchecked.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: NFA.PatternID → NFA.Unchecked.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.

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

Equations

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

instance NFA.Unchecked.instToStringState : ToString NFA.Unchecked.State

Equations

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

structure NFA.Unchecked.NFA : Type

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

• states : Array NFA.Unchecked.State
• start_anchored : NFA.Unchecked.StateID
• start_unanchored : NFA.Unchecked.StateID

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

Equations

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

instance NFA.instToStringNFA : ToString NFA.Unchecked.NFA

Equations

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

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

• Until: {n : Nat} → Fin n → NFA.Checked.EatMode n

  Eat frames until State found

• ToLast: {n : Nat} → Fin n → NFA.Checked.EatMode n

  Eat frames inclusive last occurunce of State.

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

Equations

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

instance NFA.Checked.instToStringEatMode {n : Nat} : ToString (NFA.Checked.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 : NFA.Checked.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.val) && decide (↑c.val.val ≤ 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} → Fin n → NFA.Checked.State n

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

• NextChar: {n : Nat} → Nat → Fin n → NFA.Checked.State n

  use netx char

• Fail: {n : Nat} → NFA.Checked.State n

  Fail, force backtracking

• Eat: {n : Nat} → NFA.Checked.EatMode n → Fin n → NFA.Checked.State n

  remove Frame.Step in stack

• ChangeFrameStep: {n : Nat} → Fin n → Fin n → NFA.Checked.State n

  change Frame.Step in stack and force backtracking

• RemoveFrameStep: {n : Nat} → Fin n → NFA.Checked.State n

  remove Frame.Step in stack and force backtrack

• BackRef: {n : Nat} → Nat → Bool → Fin n → NFA.Checked.State n

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

• ByteRange: {n : Nat} → NFA.Checked.Transition n → NFA.Checked.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} → Array (NFA.Checked.Transition n) → NFA.Checked.State n

  A sequence of transitions used to represent a sparse state.

• Look: {n : Nat} → NFA.Look → Fin n → NFA.Checked.State n

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

• Union: {n : Nat} → Array (Fin n) → NFA.Checked.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} → Array (Fin n) → NFA.Checked.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} → Fin n → Fin n → NFA.Checked.State n

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture: {n : Nat} → NFA.Capture.Role → Fin n → NFA.PatternID → Nat → Nat → NFA.Checked.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} → NFA.PatternID → NFA.Checked.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 (NFA.Checked.State n)

Equations

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

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

Equations

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

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

Equations

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

structure NFA.Checked.NFA : Type

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

• n : Nat

  number of states

• states : Array (NFA.Checked.State self.n)

  states of the NFA

• 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

theorem NFA.Checked.NFA.isEq (self : NFA.Checked.NFA) : self.n = self.states.size

assertion that n equals size of states

instance NFA.Checked.instInhabitedNFA : Inhabited NFA.Checked.NFA

Equations

• NFA.Checked.instInhabitedNFA = { default := { n := 0, states := #[], unanchored_prefix_in_backtrack := false, isEq := NFA.Checked.instInhabitedNFA.proof_1 } }

instance NFA.Checked.instCoeFinNSizeStateStates {nfa : NFA.Checked.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.Checked.NFA) : String

Equations

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

instance NFA.Checked.instToStringNFA : ToString NFA.Checked.NFA

Equations

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

def NFA.toCkecked (nfa : NFA.Unchecked.NFA) : Except String NFA.Checked.NFA

transform Unchecked.NFA to Checked.NFA

Equations

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