chore: minor String API improvements (#11439)

This PR performs minor maintenance on the String API

- Rename `String.Pos.toCopy` to `String.Pos.copy` to adhere to the
naming convention
- Rename `String.Pos.extract` to `String.extract` to get sane dot
notation again
- Add `String.Slice.Pos.extract`

Author: TwoFX

src/Init/Data/String/Basic.lean

@@ -824,16 +824,25 @@ The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-a
 
 If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.
 
+If possible, prefer `String.slice`, which avoids the allocation.
 -/
 @[extern "lean_string_utf8_extract"]
-def Pos.extract {s : @& String} (b e : @& s.Pos) : String where
+def extract {s : @& String} (b e : @& s.Pos) : String where
   toByteArray := s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx
   isValidUTF8 := b.isValidUTF8_extract e
 
+@[deprecated String.extract (since := "2025-12-01")]
+def Pos.extract {s : String} (b e : @& s.Pos) : String :=
+  s.extract b e
+
+@[simp]
+theorem toByteArray_extract {s : String} {b e : s.Pos} :
+    (s.extract b e).toByteArray = s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx := (rfl)
+
 /-- Creates a `String` from a `String.Slice` by copying the bytes. -/
 @[inline]
 def Slice.copy (s : Slice) : String :=
-  s.startInclusive.extract s.endExclusive
+  s.str.extract s.startInclusive s.endExclusive
 
 theorem Slice.toByteArray_copy {s : Slice} :
     s.copy.toByteArray = s.str.toByteArray.extract s.startInclusive.offset.byteIdx s.endExclusive.offset.byteIdx := (rfl)
@@ -1387,54 +1396,58 @@ theorem Pos.offset_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.offset = p
 
 /-- Given a slice `s` and a position on `s`, obtain the corresponding position on `s.copy.` -/
 @[inline]
-def Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos where
+def Slice.Pos.copy {s : Slice} (pos : s.Pos) : s.copy.Pos where
   offset := pos.offset
   isValid := Pos.Raw.isValid_copy_iff.2 pos.isValidForSlice
 
+@[deprecated Slice.Pos.copy (since := "2025-12-01")]
+def Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos :=
+  pos.copy
+
 @[simp]
-theorem Slice.Pos.offset_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.offset = pos.offset := (rfl)
+theorem Slice.Pos.offset_copy {s : Slice} {pos : s.Pos} : pos.copy.offset = pos.offset := (rfl)
 
 @[simp]
-theorem Slice.Pos.ofCopy_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.ofCopy = pos :=
+theorem Slice.Pos.ofCopy_copy {s : Slice} {pos : s.Pos} : pos.copy.ofCopy = pos :=
   Slice.Pos.ext (by simp)
 
 @[simp]
-theorem Pos.toCopy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.toCopy = pos :=
+theorem Pos.copy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.copy = pos :=
   Pos.ext (by simp)
 
 theorem Pos.ofCopy_inj {s : Slice} {pos pos' : s.copy.Pos} : pos.ofCopy = pos'.ofCopy ↔ pos = pos' :=
-  ⟨fun h => by simpa using congrArg Slice.Pos.toCopy h, (· ▸ rfl)⟩
+  ⟨fun h => by simpa using congrArg Slice.Pos.copy h, (· ▸ rfl)⟩
 
 @[simp]
-theorem Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.toCopy :=
+theorem Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.copy :=
   String.Pos.ext (by simp)
 
 @[simp]
-theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.toCopy :=
+theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.copy :=
   String.Pos.ext (by simp)
 
-theorem Slice.Pos.get_toCopy {s : Slice} {pos : s.Pos} (h) :
-    pos.toCopy.get h = pos.get (by rintro rfl; simp at h) := by
+theorem Slice.Pos.get_copy {s : Slice} {pos : s.Pos} (h) :
+    pos.copy.get h = pos.get (by rintro rfl; simp at h) := by
   rw [String.Pos.get, Slice.Pos.get_eq_utf8DecodeChar, Slice.Pos.get_eq_utf8DecodeChar]
-  simp only [str_toSlice, toByteArray_copy, startInclusive_toSlice, startPos_copy, offset_toCopy,
+  simp only [str_toSlice, toByteArray_copy, startInclusive_toSlice, startPos_copy, offset_copy,
     Slice.offset_startPos, Pos.Raw.byteIdx_zero, Pos.offset_toSlice, Nat.zero_add]
   rw [ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract]
   conv => lhs; congr; rw [ByteArray.extract_extract]
   conv => rhs; rw [ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract]
   exact ByteArray.utf8DecodeChar_extract_congr _ _ _
 
-theorem Slice.Pos.get_eq_get_toCopy {s : Slice} {pos : s.Pos} {h} :
-    pos.get h = pos.toCopy.get (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
-  (get_toCopy _).symm
+theorem Slice.Pos.get_eq_get_copy {s : Slice} {pos : s.Pos} {h} :
+    pos.get h = pos.copy.get (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
+  (get_copy _).symm
 
-theorem Slice.Pos.byte_toCopy {s : Slice} {pos : s.Pos} (h) :
-    pos.toCopy.byte h = pos.byte (by rintro rfl; simp at h) := by
+theorem Slice.Pos.byte_copy {s : Slice} {pos : s.Pos} (h) :
+    pos.copy.byte h = pos.byte (by rintro rfl; simp at h) := by
   rw [String.Pos.byte, Slice.Pos.byte, Slice.Pos.byte]
   simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]
 
-theorem Slice.Pos.byte_eq_byte_toCopy {s : Slice} {pos : s.Pos} {h} :
-    pos.byte h = pos.toCopy.byte (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
-  (byte_toCopy _).symm
+theorem Slice.Pos.byte_eq_byte_copy {s : Slice} {pos : s.Pos} {h} :
+    pos.byte h = pos.copy.byte (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
+  (byte_copy _).symm
 
 /-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`. -/
 @[inline]
@@ -1521,7 +1534,7 @@ theorem Slice.Pos.copy_eq_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.en
     ∃ t₁ t₂ : String, s.copy = t₁ ++ singleton (pos.get h) ++ t₂ ∧ t₁.utf8ByteSize = pos.offset.byteIdx := by
   obtain ⟨t₂, ht₂⟩ := (s.sliceFrom pos).copy.eq_singleton_append (by simpa [← Pos.ofCopy_inj, ← ofSliceFrom_inj])
   refine ⟨(s.sliceTo pos).copy, t₂, ?_, by simp⟩
-  simp only [Slice.startPos_copy, get_toCopy, get_eq_get_ofSliceFrom, ofSliceFrom_startPos] at ht₂
+  simp only [Slice.startPos_copy, get_copy, get_eq_get_ofSliceFrom, ofSliceFrom_startPos] at ht₂
   rw [append_assoc, ← ht₂, ← copy_eq_copy_sliceTo]
 
 theorem Slice.Pos.utf8ByteSize_byte {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} :
@@ -1751,8 +1764,8 @@ theorem Pos.offset_cast {s t : String} {pos : s.Pos} {h : s = t} :
 theorem Pos.cast_rfl {s : String} {pos : s.Pos} : pos.cast rfl = pos :=
   Pos.ext (by simp)
 
-theorem Pos.toCopy_toSlice_eq_cast {s : String} (p : s.Pos) :
-    p.toSlice.toCopy = p.cast copy_toSlice.symm :=
+theorem Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) :
+    p.toSlice.copy = p.cast copy_toSlice.symm :=
   Pos.ext (by simp)
 
 /-- Given a byte position within a string slice, obtains the smallest valid position that is
@@ -2435,6 +2448,35 @@ def Pos.slice! {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) :
     (s.slice! p₀ p₁).Pos :=
   Slice.Pos.slice! pos.toSlice _ _
 
+theorem extract_eq_copy_slice {s : String} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁) :
+    s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy := by
+  simp [← toByteArray_inj, Slice.toByteArray_copy]
+
+/--
+Copies a region of a slice to a new string.
+
+The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-allocated `String`.
+
+If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.
+
+If possible, prefer `Slice.slice`, which avoids the allocation.
+-/
+@[inline]
+def Slice.extract (s : Slice) (p₀ p₁ : s.Pos) : String :=
+  s.str.extract p₀.str p₁.str
+
+@[simp]
+theorem Slice.Pos.str_le_str_iff {s : Slice} {p q : s.Pos} : p.str ≤ q.str ↔ p ≤ q := by
+  simp [String.Pos.le_iff, Slice.Pos.le_iff, Pos.Raw.le_iff]
+
+@[simp]
+theorem Slice.Pos.str_lt_str_iff {s : Slice} {p q : s.Pos} : p.str < q.str ↔ p < q := by
+  simp [String.Pos.lt_iff, Slice.Pos.lt_iff, Pos.Raw.lt_iff]
+
+theorem Slice.extract_eq_copy_slice {s : Slice} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁) :
+    s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy := by
+  simp [← toByteArray_inj, Slice.toByteArray_copy, Slice.extract]
+
 /--
 Advances the position `p` `n` times.
 
@@ -2734,10 +2776,6 @@ where
     | [],    _, _ => []
     | c::cs, i, e => if i = e then [] else c :: go₂ cs (i + c) e
 
-@[extern "lean_string_utf8_extract", expose, deprecated Pos.Raw.extract (since := "2025-10-14")]
-def extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
-  | s, b, e => Pos.Raw.extract s b e
-
 def Pos.Raw.offsetOfPosAux (s : String) (pos : Pos.Raw) (i : Pos.Raw) (offset : Nat) : Nat :=
   if i >= pos then offset
   else if h : i.atEnd s then

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

@@ -40,7 +40,7 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
   simp [singleton]
 
 @[simp]
-theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂ := by
+theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂ := by
   simp [String.Pos.ext_iff, Pos.ext_iff]
 
 @[simp]

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

@@ -56,25 +56,25 @@ theorem Slice.Pos.Splits.cast {s₁ s₂ : Slice} {p : s₁.Pos} {t₁ t₂ : St
     p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂ :=
   splits_cast_iff.mpr
 
-theorem Slice.Pos.Splits.toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
-    (h : p.Splits t₁ t₂) : p.toCopy.Splits t₁ t₂ where
+theorem Slice.Pos.Splits.copy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
+    (h : p.Splits t₁ t₂) : p.copy.Splits t₁ t₂ where
   eq_append := h.eq_append
   offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
 
-theorem Slice.Pos.splits_of_splits_toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
-    (h : p.toCopy.Splits t₁ t₂) : p.Splits t₁ t₂ where
+theorem Slice.Pos.splits_of_splits_copy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
+    (h : p.copy.Splits t₁ t₂) : p.Splits t₁ t₂ where
   eq_append := h.eq_append
   offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
 
 @[simp]
-theorem Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} :
-    p.toCopy.Splits t₁ t₂ ↔ p.Splits t₁ t₂ :=
-  ⟨splits_of_splits_toCopy, (·.toCopy)⟩
+theorem Slice.Pos.splits_copy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} :
+    p.copy.Splits t₁ t₂ ↔ p.Splits t₁ t₂ :=
+  ⟨splits_of_splits_copy, (·.copy)⟩
 
 @[simp]
 theorem Pos.splits_toSlice_iff {s : String} {p : s.Pos} {t₁ t₂ : String} :
     p.toSlice.Splits t₁ t₂ ↔ p.Splits t₁ t₂ := by
-  rw [← Slice.Pos.splits_toCopy_iff, p.toCopy_toSlice_eq_cast, splits_cast_iff]
+  rw [← Slice.Pos.splits_copy_iff, p.copy_toSlice_eq_cast, splits_cast_iff]
 
 theorem Pos.Splits.toSlice {s : String} {p : s.Pos} {t₁ t₂ : String}
     (h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂ :=
@@ -112,15 +112,15 @@ theorem Pos.Splits.eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
 
 theorem Slice.Pos.Splits.eq_left {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ :=
-  (splits_toCopy_iff.2 h₁).eq_left (splits_toCopy_iff.2 h₂)
+  (splits_copy_iff.2 h₁).eq_left (splits_copy_iff.2 h₂)
 
 theorem Slice.Pos.Splits.eq_right {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ :=
-  (splits_toCopy_iff.2 h₁).eq_right (splits_toCopy_iff.2 h₂)
+  (splits_copy_iff.2 h₁).eq_right (splits_copy_iff.2 h₂)
 
 theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
-  (splits_toCopy_iff.2 h₁).eq (splits_toCopy_iff.2 h₂)
+  (splits_copy_iff.2 h₁).eq (splits_copy_iff.2 h₂)
 
 @[simp]
 theorem splits_endPos (s : String) : s.endPos.Splits s "" where
@@ -161,11 +161,11 @@ theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" where
 @[simp]
 theorem Slice.splits_endPos_iff {s : Slice} :
     s.endPos.Splits t₁ t₂ ↔ t₁ = s.copy ∧ t₂ = "" := by
-  rw [← Pos.splits_toCopy_iff, ← endPos_copy, String.splits_endPos_iff]
+  rw [← Pos.splits_copy_iff, ← endPos_copy, String.splits_endPos_iff]
 
 theorem Slice.Pos.Splits.eq_endPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
     p = s.endPos ↔ t₂ = "" := by
-  rw [← toCopy_inj, ← endPos_copy, h.toCopy.eq_endPos_iff]
+  rw [← copy_inj, ← endPos_copy, h.copy.eq_endPos_iff]
 
 @[simp]
 theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
@@ -175,11 +175,11 @@ theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
 @[simp]
 theorem Slice.splits_startPos_iff {s : Slice} :
     s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s.copy := by
-  rw [← Pos.splits_toCopy_iff, ← startPos_copy, String.splits_startPos_iff]
+  rw [← Pos.splits_copy_iff, ← startPos_copy, String.splits_startPos_iff]
 
 theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
     p = s.startPos ↔ t₁ = "" := by
-  rw [← toCopy_inj, ← startPos_copy, h.toCopy.eq_startPos_iff]
+  rw [← copy_inj, ← startPos_copy, h.copy.eq_startPos_iff]
 
 theorem Pos.splits_next_right {s : String} (p : s.Pos) (hp : p ≠ s.endPos) :
     p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where

src/Init/Data/String/Termination.lean

@@ -223,13 +223,13 @@ end Pos
 namespace Slice.Pos
 
 @[simp]
-theorem remainingBytes_toCopy {s : Slice} {p : s.Pos} :
-    p.toCopy.remainingBytes = p.remainingBytes := by
+theorem remainingBytes_copy {s : Slice} {p : s.Pos} :
+    p.copy.remainingBytes = p.remainingBytes := by
   simp [remainingBytes_eq, String.Pos.remainingBytes_eq, Slice.utf8ByteSize_eq]
 
 theorem Splits.remainingBytes_eq {s : Slice} {p : s.Pos} {t₁ t₂} (h : p.Splits t₁ t₂) :
     p.remainingBytes = t₂.utf8ByteSize := by
-  simpa using h.toCopy.remainingBytes_eq
+  simpa using h.copy.remainingBytes_eq
 
 end Slice.Pos
 

src/Lean/DocString/Links.lean

@@ -124,7 +124,7 @@ def rewriteManualLinksCore (s : String) : Id (Array (Lean.Syntax.Range × String
       iter' := iter'.next h'
       if urlChar c' && ¬iter'.IsAtEnd then
         continue
-      match rw (start.extract pre') with
+      match rw (s.extract start pre') with
       | .error err =>
         errors := errors.push (⟨pre.offset, pre'.offset⟩, err)
         out := out.push c

src/Lean/Server/FileWorker/ExampleHover.lean

@@ -59,11 +59,11 @@ private def lines (s : String) : Array String := Id.run do
     let c := iter.get h
     iter := iter.next h
     if c == '\n' then
-      result := result.push <| lineStart.extract iter
+      result := result.push <| s.extract lineStart iter
       lineStart := iter
 
   if iter != lineStart then
-    result := result.push <| lineStart.extract iter
+    result := result.push <| s.extract lineStart iter
   return result
 
 private inductive RWState where

src/lake/Lake/CLI/Main.lean

@@ -196,7 +196,7 @@ def setConfigOpt (kvPair : String) : CliM PUnit :=
     if h : pos.IsAtEnd then
       (kvPair.toName, "")
     else
-      (kvPair.startPos.extract pos |>.toName, (pos.next h).extract kvPair.endPos)
+      (kvPair.extract kvPair.startPos pos |>.toName, kvPair.extract (pos.next h) kvPair.endPos)
   modifyThe LakeOptions fun opts =>
     {opts with configOpts := opts.configOpts.insert key val}
 

src/lake/Lake/Config/Artifact.lean

@@ -56,9 +56,9 @@ public def ofFilePath? (path : FilePath) : Except String ArtifactDescr := do
       | throw "expected artifact file name to be a content hash"
     return {hash, ext := ""}
   else
-    let some hash := Hash.ofString? <| s.startPos.extract pos
+    let some hash := Hash.ofString? <| s.extract s.startPos pos
       | throw "expected artifact file name to be a content hash"
-    let ext := (pos.next h).extract s.endPos
+    let ext := s.extract (pos.next h) s.endPos
     return {hash, ext}
 
 public protected def fromJson? (data : Json) : Except String ArtifactDescr := do

src/lake/Lake/Util/Cli.lean

@@ -102,17 +102,17 @@ variable [Monad m] [MonadStateOf ArgList m]
   if h : pos = opt.endPos then
     handle opt
   else do
-    consArg <| (pos.next h).extract opt.endPos
-    handle <| opt.startPos.extract pos
+    consArg <| opt.extract (pos.next h) opt.endPos
+    handle <| opt.extract opt.startPos pos
 
 /-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
 @[inline] public def longOptionOrEq (handle : String → m α) (opt : String) : m α :=
   let pos := opt.find '='
   if h : pos = opt.endPos then
     handle opt
   else do
-    consArg <| (pos.next h).extract opt.endPos
-    handle <| opt.startPos.extract pos
+    consArg <| opt.extract (pos.next h) opt.endPos
+    handle <| opt.extract opt.startPos pos
 
 /-- Process a long option  of the form `--long`, `--long=arg`, `"--long arg"`. -/
 @[inline] public def longOption (handle : String → m α) : String → m α :=

src/lake/Lake/Util/Version.lean

@@ -88,7 +88,7 @@ def parseSpecialDescr? (s : String) : EStateM String s.Pos (Option String) := do
       let p := p.next h
       let p' := nextUntilWhitespace p
       set p'
-      let specialDescr := p.extract p'
+      let specialDescr := s.extract p p'
       return some specialDescr
     else
       return none
@@ -256,7 +256,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do
   let (origin, tag) :=
     if h : ¬colonPos.IsAtEnd then
       let pos := colonPos.next h
-      (ver.startPos.extract colonPos, pos.extract ver.endPos)
+      (ver.extract ver.startPos colonPos, ver.extract pos ver.endPos)
     else
       ("", ver)
   let noOrigin := origin.isEmpty