def Regex.Strategy.materializeRegexGroups : Data.CaptureGroups → Nat → Option (String.Pos × String.Pos)

materializeRegexGroups groups constructs a mapping that associates each capture group's tag with the start/end positions of the last appearance of the capture group in the input string.

Equations

• Regex.Strategy.materializeRegexGroups Regex.Data.CaptureGroups.empty x✝ = none
• Regex.Strategy.materializeRegexGroups (Regex.Data.CaptureGroups.group tag first last groups) x✝ = if tag = x✝ then some (first, last) else Regex.Strategy.materializeRegexGroups groups x✝
• Regex.Strategy.materializeRegexGroups (g₁.concat g₂) x✝ = (Regex.Strategy.materializeRegexGroups g₂ x✝ <|> Regex.Strategy.materializeRegexGroups g₁ x✝)

def Regex.Strategy.materializeUpdatesAux (n : Nat) (accum : Vector (Option String.Pos) n) : List (Nat × String.Pos) → Vector (Option String.Pos) n

Equations

• Regex.Strategy.materializeUpdatesAux n accum [] = accum
• Regex.Strategy.materializeUpdatesAux n accum ((offset, pos) :: rest) = Regex.Strategy.materializeUpdatesAux n (accum.setIfInBounds offset (some pos)) rest

def Regex.Strategy.materializeUpdates (n : Nat) (updates : List (Nat × String.Pos)) : Vector (Option String.Pos) n

materializeUpdates n updates constructs a buffer of size n which interprets the updates list as the writes to the buffer. When the same offset appears multiple times in the list, the last one wins.

Equations

• Regex.Strategy.materializeUpdates n updates = Regex.Strategy.materializeUpdatesAux n (Vector.replicate n none) updates

def Regex.Strategy.EquivMaterializedUpdate {n : Nat} (groups : Nat → Option (String.Pos × String.Pos)) (updates : Vector (Option String.Pos) n) : Prop

Equations

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

theorem Regex.Strategy.EquivMaterializedUpdate.eq {n : Nat} {groups : Nat → Option (String.Pos × String.Pos)} {updates : Vector (Option String.Pos) n} (eqv : EquivMaterializedUpdate groups updates) (tag : Nat) (lt : 2 * tag + 1 < n) (p₁ p₂ : String.Pos) : groups tag = some (p₁, p₂) ↔ updates[2 * tag] = some p₁ ∧ updates[2 * tag + 1] = some p₂