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 "" }

Regex

Main api for Regex

• Regex.build: build a Regex from the given pattern
• Regex.captures: searches for the first match of the regex
• Regex.all_captures: searches all successive non-overlapping matches of the regex

@[reducible, inline]

abbrev Regex.Match : Type

Represents a single match of a regex in a haystack.

Equations

• Regex.Match = Substring

instance Regex.instToStringMatch : ToString Regex.Match

Equations

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

structure Regex.Captures : Type

Represents the capture groups for a single match.

• fullMatch : Regex.Match

  the full match

• groups : Array (Option Regex.Match)

  the capture groups

def Regex.Captures.end? (c : Regex.Captures) : Option String.Pos

Equations

• c.end? = some c.fullMatch.stopPos

def Regex.Captures.matches (c : Regex.Captures) : Array (Option Regex.Match)

Equations

• c.matches = #[some c.fullMatch] ++ c.groups

instance Regex.instToStringCaptures : ToString Regex.Captures

Equations

• Regex.instToStringCaptures = { toString := fun (c : Regex.Captures) => toString "fullMatch: " ++ toString c.fullMatch ++ toString "\ngroups: " ++ toString c.groups ++ toString "" }

def Regex.build (s : String) (flavor : optParam Syntax.Flavor default) (flags : optParam Syntax.Flags default) (config : optParam Compiler.Config default) (extended : optParam Regex.Grammar.ExtendedKind Regex.Grammar.ExtendedKind.None) : Except String Regex

Build a Regex from the given pattern.

Equations

• Regex.build s flavor flags config extended = do let nfa ← Syntax.AstItems.parse s flavor extended >>= Syntax.translate flags >>= Compiler.compile config Except.ok { nfa := nfa }

def Regex.Log.captures (s : Substring) (re : Regex) (at : String.Pos) (logEnabled : Bool) : Array String × Option Regex.Captures

This routine searches for the first match of this regex in the haystack given, returns an array of log msgs, the overall match and the matches of each capture group

Equations

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

theorem Regex.Log.String.Pos.lt_def {a : String.Pos} {b : String.Pos} : a < b ↔ a.byteIdx < b.byteIdx

theorem Regex.Log.String.Pos.sub_lt_sub_left {k : String.Pos} {m : String.Pos} {n : String.Pos} (h1 : k < m) (h2 : k < n) : m - n < m - k

theorem Regex.Log.String.Pos.sizeof_lt_of_lt {a : String.Pos} {b : String.Pos} (h : a < b) : sizeOf a < sizeOf b

def Regex.Log.all_captures (s : Substring) (re : Regex) (logEnabled : Bool) : Array String × Array Regex.Captures

Returns an array of log msgs and all successive non-overlapping matches in the given haystack.

Equations

• Regex.Log.all_captures s re logEnabled = Regex.Log.all_captures_loop s { byteIdx := 0 } re logEnabled (#[], #[])

def Regex.captures (s : Substring) (re : Regex) (at : optParam String.Pos { byteIdx := 0 }) : Option Regex.Captures

This routine searches for the first match of this regex in the haystack given, and if found, returns not only the overall match but also the matches of each capture group in the regex. If no match is found, then None is returned.

Equations

• Regex.captures s re at = match Regex.Log.captures s re at false with | (fst, captures) => captures

def Regex.all_captures (s : Substring) (re : Regex) : Array Regex.Captures

Returns all successive non-overlapping matches in the given haystack.

Equations

• Regex.all_captures s re = match Regex.Log.all_captures s re false with | (fst, captures) => captures