refactor: redefine String.replace

Author: TwoFX

src/Init/Data/String.lean

@@ -22,3 +22,4 @@ public import Init.Data.String.Substring
 public import Init.Data.String.TakeDrop
 public import Init.Data.String.Modify
 public import Init.Data.String.Termination
+public import Init.Data.String.ToSlice

src/Init/Data/String/Search.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.String.Pattern
+public import Init.Data.String.ToSlice
+public import Init.Data.String.Slice
+
+set_option doc.verso true
+
+/-!
+# String API
+-/
+
+public section
+
+namespace String
+
+section
+open String.Slice Pattern
+
+variable {ρ : Type} {σ : Slice → Type}
+variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterators.Finite (σ s) Id]
+variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
+
+
+/--
+Constructs a new string obtained by replacing all occurrences of {name}`pattern` with
+{name}`replacement` in {name}`s`.
+
+Examples:
+* {lean}`"red green blue".replace "e" "" = "rd grn blu"`
+* {lean}`"red green blue".replace "ee" "E" = "red grEn blue"`
+* {lean}`"red green blue".replace "e" "E" = "rEd grEEn bluE"`
+* {lean}`"abc".replace "" "k" = "rakbkck"`
+-/
+@[inline]
+def replace [ToForwardSearcher ρ σ] [ToSlice α] (s : String) (pattern : ρ)
+    (replacement : α) : String :=
+  s.toSlice.replace pattern replacement
+
+end
+
+end String

src/Init/Data/String/Slice.lean

@@ -9,6 +9,7 @@ prelude
 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
 
 set_option doc.verso true
 
@@ -36,6 +37,12 @@ public section
 
 namespace String.Slice
 
+instance : HAppend String String.Slice String where
+  -- This implementation performs an unnecessary copy which could be avoided by providing a custom
+  -- C++ implementation for this instance. Note: if `String` had no custom runtime representation
+  -- at all, then this would be very easy to get right from Lean using `ByteArray.copySlice`.
+  hAppend s t := s ++ t.copy
+
 open Pattern
 
 /--
@@ -349,6 +356,22 @@ Examples:
 def dropPrefix [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
   dropPrefix? s pat |>.getD s
 
+/--
+Constructs a new string obtained by replacing all occurrences of {name}`pattern` with
+{name}`replacement` in {name}`s`.
+
+Examples:
+* {lean}`"red green blue".toSlice.replace "e" "" = "rd grn blu"`
+* {lean}`"red green blue".toSlice.replace "ee" "E" = "red grEn blue"`
+* {lean}`"red green blue".toSlice.replace "e" "E" = "rEd grEEn bluE"`
+* {lean}`"abc".toSlice.replace "" "k" = "rakbkck"`
+-/
+def replace [ToForwardSearcher ρ σ] [ToSlice α] (s : Slice) (pattern : ρ) (replacement : α) :
+    String :=
+  (ToForwardSearcher.toSearcher s pattern).fold (init := "") (fun
+    | sofar, .matched .. => sofar ++ ToSlice.toSlice replacement
+    | sofar, .rejected start stop => sofar ++ s.replaceStartEnd! start stop)
+
 /--
 Removes the specified number of characters (Unicode code points) from the start of the slice.
 

src/Init/Data/String/ToSlice.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+
+/-!
+# The `ToSlice` typeclass
+-/
+
+public section
+
+namespace String
+
+/--
+Typeclass for types that have a conversion function to `String.Slice`. This typeclass is used to
+make some `String`/`String.Slice` functions polymorphic. As such, for now it is not intended that
+there instances of this beyond `ToSlice String` and `ToSlice String.Slice`.
+
+To convert arbitrary data into a string representation, see `ToString` and `Repr`.
+-/
+class ToSlice (α : Type u) where
+  toSlice : α → String.Slice
+
+@[inline]
+instance : ToSlice String.Slice where
+  toSlice := id
+
+@[inline]
+instance : ToSlice String where
+  toSlice := toSlice
+
+end String