structure Regex.CapturedGroups : Type

A structure representing the capture groups from a regex match.

Contains the original string (haystack) and a buffer of positions marking the start and end of each capture group.

• haystack : String
• buffer : Array (Option String.Pos)

instance Regex.instReprCapturedGroups : Repr CapturedGroups

Equations

• Regex.instReprCapturedGroups = { reprPrec := Regex.instReprCapturedGroups.repr }

def Regex.instReprCapturedGroups.repr : CapturedGroups → Nat → Std.Format

Equations

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

instance Regex.instDecidableEqCapturedGroups : DecidableEq CapturedGroups

Equations

• Regex.instDecidableEqCapturedGroups = Regex.instDecidableEqCapturedGroups.decEq

def Regex.instDecidableEqCapturedGroups.decEq (x✝ x✝¹ : CapturedGroups) : Decidable (x✝ = x✝¹)

Equations

• Regex.instDecidableEqCapturedGroups.decEq { haystack := a, buffer := a_1 } { haystack := b, buffer := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Regex.instInhabitedCapturedGroups : Inhabited CapturedGroups

Equations

• Regex.instInhabitedCapturedGroups = { default := Regex.instInhabitedCapturedGroups.default }

def Regex.instInhabitedCapturedGroups.default : CapturedGroups

Equations

• Regex.instInhabitedCapturedGroups.default = { haystack := default, buffer := default }

def Regex.CapturedGroups.get (self : CapturedGroups) (index : Nat) : Option Substring

Gets a specific capture group as a substring.

• self: The captured groups
• index: The index of the capture group to retrieve (0 for the entire match)
• Returns: An optional substring representing the capture group, or none if the group didn't participate in the match

Equations

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

def Regex.CapturedGroups.toArray (self : CapturedGroups) : Array (Option Substring)

Converts all capture groups to an array of optional substrings.

• self: The captured groups
• Returns: An array where each element is either a substring for a capture group or none if that group didn't participate in the match

Equations

• self.toArray = Regex.CapturedGroups.toArray.go self 0 #[]

@[irreducible]

def Regex.CapturedGroups.toArray.go (self : CapturedGroups) (i : Nat) (accum : Array (Option Substring)) : Array (Option Substring)

Equations

• Regex.CapturedGroups.toArray.go self i accum = if 2 * i < self.buffer.size then Regex.CapturedGroups.toArray.go self (i + 1) (accum.push (self.get i)) else accum

structure Regex.Captures : Type

A structure that enables iterating through all capture groups of regex matches in a string.

Provides a stateful iterator for finding all regex matches and their capture groups in a haystack string.

• regex : Regex
• haystack : String
• currentPos : String.Pos

def Regex.instReprCaptures.repr : Captures → Nat → Std.Format

Equations

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

instance Regex.instReprCaptures : Repr Captures

Equations

• Regex.instReprCaptures = { reprPrec := Regex.instReprCaptures.repr }

def Regex.Captures.next? (self : Captures) : Option (CapturedGroups × Captures)

Gets the next match and its capture groups.

• self: The captures iterator
• Returns: An optional pair containing the captured groups and an updated iterator, or none if no more matches are found

Equations

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

theorem Regex.Captures.zeroth_group_some_of_next?_some {self next : Captures} {groups : CapturedGroups} (h : self.next? = some (groups, next)) : (groups.get 0).isSome = true

def Regex.Captures.remaining (self : Captures) : String.Pos

Gets the number of remaining characters to process in the haystack string.

• self: The captures iterator
• Returns: The number of remaining positions

Equations

• self.remaining = self.haystack.endPos + { byteIdx := 1 } - self.currentPos

theorem Regex.Captures.lt_next?_some {groups : CapturedGroups} {m m' : Captures} (h : m.next? = some (groups, m')) : m.currentPos.byteIdx < m'.currentPos.byteIdx

theorem Regex.Captures.haystack_eq_next?_some {groups : CapturedGroups} {m m' : Captures} (h : m.next? = some (groups, m')) : m'.haystack = m.haystack

theorem Regex.Captures.next?_decreasing {groups : CapturedGroups} {m m' : Captures} (h : m.next? = some (groups, m')) : m'.remaining < m.remaining

theorem String.Pos.sizeOf_eq {p : Pos} : sizeOf p = 1 + p.byteIdx

theorem String.Pos.sizeOf_lt_iff {p p' : Pos} : sizeOf p < sizeOf p' ↔ p < p'

instance Regex.instStreamCapturesCapturedGroups : Stream Captures CapturedGroups

Equations

• Regex.instStreamCapturesCapturedGroups = { next? := Regex.Captures.next? }

def Regex.captures (regex : Regex) (s : String) : Captures

Creates a new Captures iterator for a regex pattern and input string.

• regex: The compiled regex pattern to use for matching
• s: The input string to search in
• Returns: A Captures iterator positioned at the start of the string

Equations

• regex.captures s = { regex := regex, haystack := s, currentPos := 0 }