Migrate Utilities to ValidPos

Author: pandaman64

regex/Regex/Regex/Matches.lean

@@ -49,6 +49,15 @@ theorem lt_next?_some' {s : Slice} {m m' : Matches haystack} (h : m.next? = some
   unfold next? at h
   grind
 
+theorem str_eq_of_next?_some {s : Slice} {m m' : Matches haystack} (h : m.next? = some (s, m')) :
+  s.str = haystack := by
+  unfold next? at h
+  split at h <;> try contradiction
+  split at h <;> try contradiction
+  simp only [Option.some.injEq, Prod.mk.injEq] at h
+  next h' =>
+    simpa [←h] using searchNext_str_eq_some h'
+
 def lt (m m' : Matches haystack) : Prop := m.currentPos < m'.currentPos
 
 instance : LT (Matches haystack) := ⟨lt⟩

regex/Regex/Regex/Utilities.lean

@@ -1,7 +1,7 @@
 import Regex.Regex.Matches
 import Regex.Regex.Captures
 
-open String (Pos)
+open String (ValidPos Slice)
 
 namespace Regex
 
@@ -12,7 +12,7 @@ Finds the first match of a regex pattern in a string.
 * `haystack`: The input string to search in
 * Returns: An optional substring representing the match, or `none` if no match is found
 -/
-def find (regex : Regex) (haystack : String) : Option Substring :=
+def find (regex : Regex) (haystack : String) : Option Slice :=
   regex.matches haystack |>.next? |>.map Prod.fst
 
 /--
@@ -22,14 +22,14 @@ Finds all matches of a regex pattern in a string.
 * `haystack`: The input string to search in
 * Returns: An array of all matched substrings
 -/
-def findAll (regex : Regex) (haystack : String) : Array Substring :=
+def findAll (regex : Regex) (haystack : String) : Array Slice :=
   go (regex.matches haystack) #[]
 where
-  go (m : Matches) (accum : Array Substring) : Array Substring :=
+  go (m : Matches haystack) (accum : Array Slice) : Array Slice :=
     match _h : m.next? with
     | some (pos, m') => go m' (accum.push pos)
     | none => accum
-  termination_by m.remaining
+  termination_by m
 
 /--
 Transforms the first match of a regex pattern using its capture groups.
@@ -39,11 +39,13 @@ Transforms the first match of a regex pattern using its capture groups.
 * `transformer`: The rule yielding the string to replace the match with
 * Returns: The modified string, or the original string if no match is found
 -/
-def transform (regex : Regex) (haystack : String) (transformer : CapturedGroups → String) : String :=
+def transform (regex : Regex) (haystack : String) (transformer : CapturedGroups haystack → String) : String :=
     match h : (regex.captures haystack).next? with
-  | some (g,_) =>
-    let s := g.get 0 |>.get (Captures.zeroth_group_some_of_next?_some h)
-    Pos.Raw.extract haystack 0 s.startPos ++ transformer g ++ Pos.Raw.extract haystack s.stopPos haystack.endPos
+  | some (g, _) =>
+    match h' : g.get 0, Captures.zeroth_group_some_of_next?_some h with
+    | some s, _ =>
+      have eq : s.str = haystack := CapturedGroups.get_str_eq_some h'
+      ValidPos.extract haystack.startValidPos (s.startInclusive.cast eq) ++ transformer g ++ ValidPos.extract (s.endExclusive.cast eq) haystack.endValidPos
   | none => haystack
 
 /--
@@ -54,17 +56,19 @@ Transforms all matches of a regex pattern using its capture groups.
 * `transformer`: The rule yielding the string to replace the match with
 * Returns: The modified string, or the original string if no matches are found
 -/
-def transformAll (regex : Regex) (haystack : String) (transformer : CapturedGroups → String) : String :=
-  go (regex.captures haystack) "" 0
+def transformAll (regex : Regex) (haystack : String) (transformer : CapturedGroups haystack → String) : String :=
+  go (regex.captures haystack) "" haystack.startValidPos
 where
-  go (c : Captures) (accum : String) (endPos : Pos.Raw) : String :=
+  go (c : Captures haystack) (accum : String) (endPos : ValidPos haystack) : String :=
     match h : c.next? with
     | some (g, c') =>
-      let s := g.get 0 |>.get (Captures.zeroth_group_some_of_next?_some h)
-      go c' (accum ++ Pos.Raw.extract haystack endPos s.startPos ++ transformer g) s.stopPos
+      match h' : g.get 0, Captures.zeroth_group_some_of_next?_some h with
+      | some s, _ =>
+        have eq : s.str = haystack := CapturedGroups.get_str_eq_some h'
+        go c' (accum ++ ValidPos.extract endPos (s.startInclusive.cast eq) ++ transformer g) (s.endExclusive.cast eq)
     | none =>
-      accum ++ Pos.Raw.extract haystack endPos haystack.endPos
-  termination_by c.remaining
+      accum ++ ValidPos.extract endPos haystack.endValidPos
+  termination_by c
 
 /--
 Replaces the first match of a regex pattern with a replacement string.
@@ -96,7 +100,7 @@ Captures the first match of a regex pattern in a string, including capture group
 * Returns: An optional `CapturedGroups` containing the match and its capture groups,
           or `none` if no match is found
 -/
-def capture (regex : Regex) (haystack : String) : Option CapturedGroups :=
+def capture (regex : Regex) (haystack : String) : Option (CapturedGroups haystack) :=
   regex.captures haystack |>.next? |>.map Prod.fst
 
 /--
@@ -106,14 +110,14 @@ Captures all matches of a regex pattern in a string, including capture groups.
 * `haystack`: The input string to search in
 * Returns: An array of `CapturedGroups`, each containing a match and its capture groups
 -/
-def captureAll (regex : Regex) (haystack : String) : Array CapturedGroups :=
+def captureAll (regex : Regex) (haystack : String) : Array (CapturedGroups haystack) :=
   go (regex.captures haystack) #[]
 where
-  go (m : Captures) (accum : Array CapturedGroups) : Array CapturedGroups :=
+  go (m : Captures haystack) (accum : Array (CapturedGroups haystack)) : Array (CapturedGroups haystack) :=
     match _h : m.next? with
     | some (groups, m') => go m' (accum.push groups)
     | none => accum
-  termination_by m.remaining
+  termination_by m
 
 /--
 Extracts the first regex match in a string.
@@ -123,7 +127,7 @@ Extracts the first regex match in a string.
 * Returns: An optional string if a the match is found, or `none` otherwise
 -/
 def extract (regex : Regex) (haystack : String) : Option String :=
-  regex.find haystack |>.map Substring.toString
+  regex.find haystack |>.map Slice.copy
 
 /--
 Extracts all regex matches in a string.
@@ -133,7 +137,7 @@ Extracts all regex matches in a string.
 * Returns: an array containing all regex matches occuring in a string
 -/
 def extractAll (regex : Regex) (haystack : String) : Array String :=
-  regex.findAll haystack |>.map Substring.toString
+  regex.findAll haystack |>.map Slice.copy
 
 /--
 Tests if a regex matches a string.
@@ -162,15 +166,21 @@ Splits a string using regex matches as breakpoints.
 * `haystack`: The input string to search in
 * Returns: an array containing the substrings in between the regex matches
 -/
-def split (regex : Regex) (haystack : String) : Array Substring :=
-  go (regex.matches haystack) #[] 0
+def split (regex : Regex) (haystack : String) : Array Slice :=
+  go (regex.matches haystack) #[] haystack.startValidPos
 where
-  go (m : Matches) (accum : Array Substring) (endPos : Pos.Raw) : Array Substring :=
-    match _h : m.next? with
+  go (m : Matches haystack) (accum : Array Slice) (endPos : ValidPos haystack) : Array Slice :=
+    match h : m.next? with
     | some (s, m') =>
-      go m' (accum.push ⟨haystack, endPos, s.startPos⟩) s.stopPos
+      have eq : s.str = haystack := Matches.str_eq_of_next?_some h
+      let startPos := s.startInclusive.cast eq
+      if le : endPos ≤ startPos then
+        go m' (accum.push ⟨haystack, endPos, startPos, le⟩) (s.endExclusive.cast eq)
+      else
+        -- This should never happen
+        go m' accum (s.endExclusive.cast eq)
     | none =>
-      accum.push ⟨haystack, endPos, haystack.endPos⟩
-  termination_by m.remaining
+      accum.push (haystack.replaceStart endPos)
+  termination_by m
 
 end Regex