refactor: better name for String.replaceStart and variants (#11290)

This PR renames `String.replaceStartEnd` to `String.slice`,
`String.replaceStart` to `String.sliceFrom`, and `String.replaceEnd` to
`String.sliceTo`, and similar for the corresponding functions on
`String.Slice`.

Author: TwoFX

src/Init/Data/String/Basic.lean

@@ -81,13 +81,13 @@ theorem ValidPos.Splits.toSlice {s : String} {p : s.ValidPos} {t₁ t₂ : Strin
   splits_toSlice_iff.mpr h
 
 theorem ValidPos.splits {s : String} (p : s.ValidPos) :
-    p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy where
+    p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy where
   eq_append := by simp [← bytes_inj, Slice.bytes_copy, ← size_bytes]
   offset_eq_rawEndPos := by simp
 
 theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
-    p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy where
-  eq_append := copy_eq_copy_replaceEnd
+    p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy where
+  eq_append := copy_eq_copy_sliceTo
   offset_eq_rawEndPos := by simp
 
 theorem ValidPos.Splits.bytes_left_eq {s : String} {p : s.ValidPos} {t₁ t₂}
@@ -182,40 +182,40 @@ theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t
   rw [← toCopy_inj, ← startValidPos_copy, h.toCopy.eq_startValidPos_iff]
 
 theorem ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
-    p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) where
-  eq_append := by simpa [← append_assoc] using p.eq_copy_replaceEnd_append_get hp
+    p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where
+  eq_append := by simpa [← append_assoc] using p.eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
 theorem ValidPos.splits_next {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
-    (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy where
-  eq_append := p.eq_copy_replaceEnd_append_get hp
+    (p.next hp).Splits ((s.sliceTo p).copy ++ singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy where
+  eq_append := p.eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
 theorem Slice.Pos.splits_next_right {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
-    p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) where
-  eq_append := by simpa [← append_assoc] using p.copy_eq_copy_replaceEnd_append_get hp
+    p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where
+  eq_append := by simpa [← append_assoc] using p.copy_eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
 theorem Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
-    (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy where
-  eq_append := p.copy_eq_copy_replaceEnd_append_get hp
+    (p.next hp).Splits ((s.sliceTo p).copy ++ singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy where
+  eq_append := p.copy_eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
 theorem ValidPos.Splits.exists_eq_singleton_append {s : String} {p : s.ValidPos}
     (hp : p ≠ s.endValidPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
-  ⟨(s.replaceStart (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
+  ⟨(s.sliceFrom (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
 
 theorem ValidPos.Splits.exists_eq_append_singleton {s : String} {p : s.ValidPos}
     (hp : p ≠ s.endValidPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
-  ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
+  ⟨(s.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩
 
 theorem Slice.Pos.Splits.exists_eq_singleton_append {s : Slice} {p : s.Pos}
     (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
-  ⟨(s.replaceStart (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
+  ⟨(s.sliceFrom (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
 
 theorem Slice.Pos.Splits.exists_eq_append_singleton {s : Slice} {p : s.Pos}
     (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
-  ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
+  ⟨(s.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩
 
 theorem ValidPos.Splits.ne_endValidPos_of_singleton {s : String} {p : s.ValidPos}
     (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endValidPos := by

src/Init/Data/String/Lemmas/Splits.lean

@@ -41,10 +41,10 @@ def ValidPos.set {s : String} (p : s.ValidPos) (c : Char) (hp : p ≠ s.endValid
       refine ByteArray.IsValidUTF8.append ?_ (p.next hp).isValid.isValidUTF8_extract_utf8ByteSize
       exact p.isValid.isValidUTF8_extract_zero.push hc.1)
   else
-    (s.replaceEnd p).copy ++ singleton c ++ (s.replaceStart (p.next hp)).copy
+    (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy
 
 theorem ValidPos.set_eq_append {s : String} {p : s.ValidPos} {c : Char} {hp} :
-    p.set c hp = (s.replaceEnd p).copy ++ singleton c ++ (s.replaceStart (p.next hp)).copy := by
+    p.set c hp = (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy := by
   rw [set]
   split
   · rename_i h
@@ -56,7 +56,7 @@ theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp :
     {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) : q.IsValid (p.set c hp) := by
   rw [ValidPos.set_eq_append, String.append_assoc]
   apply append_right
-  rw [isValid_copy_iff, isValidForSlice_stringReplaceEnd]
+  rw [isValid_copy_iff, isValidForSlice_stringSliceTo]
   exact ⟨hpq, hq⟩
 
 /-- Given a valid position in a string, obtain the corresponding position after setting a character on
@@ -91,7 +91,7 @@ def ValidPos.appendRight {s : String} (p : s.ValidPos) (t : String) : (s ++ t).V
   isValid := p.isValid.append_right t
 
 theorem ValidPos.splits_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
-    (p.pastSet c hp).Splits ((s.replaceEnd p).copy ++ singleton c) (s.replaceStart (p.next hp)).copy where
+    (p.pastSet c hp).Splits ((s.sliceTo p).copy ++ singleton c) (s.sliceFrom (p.next hp)).copy where
   eq_append := set_eq_append
   offset_eq_rawEndPos := by simp
 

src/Init/Data/String/Modify.lean

@@ -64,7 +64,7 @@ Examples:
 @[inline]
 def Slice.Pos.find? {s : Slice} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ]  :
     Option s.Pos :=
-  ((s.replaceStart pos).find? pattern).map ofReplaceStart
+  ((s.sliceFrom pos).find? pattern).map ofSliceFrom
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in after the position

src/Init/Data/String/Search.lean

@@ -145,7 +145,7 @@ instance : Std.Iterators.Iterator (SplitIterator pat s) Id Slice where
     | ⟨.operating currPos searcher⟩ =>
       match h : searcher.step with
       | ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
-        let slice := s.replaceStartEnd! currPos startPos
+        let slice := s.slice! currPos startPos
         let nextIt := ⟨.operating endPos searcher'⟩
         pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
       | ⟨.yield searcher' (.rejected ..), hps⟩ =>
@@ -155,7 +155,7 @@ instance : Std.Iterators.Iterator (SplitIterator pat s) Id Slice where
         pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
           by simp [hps.isPlausibleSuccessor_of_skip]⟩)
       | ⟨.done, _⟩ =>
-        let slice := s.replaceStart currPos
+        let slice := s.sliceFrom currPos
         pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
     | ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
 
@@ -241,7 +241,7 @@ instance : Std.Iterators.Iterator (SplitInclusiveIterator pat s) Id Slice where
     | ⟨.operating currPos searcher⟩ =>
       match h : searcher.step with
       | ⟨.yield searcher' (.matched _ endPos), hps⟩ =>
-        let slice := s.replaceStartEnd! currPos endPos
+        let slice := s.slice! currPos endPos
         let nextIt := ⟨.operating endPos searcher'⟩
         pure (.deflate ⟨.yield nextIt slice,
           by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
@@ -253,7 +253,7 @@ instance : Std.Iterators.Iterator (SplitInclusiveIterator pat s) Id Slice where
           by simp [hps.isPlausibleSuccessor_of_skip]⟩)
       | ⟨.done, _⟩ =>
         if currPos != s.endPos then
-          let slice := s.replaceStart currPos
+          let slice := s.sliceFrom currPos
           pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
           pure (.deflate ⟨.done, by simp⟩)
@@ -337,7 +337,7 @@ Examples:
 -/
 @[inline]
 def dropPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option Slice :=
-  (ForwardPattern.dropPrefix? pat s).map s.replaceStart
+  (ForwardPattern.dropPrefix? pat s).map s.sliceFrom
 
 /--
 If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -377,7 +377,7 @@ def replace [ToSlice α] (s : Slice) (pattern : ρ) [ToForwardSearcher pattern 
     String :=
   (ToForwardSearcher.toSearcher pattern s).fold (init := "") (fun
     | sofar, .matched .. => sofar ++ ToSlice.toSlice replacement
-    | sofar, .rejected start stop => sofar ++ s.replaceStartEnd! start stop)
+    | sofar, .rejected start stop => sofar ++ s.slice! start stop)
 
 /--
 Removes the specified number of characters (Unicode code points) from the start of the slice.
@@ -391,7 +391,7 @@ Examples:
 -/
 @[inline]
 def drop (s : Slice) (n : Nat) : Slice :=
-  s.replaceStart (s.startPos.nextn n)
+  s.sliceFrom (s.startPos.nextn n)
 
 /--
 Creates a new slice that contains the longest prefix of {name}`s` for which {name}`pat` matched
@@ -409,13 +409,13 @@ def dropWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice :=
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
-    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.replaceStart curr) then
-      if curr < Pos.ofReplaceStart nextCurr then
-        go (Pos.ofReplaceStart nextCurr)
+    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then
+      if curr < Pos.ofSliceFrom nextCurr then
+        go (Pos.ofSliceFrom nextCurr)
       else
-        s.replaceStart curr
+        s.sliceFrom curr
     else
-      s.replaceStart curr
+      s.sliceFrom curr
   termination_by curr
 
 /--
@@ -449,7 +449,7 @@ Examples:
 -/
 @[inline]
 def take (s : Slice) (n : Nat) : Slice :=
-  s.replaceEnd (s.startPos.nextn n)
+  s.sliceTo (s.startPos.nextn n)
 
 /--
 Creates a new slice that contains the longest prefix of {name}`s` for which {name}`pat` matched
@@ -469,13 +469,13 @@ def takeWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice :=
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
-    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.replaceStart curr) then
-      if curr < Pos.ofReplaceStart nextCurr then
-        go (Pos.ofReplaceStart nextCurr)
+    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then
+      if curr < Pos.ofSliceFrom nextCurr then
+        go (Pos.ofSliceFrom nextCurr)
       else
-        s.replaceEnd curr
+        s.sliceTo curr
     else
-      s.replaceEnd curr
+      s.sliceTo curr
   termination_by curr
 
 /--
@@ -579,7 +579,7 @@ instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
     | ⟨.operating currPos searcher⟩ =>
       match h : searcher.step with
       | ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
-        let slice := s.replaceStartEnd! endPos currPos
+        let slice := s.slice! endPos currPos
         let nextIt := ⟨.operating startPos searcher'⟩
         pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
       | ⟨.yield searcher' (.rejected ..), hps⟩ =>
@@ -590,7 +590,7 @@ instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
           by simp [hps.isPlausibleSuccessor_of_skip]⟩)
       | ⟨.done, _⟩ =>
         if currPos ≠ s.startPos then
-          let slice := s.replaceEnd currPos
+          let slice := s.sliceTo currPos
           pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
           pure (.deflate ⟨.done, by simp⟩)
@@ -672,7 +672,7 @@ Examples:
 -/
 @[inline]
 def dropSuffix? (s : Slice) (pat : ρ) [BackwardPattern pat] : Option Slice :=
-  (BackwardPattern.dropSuffix? pat s).map s.replaceEnd
+  (BackwardPattern.dropSuffix? pat s).map s.sliceTo
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -705,7 +705,7 @@ Examples:
 -/
 @[inline]
 def dropEnd (s : Slice) (n : Nat) : Slice :=
-  s.replaceEnd (s.endPos.prevn n)
+  s.sliceTo (s.endPos.prevn n)
 
 /--
 Creates a new slice that contains the longest suffix of {name}`s` for which {name}`pat` matched
@@ -722,13 +722,13 @@ def dropEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice :=
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
-    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.replaceEnd curr) then
-      if Pos.ofReplaceEnd nextCurr < curr then
-        go (Pos.ofReplaceEnd nextCurr)
+    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then
+      if Pos.ofSliceTo nextCurr < curr then
+        go (Pos.ofSliceTo nextCurr)
       else
-        s.replaceEnd curr
+        s.sliceTo curr
     else
-      s.replaceEnd curr
+      s.sliceTo curr
   termination_by curr.down
 
 /--
@@ -762,7 +762,7 @@ Examples:
 -/
 @[inline]
 def takeEnd (s : Slice) (n : Nat) : Slice :=
-  s.replaceStart (s.endPos.prevn n)
+  s.sliceFrom (s.endPos.prevn n)
 
 /--
 Creates a new slice that contains the suffix prefix of {name}`s` for which {name}`pat` matched
@@ -781,13 +781,13 @@ def takeEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice :=
 where
   @[specialize pat]
   go (curr : s.Pos) : Slice :=
-    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.replaceEnd curr) then
-      if Pos.ofReplaceEnd nextCurr < curr then
-        go (Pos.ofReplaceEnd nextCurr)
+    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then
+      if Pos.ofSliceTo nextCurr < curr then
+        go (Pos.ofSliceTo nextCurr)
       else
-        s.replaceStart curr
+        s.sliceFrom curr
     else
-      s.replaceStart curr
+      s.sliceFrom curr
   termination_by curr.down
 
 /--

src/Init/Data/String/Slice.lean

@@ -98,7 +98,7 @@ where
     if nonempty && it' == it.2 then
       .error ⟨_, it'⟩ (.other "Expected a nonempty string")
     else
-      .success ⟨_, it'⟩ (it.1.replaceStartEnd! it.2 it').copy
+      .success ⟨_, it'⟩ (it.1.slice! it.2 it').copy
 
   /-- Parses a named attribute, and returns its name and value. -/
   namedAttr : Parser (String × String) := attempt do

src/Lean/ErrorExplanation.lean

@@ -42,7 +42,7 @@ private def addCommentAt (indent : Nat) (line : String) : String := Id.run do
     else
       -- The line was entirely ' ', and was shorter than the indentation level. No `--` added.
       return line
-  let remaining := line.replaceStart iter
+  let remaining := line.sliceFrom iter
   if remaining.all (· == ' ') then
     return line
   else

src/Lean/Server/FileWorker/ExampleHover.lean

@@ -41,7 +41,7 @@ protected def Parser.run (p : Parser α) (s : String) : Except String α :=
 Parses the given string.
 -/
 def pstring (s : String) : Parser String := fun it =>
-  if (it.1.replaceStart it.2).startsWith s then
+  if (it.1.sliceFrom it.2).startsWith s then
     .success ⟨_, it.2.nextn s.length⟩ s
   else
     .error it (.other s!"expected: {s}")