refactor: use String.Slice in String.take and variants (#11180)

This PR redefines `String.take` and variants to operate on
`String.Slice`. While previously functions returning a substring of the
input sometimes returned `String` and sometimes returned
`Substring.Raw`, they now uniformly return `String.Slice`.

This is a BREAKING change, because many functions now have a different
return type. So for example, if `s` is a string and `f` is a function
accepting a string, `f (s.drop 1)` will no longer compile because
`s.drop 1` is a `String.Slice`. To fix this, insert a call to `copy` to
restore the old behavior: `f (s.drop 1).copy`.

Of course, in many cases, there will be more efficient options. For
example, don't write `f <| s.drop 1 |>.copy |>.dropEnd 1 |>.copy`, write
`f <| s.drop 1 |>.dropEnd 1 |>.copy` instead. Also, instead of `(s.drop
1).copy = "Hello"`, write `s.drop 1 == "Hello".toSlice` instead.

Author: TwoFX

src/Init/Data/String/Basic.lean

@@ -2785,23 +2785,6 @@ where
 def substrEq (s1 : String) (pos1 : String.Pos.Raw) (s2 : String) (pos2 : String.Pos.Raw) (sz : Nat) : Bool :=
   Pos.Raw.substrEq s1 pos1 s2 pos2 sz
 
-/--
-Checks whether the first string (`p`) is a prefix of the second (`s`).
-
-`String.startsWith` is a version that takes the potential prefix after the string.
-
-Examples:
- * `"red".isPrefixOf "red green blue" = true`
- * `"green".isPrefixOf "red green blue" = false`
- * `"".isPrefixOf "red green blue" = true`
--/
-def isPrefixOf (p : String) (s : String) : Bool :=
-  Pos.Raw.substrEq p 0 s 0 p.rawEndPos.byteIdx
-
-@[export lean_string_isprefixof]
-def Internal.isPrefixOfImpl (p : String) (s : String) : Bool :=
-  String.isPrefixOf p s
-
 /--
 Returns the position of the beginning of the line that contains the position `pos`.
 

src/Init/Data/String/Slice.lean

@@ -10,6 +10,7 @@ public import Init.Data.String.Pattern
 public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
+public import Init.Data.String.Termination
 
 set_option doc.verso true
 
@@ -403,19 +404,19 @@ Examples:
  * {lean}`"red green blue".toSlice.dropWhile (fun (_ : Char) => true) == "".toSlice`
 -/
 @[inline]
-partial def dropWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
-  go s
+def dropWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
+  go s.startPos
 where
   @[specialize pat]
-  go (s : Slice) : Slice :=
-    if let some nextS := dropPrefix? s pat then
-      -- TODO: need lawful patterns to show this terminates
-      if s.startInclusive.offset < nextS.startInclusive.offset then
-        go nextS
+  go (curr : s.Pos) : Slice :=
+    if let some nextCurr := ForwardPattern.dropPrefix? (s.replaceStart curr) pat then
+      if curr < Pos.ofReplaceStart nextCurr then
+        go (Pos.ofReplaceStart nextCurr)
       else
-        s
+        s.replaceStart curr
     else
-      s
+      s.replaceStart curr
+  termination_by curr
 
 /--
 Removes leading whitespace from a slice by moving its start position to the first non-whitespace
@@ -463,19 +464,19 @@ Examples:
  * {lean}`"red green blue".toSlice.takeWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
 @[inline]
-partial def takeWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
+def takeWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
   go s.startPos
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
     if let some nextCurr := ForwardPattern.dropPrefix? (s.replaceStart curr) pat then
-      if (s.replaceStart curr).startPos < nextCurr then
-        -- TODO: need lawful patterns to show this terminates
+      if curr < Pos.ofReplaceStart nextCurr then
         go (Pos.ofReplaceStart nextCurr)
       else
         s.replaceEnd curr
     else
       s.replaceEnd curr
+  termination_by curr
 
 /--
 Finds the position of the first match of the pattern {name}`pat` in a slice {name}`s`. If there
@@ -712,23 +713,23 @@ Examples:
  * {lean}`"red green blue".toSlice.dropEndWhile (fun (_ : Char) => true) == "".toSlice`
 -/
 @[inline]
-partial def dropEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
-  go s
+def dropEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
+  go s.endPos
 where
   @[specialize pat]
-  go (s : Slice) : Slice :=
-    if let some nextS := dropSuffix? s pat then
-      -- TODO: need lawful patterns to show this terminates
-      if nextS.endExclusive.offset < s.endExclusive.offset then
-        go nextS
+  go (curr : s.Pos) : Slice :=
+    if let some nextCurr := BackwardPattern.dropSuffix? (s.replaceEnd curr) pat then
+      if Pos.ofReplaceEnd nextCurr < curr then
+        go (Pos.ofReplaceEnd nextCurr)
       else
-        s
+        s.replaceEnd curr
     else
-      s
+      s.replaceEnd curr
+  termination_by curr.down
 
 /--
-Removes trailing whitespace from a slice by moving its start position to the first non-whitespace
-character, or to its end position if there is no non-whitespace character.
+Removes trailing whitespace from a slice by moving its end position to the last non-whitespace
+character, or to its start position if there is no non-whitespace character.
 
 “Whitespace” is defined as characters for which {name}`Char.isWhitespace` returns {name}`true`.
 
@@ -771,19 +772,19 @@ Examples:
  * {lean}`"red green blue".toSlice.takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
 @[inline]
-partial def takeEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
+def takeEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
   go s.endPos
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
     if let some nextCurr := BackwardPattern.dropSuffix? (s.replaceEnd curr) pat then
-      if nextCurr < (s.replaceEnd curr).endPos then
-        -- TODO: need lawful patterns to show this terminates
+      if Pos.ofReplaceEnd nextCurr < curr then
         go (Pos.ofReplaceEnd nextCurr)
       else
         s.replaceStart curr
     else
       s.replaceStart curr
+  termination_by curr.down
 
 /--
 Finds the position of the first match of the pattern {name}`pat` in a slice {name}`true`, starting
@@ -1338,4 +1339,36 @@ Examples:
 def back (s : Slice) : Char :=
   s.back?.getD default
 
+/--
+Appends the slices in a list of slices, placing the separator {name}`s` between each pair.
+
+Examples:
+ * {lean}`", ".toSlice.intercalate ["red".toSlice, "green".toSlice, "blue".toSlice] = "red, green, blue"`
+ * {lean}`" and ".toSlice.intercalate ["tea".toSlice, "coffee".toSlice] = "tea and coffee"`
+ * {lean}`" | ".toSlice.intercalate ["M".toSlice, "".toSlice, "N".toSlice] = "M |  | N"`
+-/
+def intercalate (s : Slice) : List Slice → String
+  | []      => ""
+  | a :: as => go a.copy s as
+where go (acc : String) (s : Slice) : List Slice → String
+  | a :: as => go (acc ++ s ++ a) s as
+  | []      => acc
+
+@[inherit_doc Slice.copy]
+def toString (s : Slice) : String :=
+  s.copy
+
+instance : ToString String.Slice where
+  toString := toString
+
+/--
+Converts a string to the Lean compiler's representation of names. The resulting name is
+hierarchical, and the string is split at the dots ({lean}`'.'`).
+
+{lean}`"a.b".toSlice.toName` is the name {lit}`a.b`, not {lit}`«a.b»`. For the latter, use
+`Name.mkSimple`.
+-/
+def toName (s : Slice) : Lean.Name :=
+  s.toString.toName
+
 end String.Slice