def Regex.Strategy.materializeRegexGroups {s : String} : Data.CaptureGroups s → Nat → Option (s.ValidPos × s.ValidPos)

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 {s : String} (n : Nat) (accum : Vector s.ValidPosPlusOne n) : List (Nat × s.ValidPos) → Vector s.ValidPosPlusOne n

Equations

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

def Regex.Strategy.materializeUpdates {s : String} (n : Nat) (updates : List (Nat × s.ValidPos)) : Vector s.ValidPosPlusOne 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 (String.ValidPosPlusOne.sentinel s)) updates

def Regex.Strategy.equivPos {s : String} (p : Option s.ValidPos) (p' : s.ValidPosPlusOne) : Prop

Equations

• Regex.Strategy.equivPos (some p_2) p' = (p' = String.ValidPosPlusOne.validPos p_2)
• Regex.Strategy.equivPos none p' = (p' = String.ValidPosPlusOne.sentinel s)

@[simp]

theorem Regex.Strategy.equivPos.some_iff {s : String} {p : s.ValidPos} {p' : s.ValidPosPlusOne} : equivPos (some p) p' ↔ p' = String.ValidPosPlusOne.validPos p

@[simp]

theorem Regex.Strategy.equivPos.none_iff {s : String} {p' : s.ValidPosPlusOne} : equivPos none p' ↔ p' = String.ValidPosPlusOne.sentinel s

@[simp]

theorem Regex.Strategy.equivPos.validPos_iff {s : String} {p p' : s.ValidPos} : equivPos (some p) (String.ValidPosPlusOne.validPos p') ↔ p = p'

@[simp]

theorem Regex.Strategy.equivPos.sentinel_iff {s : String} {p : Option s.ValidPos} : equivPos p (String.ValidPosPlusOne.sentinel s) ↔ p = none

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

Equations

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

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

theorem Regex.Strategy.EquivMaterializedUpdate.eq_none {s : String} {n : Nat} {groups : Nat → Option (s.ValidPos × s.ValidPos)} {updates : Vector s.ValidPosPlusOne n} (eqv : EquivMaterializedUpdate groups updates) (tag : Nat) (lt : 2 * tag + 1 < n) (p₁ p₂ : s.ValidPos) : groups tag = none ↔ updates[2 * tag] = String.ValidPosPlusOne.sentinel s ∧ updates[2 * tag + 1] = String.ValidPosPlusOne.sentinel s