instance Compiler.Code.instMonadLiftTStateTIdEStateM_regex {σ ε : Type u_1} : MonadLiftT (StateT σ Id) (EStateM ε σ)

Equations

• Compiler.Code.instMonadLiftTStateTIdEStateM_regex = { monadLift := fun {α : Type ?u.14} => EStateM.modifyGet }

instance Compiler.Code.instMonadLiftTStateTIdEStateMProd_regex {σ₁ ε : Type (max u_1 u_2)} {σ₂ : Type u_2} : MonadLiftT (StateT σ₁ Id) (EStateM ε (σ₁ × σ₂))

Equations

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

instance Compiler.Code.instMonadLiftTEStateMProd_regex {ε σ₁ : Type (max u_1 u_2)} {σ₂ : Type u_2} : MonadLiftT (EStateM ε σ₁) (EStateM ε (σ₁ × σ₂))

Equations

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

@[reducible, inline]

abbrev Compiler.Code.CompilerM (α : Type) : Type

the state consists of a pair of arrays of capture groups and of Unchecked.State's

Equations

• Compiler.Code.CompilerM α = EStateM String (Array NFA.Unchecked.State × Array Nat) α

@[reducible, inline]

abbrev Compiler.Code.StackM (α : Type) : Type

Equations

• Compiler.Code.StackM α = StateT (Array NFA.Unchecked.State) Id α

def Compiler.Code.push (s : NFA.Unchecked.State) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.push s = do let states ← get set (states.push s) pure states.size

def Compiler.Code.push' (s : NFA.Unchecked.State) : StackM ThompsonRef

Equations

• Compiler.Code.push' s = do let states ← get set (states.push s) pure { start := states.size, «end» := states.size }

def Compiler.Code.add_match (pattern_id : NFA.PatternID) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_match pattern_id = Compiler.Code.push (NFA.Unchecked.State.Match pattern_id)

def Compiler.Code.add_union : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_union = Compiler.Code.push (NFA.Unchecked.State.Union #[])

def Compiler.Code.add_union_reverse : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_union_reverse = Compiler.Code.push (NFA.Unchecked.State.UnionReverse #[])

def Compiler.Code.add_backrefence (case_insensitive : Bool) (b : Nat) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_backrefence case_insensitive b = Compiler.Code.push (NFA.Unchecked.State.BackRef b case_insensitive 0)

def Compiler.Code.c_range (start «end» : UInt32) : StackM ThompsonRef

Equations

• Compiler.Code.c_range start «end» = Compiler.Code.push' (NFA.Unchecked.State.ByteRange { start := start, «end» := «end», next := 0 })

def Compiler.Code.add_empty : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_empty = Compiler.Code.push (NFA.Unchecked.State.Empty 0)

def Compiler.Code.add_fail : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_fail = Compiler.Code.push NFA.Unchecked.State.Fail

def Compiler.Code.add_eat (mode : NFA.Unchecked.EatMode) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_eat mode = Compiler.Code.push (NFA.Unchecked.State.Eat mode 0)

def Compiler.Code.add_change_state : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_change_state = Compiler.Code.push (NFA.Unchecked.State.ChangeFrameStep 0 0)

def Compiler.Code.add_remove_state : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_remove_state = Compiler.Code.push (NFA.Unchecked.State.RemoveFrameStep 0)

def Compiler.Code.add_next_char (offset : Nat) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_next_char offset = Compiler.Code.push (NFA.Unchecked.State.NextChar offset 0)

def Compiler.Code.c_empty : StackM ThompsonRef

Equations

• Compiler.Code.c_empty = Compiler.Code.push' (NFA.Unchecked.State.Empty 0)

def Compiler.Code.add_sparse (trans : Array NFA.Unchecked.Transition) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.add_sparse trans = Compiler.Code.push (NFA.Unchecked.State.SparseTransitions trans)

def Compiler.Code.c_unicode_class (cls : Syntax.ClassUnicode) : StackM ThompsonRef

Equations

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

def Compiler.Code.c_literal (c : Char) : StackM ThompsonRef

Equations

• Compiler.Code.c_literal c = Compiler.Code.c_range c.val c.val

def Compiler.Code.c_look (look : Syntax.Look) : StackM ThompsonRef

Equations

• Compiler.Code.c_look Syntax.Look.Start = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.Start 0)
• Compiler.Code.c_look Syntax.Look.End = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.End 0)
• Compiler.Code.c_look Syntax.Look.EndWithOptionalLF = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.EndWithOptionalLF 0)
• Compiler.Code.c_look Syntax.Look.StartLF = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.StartLF 0)
• Compiler.Code.c_look Syntax.Look.EndLF = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.EndLF 0)
• Compiler.Code.c_look Syntax.Look.StartCRLF = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.StartCRLF 0)
• Compiler.Code.c_look Syntax.Look.EndCRLF = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.EndCRLF 0)
• Compiler.Code.c_look Syntax.Look.WordUnicode = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordUnicode 0)
• Compiler.Code.c_look Syntax.Look.WordUnicodeNegate = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordUnicodeNegate 0)
• Compiler.Code.c_look Syntax.Look.WordStartUnicode = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordStartUnicode 0)
• Compiler.Code.c_look Syntax.Look.WordEndUnicode = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordEndUnicode 0)
• Compiler.Code.c_look Syntax.Look.WordStartHalfUnicode = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordStartHalfUnicode 0)
• Compiler.Code.c_look Syntax.Look.WordEndHalfUnicode = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.WordEndHalfUnicode 0)
• Compiler.Code.c_look Syntax.Look.PreviousMatch = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.PreviousMatch 0)
• Compiler.Code.c_look Syntax.Look.ClearMatches = Compiler.Code.push' (NFA.Unchecked.State.Look NFA.Look.ClearMatches 0)

def Compiler.Code.c_cap' (role : NFA.Capture.Role) (pattern_id slot : Nat) : StackM NFA.Unchecked.StateID

Equations

• Compiler.Code.c_cap' role pattern_id slot = Compiler.Code.push (NFA.Unchecked.State.Capture role 0 0 pattern_id slot)

def Compiler.Code.c_possessive (tref : ThompsonRef) : PatchM ThompsonRef

embed start to end in a possessive union, i.e. remove backtracking frames from stack if end state is reached

Equations

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

def Compiler.Code.is_possible_empty_repetition (hir : Syntax.Hir) : Bool

Equations

• Compiler.Code.is_possible_empty_repetition (Syntax.Hir.mk (Syntax.HirKind.Repetition (Syntax.Repetition.mk 0 max greedy possessive sub)) props) = true
• Compiler.Code.is_possible_empty_repetition hir = false

def Compiler.Code.is_empty_concat (hir : Syntax.Hir) : Bool

Equations

• Compiler.Code.is_empty_concat hir = match hir with | Syntax.Hir.mk (Syntax.HirKind.Concat #[]) props => true | x => false

def Compiler.Code.get_possible_empty_capture_group (hir : Syntax.Hir) : Option Nat

collect group if hir is a capture group which may match with a empty string, it is used to build a greedy search in the Pcre flavor

Equations

• One or more equations did not get rendered due to their size.
• Compiler.Code.get_possible_empty_capture_group (Syntax.Hir.mk (Syntax.HirKind.Capture (Syntax.Capture.mk g name (Syntax.Hir.mk kind_2 props_1))) props) = none
• Compiler.Code.get_possible_empty_capture_group (Syntax.Hir.mk kind props) = none

def Compiler.Code.c_back_ref (case_insensitive : Bool) (n : Nat) : PatchM ThompsonRef

Equations

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

def Compiler.Code.head (hirs : Array Syntax.Hir) (h : 0 < hirs.size) : { pair : Syntax.Hir × Array Syntax.Hir // pair.fst ∈ hirs ∧ pair.snd.size < hirs.size ∧ sizeOf pair.snd < sizeOf hirs }

Equations

• Compiler.Code.head hirs h = match hm : hirs.toList, ⋯ with | head :: tail, this => ⟨(head, tail.toArray), ⋯⟩

theorem Compiler.Code.head_mem_lt {hirs : Array Syntax.Hir} {h : 0 < hirs.size} (x : { hir : Syntax.Hir // hir ∈ (head hirs h).val.snd }) : sizeOf x.val < sizeOf hirs

theorem Compiler.Code.head_apply_lt (hirs : Array Syntax.Hir) (h : 0 < hirs.size) : sizeOf (head hirs h).val.fst < sizeOf hirs

def Compiler.Code.cannotMatchEmptyString (hir : Syntax.Hir) : Bool

Equations

• Compiler.Code.cannotMatchEmptyString hir = match hir.properties.minimum_len with | some n => decide (n > 0) | none => false

def Compiler.Code.c_lookaround_PositiveLookahead (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_lookaround_NegativeLookahead (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_lookaround_PositiveLookbehind (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_lookaround_NegativeLookbehind (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_repetition_0_some_1_false (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_repetition_0_some_1_true (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_repetition_0_none (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) : PatchM ThompsonRef

Equations

• Compiler.Code.c_repetition_0_none union compiled = do Compiler.Code.patch union compiled.start Compiler.Code.patch compiled.end union pure { start := union, «end» := union }

def Compiler.Code.c_at_least_0_pre (compiled : ThompsonRef) (greedy : Bool) : PatchM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_at_least_0_post (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_at_least_set (possible_empty_capture_group : Option Nat) (greedy : Bool) : CompilerM Unit

Equations

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

def Compiler.Code.c_at_least_0 (compiled : ThompsonRef) (possible_empty_capture_group : Option Nat) (greedy : Bool) : CompilerM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_at_least_1_pre (greedy : Bool) : PatchM NFA.Unchecked.StateID

Equations

• Compiler.Code.c_at_least_1_pre greedy = if greedy = true then liftM Compiler.Code.add_union else liftM Compiler.Code.add_union_reverse

def Compiler.Code.c_at_least_1_post (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_at_least_1 (possible_empty_capture_group : Option Nat) (greedy : Bool) : CompilerM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_at_least_2 («prefix» last : ThompsonRef) (greedy possessive : Bool) : PatchM ThompsonRef

Equations

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

def Compiler.Code.c_bounded.fold.patch.pre (compiled : ThompsonRef) (prev_end : NFA.Unchecked.StateID) (greedy : Bool) : PatchM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_bounded.fold.patch.possessive (compiled : ThompsonRef) (empty : NFA.Unchecked.StateID) : PatchM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_bounded.fold.patch.post (compiled : ThompsonRef) (union empty : NFA.Unchecked.StateID) : PatchM NFA.Unchecked.StateID

Equations

• Compiler.Code.c_bounded.fold.patch.post compiled union empty = do Compiler.Code.patch union empty pure compiled.end

def Compiler.Code.c_bounded.fold.patch (compiled : ThompsonRef) (prev_end empty : NFA.Unchecked.StateID) (greedy possessive : Bool) : PatchM NFA.Unchecked.StateID

Equations

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

def Compiler.Code.c_alt_iter_step (first second : ThompsonRef) : PatchM (NFA.Unchecked.StateID × NFA.Unchecked.StateID)

Equations

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

def Compiler.Code.c_rep_pre (greedy : Bool) : PatchM NFA.Unchecked.StateID

Equations

• Compiler.Code.c_rep_pre greedy = if greedy = true then liftM Compiler.Code.add_union else liftM Compiler.Code.add_union_reverse

@[irreducible]

def Compiler.Code.c_concat.fold (hirs : Array Syntax.Hir) (s : NFA.Unchecked.StateID) : CompilerM NFA.Unchecked.StateID

Equations

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

@[irreducible]

def Compiler.Code.c_concat (hirs : Array Syntax.Hir) : CompilerM ThompsonRef

Equations

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

@[irreducible]

def Compiler.Code.c_alt_iter.fold (hirs : Array Syntax.Hir) (union «end» : NFA.Unchecked.StateID) : CompilerM Unit

Equations

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

@[irreducible]

def Compiler.Code.c_alt_iter (hirs : Array Syntax.Hir) : CompilerM ThompsonRef

Equations

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

@[irreducible]

def Compiler.Code.c_exactly.fold (hir : Syntax.Hir) (n : Nat) («end» : NFA.Unchecked.StateID) : CompilerM NFA.Unchecked.StateID

Equations

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

@[irreducible]

def Compiler.Code.c_exactly (hir : Syntax.Hir) (n : Nat) : CompilerM ThompsonRef

Equations

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

@[irreducible]

def Compiler.Code.c_at_least (hir : Syntax.Hir) (n : Nat) (greedy possessive : Bool) : CompilerM ThompsonRef

Compile the given expression such that it may be matched n or more times

Equations

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

@[irreducible]

def Compiler.Code.c_bounded.fold (hir : Syntax.Hir) (n : Nat) («prefix» : ThompsonRef) (empty : NFA.Unchecked.StateID) (greedy possessive : Bool) : CompilerM NFA.Unchecked.StateID

Equations

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

@[irreducible]

def Compiler.Code.c_bounded (hir : Syntax.Hir) (min max : Nat) (greedy possessive : Bool) : CompilerM ThompsonRef

Compile the given expression such that it matches at least min times, but no more than max times.

Equations

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

@[irreducible]

def Compiler.Code.c_lookaround (look : Syntax.Lookaround) : CompilerM ThompsonRef

Equations

• One or more equations did not get rendered due to their size.
• Compiler.Code.c_lookaround (Syntax.Lookaround.PositiveLookahead h) = do let compiled ← Compiler.Code.c h liftM (Compiler.Code.c_lookaround_PositiveLookahead compiled)
• Compiler.Code.c_lookaround (Syntax.Lookaround.NegativeLookahead h) = do let compiled ← Compiler.Code.c h liftM (Compiler.Code.c_lookaround_NegativeLookahead compiled)

@[irreducible]

def Compiler.Code.c_repetition (rep : Syntax.Repetition) : CompilerM ThompsonRef

Equations

• One or more equations did not get rendered due to their size.
• Compiler.Code.c_repetition (Syntax.Repetition.mk min (some max) greedy possessive sub) = if min ≤ max then Compiler.Code.c_bounded sub min max greedy possessive else liftM Compiler.Code.c_empty

@[irreducible]

def Compiler.Code.c_cap (hir : Syntax.Capture) : CompilerM ThompsonRef

Equations

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

@[irreducible]

def Compiler.Code.c (hir : Syntax.Hir) : CompilerM ThompsonRef

Equations

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

def Compiler.Code.init (anchored : Bool) : CompilerM ThompsonRef

Equations

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

def Compiler.Code.compile (anchored : Bool) (expr : Syntax.Hir) : CompilerM Unit

Compile the HIR expression given.

Equations

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