refactor: use String.split instead of String.splitOn or String.splitToList (#11250)

This PR introduces a function `String.split` which is based on
`String.Slice.split` and therefore supports all pattern types and
returns a `Std.Iter String.Slice`.

This supersedes the functions `String.splitOn` and `String.splitToList`,
and we remove all all uses of these functions from core. They will be
deprecated in a future PR.

Migrating from `String.splitOn` and `String.splitToList` is easy: we
introduce functions `Iter.toStringList` and `Iter.toStringArray` that
can be used to conveniently go from `Std.Iter String.Slice` to `List
String` and `Array String`, so for example `s.splitOn "foo"` can be
replaced by `s.split "foo" |>.toStringList`.

Author: TwoFX

src/Init/Data/Format/Instances.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-import Init.Data.String.Basic
+import Init.Data.String.Search
 
 public section
 
@@ -47,7 +47,7 @@ Converts a string to a pretty-printer document, replacing newlines in the string
 `Std.Format.line`.
 -/
 def String.toFormat (s : String) : Std.Format :=
-  Std.Format.joinSep (s.splitOn "\n") Std.Format.line
+  Std.Format.joinSep (s.split '\n').toList Std.Format.line
 
 instance : ToFormat String.Pos.Raw where
   format p := format p.byteIdx

src/Init/Data/String.lean

@@ -25,3 +25,4 @@ public import Init.Data.String.Modify
 public import Init.Data.String.Termination
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
+public import Init.Data.String.Legacy

src/Init/Data/String/Basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura, Mario Carneiro
+Author: Leonardo de Moura, Mario Carneiro, Markus Himmel
 -/
 module
 
@@ -2479,98 +2479,6 @@ where
 def extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
   | s, b, e => Pos.Raw.extract s b e
 
-@[specialize] def splitAux (s : String) (p : Char → Bool) (b : Pos.Raw) (i : Pos.Raw) (r : List String) : List String :=
-  if h : i.atEnd s then
-    let r := (b.extract s i)::r
-    r.reverse
-  else
-    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (Pos.Raw.lt_next s _)
-    if p (i.get s) then
-      let i' := i.next s
-      splitAux s p i' i' (b.extract s i :: r)
-    else
-      splitAux s p b (i.next s) r
-termination_by s.rawEndPos.1 - i.1
-
-/--
-Splits a string at each character for which `p` returns `true`.
-
-The characters that satisfy `p` are not included in any of the resulting strings. If multiple
-characters in a row satisfy `p`, then the resulting list will contain empty strings.
-
-Examples:
-* `"coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]`
-* `"coffee  tea  water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]`
-* `"fun x =>\n  x + 1\n".split (· == '\n') = ["fun x =>", "  x + 1", ""]`
--/
-@[inline] def splitToList (s : String) (p : Char → Bool) : List String :=
-  splitAux s p 0 0 []
-
-@[inline, deprecated splitToList (since := "2025-10-17")]
-def split (s : String) (p : Char → Bool) : List String :=
-  splitToList s p
-
-/--
-Auxiliary for `splitOn`. Preconditions:
-* `sep` is not empty
-* `b <= i` are indexes into `s`
-* `j` is an index into `sep`, and not at the end
-
-It represents the state where we have currently parsed some split parts into `r` (in reverse order),
-`b` is the beginning of the string / the end of the previous match of `sep`, and the first `j` bytes
-of `sep` match the bytes `i-j .. i` of `s`.
--/
-def splitOnAux (s sep : String) (b : Pos.Raw) (i : Pos.Raw) (j : Pos.Raw) (r : List String) : List String :=
-  if i.atEnd s then
-    let r := (b.extract s i)::r
-    r.reverse
-  else
-    if i.get s == j.get sep then
-      let i := i.next s
-      let j := j.next sep
-      if j.atEnd sep then
-        splitOnAux s sep i i 0 (b.extract s (i.unoffsetBy j)::r)
-      else
-        splitOnAux s sep b i j r
-    else
-      splitOnAux s sep b ((i.unoffsetBy j).next s) 0 r
-termination_by (s.rawEndPos.1 - (j.byteDistance i), sep.rawEndPos.1 - j.1)
-decreasing_by
-  focus
-    rename_i h _ _
-    left; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Pos.Raw.lt_next s _))
-  focus
-    rename_i i₀ j₀ _ eq h'
-    rw [show (j₀.next sep).byteDistance (i₀.next s) = j₀.byteDistance i₀ by
-      change (_ + Char.utf8Size _) - (_ + Char.utf8Size _) = _
-      rw [(beq_iff_eq ..).1 eq, Nat.add_sub_add_right]; rfl]
-    right; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.le_add_right ..) (Nat.gt_of_not_le (mt decide_eq_true h')))
-      (Pos.Raw.lt_next sep _)
-  focus
-    rename_i h _
-    left; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
-      (Pos.Raw.lt_next s _)
-
-/--
-Splits a string `s` on occurrences of the separator string `sep`. The default separator is `" "`.
-
-When `sep` is empty, the result is `[s]`. When `sep` occurs in overlapping patterns, the first match
-is taken. There will always be exactly `n+1` elements in the returned list if there were `n`
-non-overlapping matches of `sep` in the string. The separators are not included in the returned
-substrings.
-
-Examples:
-* `"here is some text ".splitOn = ["here", "is", "some", "text", ""]`
-* `"here is some text ".splitOn "some" = ["here is ", " text "]`
-* `"here is some text ".splitOn "" = ["here is some text "]`
-* `"ababacabac".splitOn "aba" = ["", "bac", "c"]`
--/
-@[inline] def splitOn (s : String) (sep : String := " ") : List String :=
-  if sep == "" then [s] else splitOnAux s sep 0 0 0 []
 
 
 def Pos.Raw.offsetOfPosAux (s : String) (pos : Pos.Raw) (i : Pos.Raw) (offset : Nat) : Nat :=

src/Init/Data/String/Legacy.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura, Mario Carneiro
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+
+/-!
+# Legacy string functions
+
+This file contains `String` functions which have since been replaced by different functions and
+will be deprecated in the future.
+-/
+
+public section
+
+namespace String
+
+@[specialize] def splitAux (s : String) (p : Char → Bool) (b : Pos.Raw) (i : Pos.Raw) (r : List String) : List String :=
+  if h : i.atEnd s then
+    let r := (b.extract s i)::r
+    r.reverse
+  else
+    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (Pos.Raw.lt_next s _)
+    if p (i.get s) then
+      let i' := i.next s
+      splitAux s p i' i' (b.extract s i :: r)
+    else
+      splitAux s p b (i.next s) r
+termination_by s.rawEndPos.1 - i.1
+
+/--
+Splits a string at each character for which `p` returns `true`.
+
+The characters that satisfy `p` are not included in any of the resulting strings. If multiple
+characters in a row satisfy `p`, then the resulting list will contain empty strings.
+
+This is a legacy function. Use `String.split` instead.
+
+Examples:
+* `"coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]`
+* `"coffee  tea  water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]`
+* `"fun x =>\n  x + 1\n".split (· == '\n') = ["fun x =>", "  x + 1", ""]`
+-/
+@[inline] def splitToList (s : String) (p : Char → Bool) : List String :=
+  splitAux s p 0 0 []
+
+/--
+Auxiliary for `splitOn`. Preconditions:
+* `sep` is not empty
+* `b <= i` are indexes into `s`
+* `j` is an index into `sep`, and not at the end
+
+It represents the state where we have currently parsed some split parts into `r` (in reverse order),
+`b` is the beginning of the string / the end of the previous match of `sep`, and the first `j` bytes
+of `sep` match the bytes `i-j .. i` of `s`.
+-/
+def splitOnAux (s sep : String) (b : Pos.Raw) (i : Pos.Raw) (j : Pos.Raw) (r : List String) : List String :=
+  if i.atEnd s then
+    let r := (b.extract s i)::r
+    r.reverse
+  else
+    if i.get s == j.get sep then
+      let i := i.next s
+      let j := j.next sep
+      if j.atEnd sep then
+        splitOnAux s sep i i 0 (b.extract s (i.unoffsetBy j)::r)
+      else
+        splitOnAux s sep b i j r
+    else
+      splitOnAux s sep b ((i.unoffsetBy j).next s) 0 r
+termination_by (s.rawEndPos.1 - (j.byteDistance i), sep.rawEndPos.1 - j.1)
+decreasing_by
+  focus
+    rename_i h _ _
+    left; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Pos.Raw.lt_next s _))
+  focus
+    rename_i i₀ j₀ _ eq h'
+    rw [show (j₀.next sep).byteDistance (i₀.next s) = j₀.byteDistance i₀ by
+      change (_ + Char.utf8Size _) - (_ + Char.utf8Size _) = _
+      rw [(beq_iff_eq ..).1 eq, Nat.add_sub_add_right]; rfl]
+    right; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.le_add_right ..) (Nat.gt_of_not_le (mt decide_eq_true h')))
+      (Pos.Raw.lt_next sep _)
+  focus
+    rename_i h _
+    left; exact Nat.sub_lt_sub_left
+      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
+      (Pos.Raw.lt_next s _)
+
+/--
+Splits a string `s` on occurrences of the separator string `sep`. The default separator is `" "`.
+
+When `sep` is empty, the result is `[s]`. When `sep` occurs in overlapping patterns, the first match
+is taken. There will always be exactly `n+1` elements in the returned list if there were `n`
+non-overlapping matches of `sep` in the string. The separators are not included in the returned
+substrings.
+
+This is a legacy function. Use `String.split` instead.
+
+Examples:
+* `"here is some text ".splitOn = ["here", "is", "some", "text", ""]`
+* `"here is some text ".splitOn "some" = ["here is ", " text "]`
+* `"here is some text ".splitOn "" = ["here is some text "]`
+* `"ababacabac".splitOn "aba" = ["", "bac", "c"]`
+-/
+@[inline] def splitOn (s : String) (sep : String := " ") : List String :=
+  if sep == "" then [s] else splitOnAux s sep 0 0 0 []
+
+end String

src/Init/Data/String/Search.lean

@@ -96,6 +96,25 @@ Examples:
 def find? [ToForwardSearcher ρ σ] (s : String) (pattern : ρ) : Option s.ValidPos :=
   s.startValidPos.find? pattern
 
+/--
+Splits a string at each subslice that matches the pattern {name}`pat`.
+
+The subslices that matched the pattern are not included in any of the resulting subslices. If
+multiple subslices in a row match the pattern, the resulting list will contain empty strings.
+
+This function is generic over all currently supported patterns.
+
+Examples:
+ * {lean}`("coffee tea water".split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
+ * {lean}`("ababababa".split "aba").toList == ["coffee".toSlice, "water".toSlice]`
+ * {lean}`("baaab".split "aa").toList == ["b".toSlice, "ab".toSlice]`
+-/
+@[inline]
+def split [ToForwardSearcher ρ σ] (s : String) (pat : ρ) :=
+  (s.toSlice.split pat : Std.Iter String.Slice)
+
 end
 
 end String

src/Init/Data/String/Slice.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
+Authors: Henrik Böving, Markus Himmel
 -/
 module
 
@@ -795,9 +795,8 @@ This function is generic over all currently supported patterns except
 {name}`String`/{name}`String.Slice`.
 
 Examples:
- * {lean}`("coffee tea water".toSlice.find? Char.isWhitespace).map (·.get!) == some ' '`
- * {lean}`"tea".toSlice.find? (fun (c : Char) => c == 'X') == none`
- * {lean}`("coffee tea water".toSlice.find? "tea").map (·.get!) == some 't'`
+ * {lean}`("coffee tea water".toSlice.revFind? Char.isWhitespace).map (·.get!) == some ' '`
+ * {lean}`"tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none`
 -/
 @[specialize pat]
 def revFind? [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
@@ -1371,4 +1370,20 @@ hierarchical, and the string is split at the dots ({lean}`'.'`).
 def toName (s : Slice) : Lean.Name :=
   s.toString.toName
 
+instance : Std.ToFormat String.Slice where
+  format s := Std.ToFormat.format s.copy
+
 end String.Slice
+
+/-- Converts a {lean}`Std.Iter String.Slice` to a {lean}`List String`. -/
+@[inline]
+def Std.Iterators.Iter.toStringList {α : Type} [Std.Iterators.Iterator α Id String.Slice]
+    [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id]
+    (i : Std.Iter (α := α) String.Slice) : List String :=
+  i.map String.Slice.copy |>.toList
+
+/-- Converts a {lean}`Std.Iter String.Slice` to an {lean}`Array String`. -/
+def Std.Iterators.Iter.toStringArray {α : Type} [Std.Iterators.Iterator α Id String.Slice]
+    [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id]
+    (i : Std.Iter (α := α) String.Slice) : Array String :=
+  i.map String.Slice.copy |>.toArray

src/Init/System/FilePath.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.String.Basic
 import Init.Data.String.Modify
+import Init.Data.String.Search
 
 public section
 
@@ -242,7 +243,7 @@ def withExtension (p : FilePath) (ext : String) : FilePath :=
 Splits a path into a list of individual file names at the platform-specific path separator.
 -/
 def components (p : FilePath) : List String :=
-  p.normalize |>.toString.splitOn pathSeparator.toString
+  p.normalize |>.toString.split pathSeparator.toString |>.toStringList
 
 end FilePath
 
@@ -273,7 +274,7 @@ Separates the entries in the `$PATH` (or `%PATH%`) environment variable by the c
 platform-dependent separator character.
 -/
 def parse (s : String) : SearchPath :=
-  s.splitToList (fun c => SearchPath.separator == c) |>.map FilePath.mk
+  s.split SearchPath.separator |>.map (FilePath.mk ∘ String.Slice.copy) |>.toList
 
 /--
 Joins a list of paths into a suitable value for the current platform's `$PATH` (or `%PATH%`)

src/Lean/Compiler/FFI.lean

@@ -19,7 +19,7 @@ namespace Lean.Compiler.FFI
 private opaque getLeancExtraFlags : Unit → String
 
 private def flagsStringToArray (s : String) : Array String :=
-  s.splitOn.toArray |>.filter (· ≠ "")
+  s.split ' ' |>.filter (!·.isEmpty) |>.toStringArray
 
 /--
 Return C compiler flags for including Lean's headers.

src/Lean/Data/Lsp/Communication.lean

@@ -9,6 +9,7 @@ module
 prelude
 public import Lean.Data.JsonRpc
 import Init.Data.String.TakeDrop
+import Init.Data.String.Search
 
 public section
 

src/Lean/DocString/Formatter.lean

@@ -154,8 +154,10 @@ partial def versoSyntaxToString' (stx : Syntax) : ReaderT Nat (StateM String) Un
       out "\n"
       let i ← read
       let s := Syntax.decodeStrLit (atomString s) |>.getD ""
-        |>.splitToList (· == '\n')
-        |>.map ("".pushn ' ' i ++ · ) |> "\n".intercalate
+        |>.split '\n'
+        |>.map (fun (s : String.Slice) => "".pushn ' ' i ++ s)
+        |>.toList
+        |> "\n".intercalate
       out s
       out <| "".pushn ' ' i
       out <| atomString tk2