@[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.instBEqRole.beq }

def NFA.Capture.instBEqRole.beq : Role → Role → Bool

Equations

• NFA.Capture.instBEqRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NFA.Capture.instDecidableEqRole : DecidableEq Role

Equations

• NFA.Capture.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NFA.Capture.instLawfulBEqRole : LawfulBEq Role

instance NFA.Capture.instReflBEqRole : ReflBEq Role

def NFA.Capture.roleToString : Role → String

Equations

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

instance NFA.Capture.instToStringRole : ToString Role

Equations

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

structure NFA.Capture : Type

A capture location. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• role : Role
• group : Nat

theorem NFA.Capture.ext_iff {x y : Capture} : x = y ↔ x.role = y.role ∧ x.group = y.group

theorem NFA.Capture.ext {x y : Capture} (role : x.role = y.role) (group : x.group = y.group) : x = y

def NFA.instBEqCapture.beq : Capture → Capture → Bool

Equations

• NFA.instBEqCapture.beq { role := a, group := a_1 } { role := b, group := b_1 } = (a == b && a_1 == b_1)
• NFA.instBEqCapture.beq x✝¹ x✝ = false

instance NFA.instBEqCapture : BEq Capture

Equations

• NFA.instBEqCapture = { beq := NFA.instBEqCapture.beq }

def NFA.instDecidableEqCapture.decEq (x✝ x✝¹ : Capture) : Decidable (x✝ = x✝¹)

Equations

• NFA.instDecidableEqCapture.decEq { role := a, group := a_1 } { role := b, group := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance NFA.instDecidableEqCapture : DecidableEq Capture

Equations

• NFA.instDecidableEqCapture = NFA.instDecidableEqCapture.decEq

instance NFA.instLECapture : LE Capture

Equations

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

instance NFA.instDecidableLeCapture (a b : Capture) : Decidable (a ≤ b)

Equations

• NFA.instDecidableLeCapture a b = ⋯.mpr instDecidableIte

def NFA.Capture.toString (c : Capture) : String

Equations

• c.toString = toString c.role ++ toString " " ++ toString c.group

instance NFA.Capture.instToString : ToString Capture

Equations

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

inductive NFA.Capture.Valid : Array Capture → Prop

A valid capture array consists of capture groups with two slots. For every capture group slot with Role.End exists a group slot with Role.Start

• mk {captures : Array Capture} (h : ∀ (c : { c : Capture // c ∈ captures ∧ c.role = Role.End }), ∃ (c' : Capture), c' ∈ captures ∧ c'.role = Role.Start ∧ c.val.group = c'.group) : Valid captures

theorem NFA.Capture.Valid.forall {captures : Array Capture} : Valid captures → ∀ (c : { c : Capture // c ∈ captures ∧ c.role = Role.End }), ∃ (c' : Capture), c' ∈ captures ∧ c'.role = Role.Start ∧ c.val.group = c'.group

theorem NFA.Capture.Valid.iff {captures : Array Capture} : Valid captures ↔ ∀ (c : { c : Capture // c ∈ captures ∧ c.role = Role.End }), ∃ (c' : Capture), c' ∈ captures ∧ c'.role = Role.Start ∧ c.val.group = c'.group

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.instBEqLook.beq }

def NFA.instBEqLook.beq : Look → Look → Bool

Equations

• NFA.instBEqLook.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NFA.instDecidableEqLook : DecidableEq Look

Equations

• NFA.instDecidableEqLook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

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.instBEqEatMode.beq }

def NFA.Unchecked.instBEqEatMode.beq : EatMode → EatMode → Bool

Equations

• NFA.Unchecked.instBEqEatMode.beq (NFA.Unchecked.EatMode.Until a) (NFA.Unchecked.EatMode.Until b) = (a == b)
• NFA.Unchecked.instBEqEatMode.beq (NFA.Unchecked.EatMode.ToLast a) (NFA.Unchecked.EatMode.ToLast b) = (a == b)
• NFA.Unchecked.instBEqEatMode.beq x✝¹ x✝ = false

def NFA.Unchecked.instDecidableEqEatMode.decEq (x✝ x✝¹ : EatMode) : Decidable (x✝ = x✝¹)

Equations

• NFA.Unchecked.instDecidableEqEatMode.decEq (NFA.Unchecked.EatMode.Until a) (NFA.Unchecked.EatMode.Until b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• NFA.Unchecked.instDecidableEqEatMode.decEq (NFA.Unchecked.EatMode.Until a) (NFA.Unchecked.EatMode.ToLast a_1) = isFalse ⋯
• NFA.Unchecked.instDecidableEqEatMode.decEq (NFA.Unchecked.EatMode.ToLast a) (NFA.Unchecked.EatMode.Until a_1) = isFalse ⋯
• NFA.Unchecked.instDecidableEqEatMode.decEq (NFA.Unchecked.EatMode.ToLast a) (NFA.Unchecked.EatMode.ToLast b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance NFA.Unchecked.instDecidableEqEatMode : DecidableEq EatMode

Equations

• NFA.Unchecked.instDecidableEqEatMode = NFA.Unchecked.instDecidableEqEatMode.decEq

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

Equations

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

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.instBEqTransition.beq }

def NFA.Unchecked.instBEqTransition.beq : Transition → Transition → Bool

Equations

• NFA.Unchecked.instBEqTransition.beq { start := a, «end» := a_1, next := a_2 } { start := b, «end» := b_1, next := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• NFA.Unchecked.instBEqTransition.beq x✝¹ x✝ = false

instance NFA.Unchecked.instDecidableEqTransition : DecidableEq Transition

Equations

• NFA.Unchecked.instDecidableEqTransition = NFA.Unchecked.instDecidableEqTransition.decEq

def NFA.Unchecked.instDecidableEqTransition.decEq (x✝ x✝¹ : Transition) : Decidable (x✝ = x✝¹)

Equations

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

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 : 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.instBEqState.beq }

def NFA.Unchecked.instBEqState.beq : State → State → Bool

Equations

• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Empty a) (NFA.Unchecked.State.Empty b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.NextChar a a_1) (NFA.Unchecked.State.NextChar b b_1) = (a == b && a_1 == b_1)
• NFA.Unchecked.instBEqState.beq NFA.Unchecked.State.Fail NFA.Unchecked.State.Fail = true
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Eat a a_1) (NFA.Unchecked.State.Eat b b_1) = (a == b && a_1 == b_1)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.ChangeFrameStep a a_1) (NFA.Unchecked.State.ChangeFrameStep b b_1) = (a == b && a_1 == b_1)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.RemoveFrameStep a) (NFA.Unchecked.State.RemoveFrameStep b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.BackRef a a_1 a_2) (NFA.Unchecked.State.BackRef b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.ByteRange a) (NFA.Unchecked.State.ByteRange b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.SparseTransitions a) (NFA.Unchecked.State.SparseTransitions b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Look a a_1) (NFA.Unchecked.State.Look b b_1) = (a == b && a_1 == b_1)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Union a) (NFA.Unchecked.State.Union b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.UnionReverse a) (NFA.Unchecked.State.UnionReverse b) = (a == b)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.BinaryUnion a a_1) (NFA.Unchecked.State.BinaryUnion b b_1) = (a == b && a_1 == b_1)
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Capture a a_1 a_2 a_3) (NFA.Unchecked.State.Capture b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• NFA.Unchecked.instBEqState.beq (NFA.Unchecked.State.Match a) (NFA.Unchecked.State.Match b) = (a == b)
• NFA.Unchecked.instBEqState.beq x✝¹ x✝ = false

instance NFA.Unchecked.instDecidableEqState : DecidableEq State

Equations

• NFA.Unchecked.instDecidableEqState = NFA.Unchecked.instDecidableEqState.decEq

def NFA.Unchecked.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

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

instance NFA.Unchecked.instBEqState_1 : BEq State

Equations

• NFA.Unchecked.instBEqState_1 = { beq := NFA.Unchecked.beq'✝ }

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
• (NFA.Unchecked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next
• NFA.Unchecked.State.Fail.toString = toString "State.Fail"
• (NFA.Unchecked.State.Eat s n).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString n
• (NFA.Unchecked.State.ChangeFrameStep «from» to).toString = toString "State.ChangeFrameStep from " ++ toString «from» ++ toString " to " ++ toString to
• (NFA.Unchecked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid
• (NFA.Unchecked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next
• (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) : StateID

next StateID of State s

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).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 }

structure NFA.Unchecked.NFA : Type

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

• states : Array State
• 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.instBEqEatMode.beq {n✝ : Nat} : EatMode n✝ → EatMode n✝ → Bool

Equations

• NFA.Checked.instBEqEatMode.beq (NFA.Checked.EatMode.Until a) (NFA.Checked.EatMode.Until b) = (a == b)
• NFA.Checked.instBEqEatMode.beq (NFA.Checked.EatMode.ToLast a) (NFA.Checked.EatMode.ToLast b) = (a == b)
• NFA.Checked.instBEqEatMode.beq x✝¹ x✝ = false

instance NFA.Checked.instBEqEatMode {n✝ : Nat} : BEq (EatMode n✝)

Equations

• NFA.Checked.instBEqEatMode = { beq := NFA.Checked.instBEqEatMode.beq }

def NFA.Checked.instDecidableEqEatMode.decEq {n✝ : Nat} (x✝ x✝¹ : EatMode n✝) : Decidable (x✝ = x✝¹)

Equations

• NFA.Checked.instDecidableEqEatMode.decEq (NFA.Checked.EatMode.Until a) (NFA.Checked.EatMode.Until b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• NFA.Checked.instDecidableEqEatMode.decEq (NFA.Checked.EatMode.Until a) (NFA.Checked.EatMode.ToLast a_1) = isFalse ⋯
• NFA.Checked.instDecidableEqEatMode.decEq (NFA.Checked.EatMode.ToLast a) (NFA.Checked.EatMode.Until a_1) = isFalse ⋯
• NFA.Checked.instDecidableEqEatMode.decEq (NFA.Checked.EatMode.ToLast a) (NFA.Checked.EatMode.ToLast b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance NFA.Checked.instDecidableEqEatMode {n✝ : Nat} : DecidableEq (EatMode n✝)

Equations

• NFA.Checked.instDecidableEqEatMode = NFA.Checked.instDecidableEqEatMode.decEq

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

Equations

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

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.instBEqTransition.beq {n✝ : Nat} : Transition n✝ → Transition n✝ → Bool

Equations

• NFA.Checked.instBEqTransition.beq { start := a, «end» := a_1, next := a_2 } { start := b, «end» := b_1, next := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• NFA.Checked.instBEqTransition.beq x✝¹ x✝ = false

instance NFA.Checked.instBEqTransition {n✝ : Nat} : BEq (Transition n✝)

Equations

• NFA.Checked.instBEqTransition = { beq := NFA.Checked.instBEqTransition.beq }

instance NFA.Checked.instDecidableEqTransition {n✝ : Nat} : DecidableEq (Transition n✝)

Equations

• NFA.Checked.instDecidableEqTransition = NFA.Checked.instDecidableEqTransition.decEq

def NFA.Checked.instDecidableEqTransition.decEq {n✝ : Nat} (x✝ x✝¹ : Transition n✝) : Decidable (x✝ = x✝¹)

Equations

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

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 : 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.

def NFA.Checked.instBEqState.beq {n✝ : Nat} : State n✝ → State n✝ → Bool

Equations

• NFA.Checked.instBEqState.beq (NFA.Checked.State.Empty a) (NFA.Checked.State.Empty b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.NextChar a a_1) (NFA.Checked.State.NextChar b b_1) = (a == b && a_1 == b_1)
• NFA.Checked.instBEqState.beq NFA.Checked.State.Fail NFA.Checked.State.Fail = true
• NFA.Checked.instBEqState.beq (NFA.Checked.State.Eat a a_1) (NFA.Checked.State.Eat b b_1) = (a == b && a_1 == b_1)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.ChangeFrameStep a a_1) (NFA.Checked.State.ChangeFrameStep b b_1) = (a == b && a_1 == b_1)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.RemoveFrameStep a) (NFA.Checked.State.RemoveFrameStep b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.BackRef a a_1 a_2) (NFA.Checked.State.BackRef b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• NFA.Checked.instBEqState.beq (NFA.Checked.State.ByteRange a) (NFA.Checked.State.ByteRange b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.SparseTransitions a) (NFA.Checked.State.SparseTransitions b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.Look a a_1) (NFA.Checked.State.Look b b_1) = (a == b && a_1 == b_1)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.Union a) (NFA.Checked.State.Union b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.UnionReverse a) (NFA.Checked.State.UnionReverse b) = (a == b)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.BinaryUnion a a_1) (NFA.Checked.State.BinaryUnion b b_1) = (a == b && a_1 == b_1)
• NFA.Checked.instBEqState.beq (NFA.Checked.State.Capture a a_1 a_2 a_3) (NFA.Checked.State.Capture b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• NFA.Checked.instBEqState.beq (NFA.Checked.State.Match a) (NFA.Checked.State.Match b) = (a == b)
• NFA.Checked.instBEqState.beq x✝¹ x✝ = false

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

Equations

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

def NFA.Checked.instDecidableEqState.decEq {n✝ : Nat} (x✝ x✝¹ : State n✝) : Decidable (x✝ = x✝¹)

Equations

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

instance NFA.Checked.instDecidableEqState {n✝ : Nat} : DecidableEq (State n✝)

Equations

• NFA.Checked.instDecidableEqState = NFA.Checked.instDecidableEqState.decEq

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

Equations

• NFA.Checked.instBEqState_1 = { 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
• (NFA.Checked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next
• NFA.Checked.State.Fail.toString = toString "State.Fail"
• (NFA.Checked.State.Eat s next).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString next
• (NFA.Checked.State.ChangeFrameStep f t).toString = toString "State.ChangeFrameStep from " ++ toString f ++ toString " to " ++ toString t
• (NFA.Checked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid
• (NFA.Checked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next
• (NFA.Checked.State.Union alts).toString = toString "State.Union [" ++ toString (String.join (List.map (fun (t : Fin n) => toString " " ++ toString t) alts.toList)) ++ 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 }

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

• captures : Array Capture

  all captures in states

• 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

• capturesValid : Capture.Valid self.captures

  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.toCkeckedState (s : Unchecked.State) (n : Nat) (h : s.nextOf < n) : Checked.State n

Equations

• One or more equations did not get rendered due to their size.
• NFA.toCkeckedState (NFA.Unchecked.State.Empty next) n h_2 = NFA.Checked.State.Empty ⟨next, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.NextChar offset next) n h_2 = NFA.Checked.State.NextChar offset ⟨next, h_2⟩
• NFA.toCkeckedState NFA.Unchecked.State.Fail n h_2 = NFA.Checked.State.Fail
• NFA.toCkeckedState (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.Until s_2) next) n h_2 = NFA.Checked.State.Eat (NFA.Checked.EatMode.Until ⟨s_2, ⋯⟩) ⟨next, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.ToLast s_2) next) n h_2 = NFA.Checked.State.Eat (NFA.Checked.EatMode.ToLast ⟨s_2, ⋯⟩) ⟨next, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.ChangeFrameStep f t) n h_2 = NFA.Checked.State.ChangeFrameStep ⟨f, ⋯⟩ ⟨t, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.RemoveFrameStep t) n h_2 = NFA.Checked.State.RemoveFrameStep ⟨t, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.BackRef b f sid) n h_2 = NFA.Checked.State.BackRef b f ⟨sid, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Look look next) n h_2 = NFA.Checked.State.Look look ⟨next, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Capture role next pattern_id group) n h_2 = NFA.Checked.State.Capture role ⟨next, h_2⟩ pattern_id group
• NFA.toCkeckedState (NFA.Unchecked.State.BinaryUnion alt1 alt2) n h_2 = NFA.Checked.State.BinaryUnion ⟨alt1, ⋯⟩ ⟨alt2, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Match pattern_id) n h_2 = NFA.Checked.State.Match pattern_id

def NFA.toFun (states : Array Unchecked.State) (h : ∀ (i : Nat) (x : i < states.size), states[i].nextOf < states.size) : { x : Unchecked.State // x ∈ states } → Checked.State states.size

Equations

• NFA.toFun states h = fun (s : { x : NFA.Unchecked.State // x ∈ states }) => NFA.toCkeckedState s.val states.size ⋯