max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename String.ValidPos to String.Pos (#11240)

Browse source 
This PR renames `String.ValidPos` to `String.Pos`, `String.endValidPos`
to `String.endPos` and `String.startValidPos` to `String.startPos`.

Accordingly, the deprecations of `String.Pos` to `String.Pos.Raw` and
`String.endPos` to `String.rawEndPos` are removed early, after an
abbreviated deprecation cycle of two releases.
This commit is contained in:
Markus Himmel 2025-11-24 17:40:21 +01:00 • committed by GitHub
parent 6da35eeccb
commit fa67f300f6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
40 changed files with 569 additions and 569 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
script/Shake.lean
View file

@ -300,7 +300,7 @@ def parseHeaderFromString (text path : String) :
throw <| .userError "parse errors in file"
-- the insertion point for `add` is the first newline after the imports
let insertion := header.raw.getTailPos?.getD parserState.pos
let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
pure (path, inputCtx, header, insertion)
/-- Parse a source file to extract the location of the import lines, for edits and error messages.
@ -593,16 +593,16 @@ def main (args : List String) : IO UInt32 := do
for stx in imports do
let mod := decodeImport stx
if remove.contains mod || seen.contains mod then
out := out ++ text.extract pos stx.raw.getPos?.get!
out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
-- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
seen := seen.insert mod
out := out ++ text.extract pos insertion
out := out ++ String.Pos.Raw.extract text pos insertion
for mod in add do
if !seen.contains mod then
seen := seen.insert mod
out := out ++ s!"{mod}\n"
out := out ++ text.extract insertion text.rawEndPos
out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
IO.FS.writeFile path out
count := count + 1

403
src/Init/Data/String/Basic.lean
View file

@ -805,25 +805,20 @@ theorem Pos.Raw.isValid_iff_isValidUTF8_extract_utf8ByteSize {s : String} {p : P
· simp
· exact h₂.1
theorem ValidPos.isValidUTF8_extract {s : String} (pos₁ pos₂ : s.ValidPos) :
theorem Pos.isValidUTF8_extract {s : String} (pos₁ pos₂ : s.Pos) :
(s.bytes.extract pos₁.offset.byteIdx pos₂.offset.byteIdx).IsValidUTF8 := by
by_cases h : pos₁ ≤ pos₂
· exact (Pos.Raw.isValidUTF8_extract_iff _ _ h pos₂.isValid.le_rawEndPos).2 (Or.inr ⟨pos₁.isValid, pos₂.isValid⟩)
· rw [ByteArray.extract_eq_empty_iff.2]
· exact ByteArray.isValidUTF8_empty
· rw [Nat.min_eq_left]
· rw [ValidPos.le_iff, Pos.Raw.le_iff] at h
· rw [Pos.le_iff, Pos.Raw.le_iff] at h
omega
· have := Pos.Raw.le_iff.1 pos₂.isValid.le_rawEndPos
rwa [size_bytes, ← byteIdx_rawEndPos]
@[extern "lean_string_utf8_extract"]
def ValidPos.extract {s : @& String} (b e : @& s.ValidPos) : String where
bytes := s.bytes.extract b.offset.byteIdx e.offset.byteIdx
isValidUTF8 := b.isValidUTF8_extract e
@[extern "lean_string_utf8_extract"]
def Pos.extract {s : @& String} (b e : @& s.ValidPos) : String where
def Pos.extract {s : @& String} (b e : @& s.Pos) : String where
bytes := s.bytes.extract b.offset.byteIdx e.offset.byteIdx
isValidUTF8 := b.isValidUTF8_extract e
@ -869,7 +864,7 @@ theorem Pos.Raw.isValid_copy_iff {s : Slice} {p : Pos.Raw} :
· simpa using h₁
· have := s.startInclusive_le_endExclusive
simp_all only [Slice.rawEndPos_copy, le_iff, Slice.byteIdx_rawEndPos, Slice.utf8ByteSize_eq,
ValidPos.le_iff]
Pos.le_iff]
rw [Slice.bytes_copy, ByteArray.extract_extract, Nat.add_zero, Nat.min_eq_left (by omega)] at h₂
rw [← byteIdx_offsetBy, Pos.Raw.isValidUTF8_extract_iff] at h₂
· rcases h₂ with (h₂|⟨-, h₂⟩)
@ -882,7 +877,7 @@ theorem Pos.Raw.isValid_copy_iff {s : Slice} {p : Pos.Raw} :
omega
· simpa using h₁
· have := s.startInclusive_le_endExclusive
simp_all only [le_iff, Slice.byteIdx_rawEndPos, Slice.utf8ByteSize_eq, ValidPos.le_iff]
simp_all only [le_iff, Slice.byteIdx_rawEndPos, Slice.utf8ByteSize_eq, Pos.le_iff]
rw [Slice.bytes_copy, ByteArray.extract_extract, Nat.add_zero, Nat.min_eq_left (by omega)]
rw [← byteIdx_offsetBy, Pos.Raw.isValidUTF8_extract_iff]
· exact Or.inr ⟨s.startInclusive.isValid, h₂⟩
@ -974,7 +969,7 @@ theorem Slice.Pos.isUTF8FirstByte_byte {s : Slice} {pos : s.Pos} {h : pos ≠ s.
/-- Given a valid position on a slice `s`, obtains the corresponding valid position on the
underlying string `s.str`. -/
@[inline]
def Slice.Pos.str {s : Slice} (pos : s.Pos) : s.str.ValidPos where
def Slice.Pos.str {s : Slice} (pos : s.Pos) : s.str.Pos where
offset := pos.offset.offsetBy s.startInclusive.offset
isValid := pos.isValidForSlice.isValid_offsetBy
@ -988,7 +983,7 @@ theorem Slice.Pos.offset_str_le_offset_endExclusive {s : Slice} {pos : s.Pos} :
have := pos.isValidForSlice.le_rawEndPos
have := s.startInclusive_le_endExclusive
simp only [Pos.Raw.le_iff, byteIdx_rawEndPos, utf8ByteSize_eq, offset_str,
Pos.Raw.byteIdx_offsetBy, ValidPos.le_iff] at *
Pos.Raw.byteIdx_offsetBy, String.Pos.le_iff] at *
omega
theorem Slice.Pos.offset_le_offset_str {s : Slice} {pos : s.Pos} :
@ -1003,23 +998,23 @@ theorem Slice.Pos.offset_le_offset_endExclusive {s : Slice} {pos : s.Pos} :
@[simp]
theorem Slice.Pos.startInclusive_le_str {s : Slice} {pos : s.Pos} :
s.startInclusive ≤ pos.str := by
simp [ValidPos.le_iff, Pos.Raw.le_iff]
simp [String.Pos.le_iff, Pos.Raw.le_iff]
/--
Given a valid position on `s.str` which is within the bounds of the slice `s`, obtains the
corresponding valid position on `s`.
-/
@[inline]
def Slice.Pos.ofStr {s : Slice} (pos : s.str.ValidPos) (h₁ : s.startInclusive ≤ pos)
def Slice.Pos.ofStr {s : Slice} (pos : s.str.Pos) (h₁ : s.startInclusive ≤ pos)
(h₂ : pos ≤ s.endExclusive) : s.Pos where
offset := pos.offset.unoffsetBy s.startInclusive.offset
isValidForSlice := by
refine ⟨?_, Pos.Raw.offsetBy_unoffsetBy_of_le h₁ |>.symm ▸ pos.isValid⟩
simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
omega
@[simp]
theorem Slice.Pos.offset_ofStr {s : Slice} {pos : s.str.ValidPos} {h₁ h₂} :
theorem Slice.Pos.offset_ofStr {s : Slice} {pos : s.str.Pos} {h₁ h₂} :
(ofStr pos h₁ h₂).offset = pos.offset.unoffsetBy s.startInclusive.offset := (rfl)
/-- Given a slice and a valid position within the slice, obtain a new slice on the same underlying
@ -1054,7 +1049,7 @@ def Slice.sliceTo (s : Slice) (pos : s.Pos) : Slice where
str := s.str
startInclusive := s.startInclusive
endExclusive := pos.str
startInclusive_le_endExclusive := by simp [ValidPos.le_iff, String.Pos.Raw.le_iff]
startInclusive_le_endExclusive := by simp [String.Pos.le_iff, String.Pos.Raw.le_iff]
@[deprecated Slice.sliceTo (since := "2025-11-20")]
def Slice.replaceEnd (s : Slice) (pos : s.Pos) : Slice :=
@ -1080,7 +1075,7 @@ def Slice.slice (s : Slice) (newStart newEnd : s.Pos)
str := s.str
startInclusive := newStart.str
endExclusive := newEnd.str
startInclusive_le_endExclusive := by simpa [ValidPos.le_iff, Pos.Raw.le_iff] using h
startInclusive_le_endExclusive := by simpa [String.Pos.le_iff, Pos.Raw.le_iff] using h
@[deprecated Slice.slice (since := "2025-11-20")]
def Slice.replaceStartEnd (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : Slice :=
@ -1214,17 +1209,17 @@ theorem Pos.Raw.IsValidForSlice.ofSlice {s : String} {p : Pos.Raw} (h : p.IsVali
/-- Turns a valid position on the string `s` into a valid position on the slice `s.toSlice`. -/
@[inline, expose]
def ValidPos.toSlice {s : String} (pos : s.ValidPos) : s.toSlice.Pos where
def Pos.toSlice {s : String} (pos : s.Pos) : s.toSlice.Pos where
offset := pos.offset
isValidForSlice := pos.isValid.toSlice
@[simp]
theorem ValidPos.offset_toSlice {s : String} {pos : s.ValidPos} : pos.toSlice.offset = pos.offset := (rfl)
theorem Pos.offset_toSlice {s : String} {pos : s.Pos} : pos.toSlice.offset = pos.offset := (rfl)
/-- Given a string `s`, turns a valid position on the slice `s.toSlice` into a valid position on the
string `s`. -/
@[inline, expose]
def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.ValidPos where
def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.Pos where
offset := pos.offset
isValid := pos.isValidForSlice.ofSlice
@ -1236,16 +1231,16 @@ theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos := by
rw [← Slice.rawEndPos_copy, copy_toSlice]
@[simp]
theorem endPos_toSlice {s : String} : s.toSlice.endPos = s.endValidPos.toSlice :=
theorem endPos_toSlice {s : String} : s.toSlice.endPos = s.endPos.toSlice :=
Slice.Pos.ext (by simp)
@[simp]
theorem startPos_toSlice {s : String} : s.toSlice.startPos = s.startValidPos.toSlice :=
theorem startPos_toSlice {s : String} : s.toSlice.startPos = s.startPos.toSlice :=
Slice.Pos.ext (by simp)
@[simp]
theorem ValidPos.ofSlice_toSlice {s : String} (pos : s.ValidPos) : pos.toSlice.ofSlice = pos :=
ValidPos.ext (by simp)
theorem Pos.ofSlice_toSlice {s : String} (pos : s.Pos) : pos.toSlice.ofSlice = pos :=
Pos.ext (by simp)
@[simp]
theorem Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSlice.toSlice = pos :=
@ -1253,35 +1248,35 @@ theorem Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSli
@[simp]
theorem Slice.Pos.toSlice_comp_ofSlice {s : String} :
ValidPos.toSlice ∘ (ofSlice (s := s)) = id := by ext; simp
Pos.toSlice ∘ (ofSlice (s := s)) = id := by ext; simp
@[simp]
theorem ValidPos.ofSlice_comp_toSlice {s : String} :
theorem Pos.ofSlice_comp_toSlice {s : String} :
Slice.Pos.ofSlice ∘ (toSlice (s := s)) = id := by ext; simp
theorem ValidPos.toSlice_inj {s : String} {p q : s.ValidPos} : p.toSlice = q.toSlice ↔ p = q :=
theorem Pos.toSlice_inj {s : String} {p q : s.Pos} : p.toSlice = q.toSlice ↔ p = q :=
⟨fun h => by simpa using congrArg Slice.Pos.ofSlice h, (· ▸ rfl)⟩
theorem Slice.Pos.ofSlice_inj {s : String} {p q : s.toSlice.Pos} : p.ofSlice = q.ofSlice ↔ p = q :=
⟨fun h => by simpa using congrArg ValidPos.toSlice h, (· ▸ rfl)⟩
⟨fun h => by simpa using congrArg Pos.toSlice h, (· ▸ rfl)⟩
@[simp]
theorem ValidPos.toSlice_le {s : String} {p q : s.ValidPos} : p.toSlice ≤ q.toSlice ↔ p ≤ q := by
theorem Pos.toSlice_le {s : String} {p q : s.Pos} : p.toSlice ≤ q.toSlice ↔ p ≤ q := by
simp [le_iff, Slice.Pos.le_iff]
@[simp]
theorem Slice.Pos.ofSlice_le {s : String} {p q : s.toSlice.Pos} :
p.ofSlice ≤ q.ofSlice ↔ p ≤ q := by
simp [ValidPos.le_iff, le_iff]
simp [String.Pos.le_iff, le_iff]
@[simp]
theorem ValidPos.toSlice_lt {s : String} {p q : s.ValidPos} : p.toSlice < q.toSlice ↔ p < q := by
theorem Pos.toSlice_lt {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q := by
simp [lt_iff, Slice.Pos.lt_iff]
@[simp]
theorem Slice.Pos.ofSlice_lt {s : String} {p q : s.toSlice.Pos} :
p.ofSlice < q.ofSlice ↔ p < q := by
simp [ValidPos.lt_iff, lt_iff]
simp [String.Pos.lt_iff, lt_iff]
/--
Returns the character at the position `pos` of a string, taking a proof that `p` is not the
@ -1294,7 +1289,7 @@ Examples:
* `("L∃∀N".pos ⟨1⟩ (by decide)).get (by decide) = '∃'`
-/
@[inline, expose]
def ValidPos.get {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : Char :=
def Pos.get {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : Char :=
pos.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h]))
/--
@ -1304,7 +1299,7 @@ past-the-end position.
This function is overridden with an efficient implementation in runtime code.
-/
@[inline, expose]
def ValidPos.get? {s : String} (pos : s.ValidPos) : Option Char :=
def Pos.get? {s : String} (pos : s.Pos) : Option Char :=
pos.toSlice.get?
/--
@ -1314,23 +1309,23 @@ past-the-end position.
This function is overridden with an efficient implementation in runtime code.
-/
@[inline, expose]
def ValidPos.get! {s : String} (pos : s.ValidPos) : Char :=
def Pos.get! {s : String} (pos : s.Pos) : Char :=
pos.toSlice.get!
/--
Returns the byte at the position `pos` of a string.
-/
@[inline, expose]
def ValidPos.byte {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : UInt8 :=
def Pos.byte {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 :=
pos.toSlice.byte (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h]))
theorem ValidPos.isUTF8FirstByte_byte {s : String} {pos : s.ValidPos} {h : pos ≠ s.endValidPos} :
theorem Pos.isUTF8FirstByte_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} :
(pos.byte h).IsUTF8FirstByte :=
Slice.Pos.isUTF8FirstByte_byte
@[simp]
theorem startValidPos_eq_endValidPos_iff {b : String} : b.startValidPos = b.endValidPos ↔ b = "" := by
simp [← utf8ByteSize_eq_zero_iff, ValidPos.ext_iff, Eq.comm (b := b.rawEndPos)]
theorem startPos_eq_endPos_iff {b : String} : b.startPos = b.endPos ↔ b = "" := by
simp [← utf8ByteSize_eq_zero_iff, Pos.ext_iff, Eq.comm (b := b.rawEndPos)]
theorem isSome_utf8DecodeChar?_zero {b : String} (hb : b ≠ "") : (b.bytes.utf8DecodeChar? 0).isSome := by
refine (((Pos.Raw.isValid_iff_isSome_utf8DecodeChar? (s := b)).1 Pos.Raw.isValid_zero).elim ?_ id)
@ -1349,19 +1344,19 @@ theorem head_data {b : String} {h} :
b.toList.head h = b.bytes.utf8DecodeChar 0 (isSome_utf8DecodeChar?_zero (by simpa using h)) :=
head_toList
theorem get_startValidPos {b : String} (h) :
b.startValidPos.get h = b.toList.head (by rwa [ne_eq, toList_eq_nil_iff, ← startValidPos_eq_endValidPos_iff]) :=
theorem get_startPos {b : String} (h) :
b.startPos.get h = b.toList.head (by rwa [ne_eq, toList_eq_nil_iff, ← startPos_eq_endPos_iff]) :=
head_toList.symm
theorem eq_singleton_append {s : String} (h : s.startValidPos ≠ s.endValidPos) :
∃ t, s = singleton (s.startValidPos.get h) ++ t := by
theorem eq_singleton_append {s : String} (h : s.startPos ≠ s.endPos) :
∃ t, s = singleton (s.startPos.get h) ++ t := by
obtain ⟨m, rfl⟩ := s.exists_eq_ofList
have hm : m ≠ [] := by
rwa [ne_eq, ← String.ofList_eq_empty_iff, ← startValidPos_eq_endValidPos_iff]
rwa [ne_eq, ← String.ofList_eq_empty_iff, ← startPos_eq_endPos_iff]
refine ⟨ofList m.tail, ?_⟩
rw (occs := [1]) [← List.cons_head_tail hm]
rw [← List.singleton_append, String.ofList_append, append_left_inj, ← singleton_eq_ofList,
get_startValidPos]
get_startPos]
simp
theorem Slice.copy_eq_copy_sliceTo {s : Slice} {pos : s.Pos} :
@ -1375,16 +1370,16 @@ theorem Slice.copy_eq_copy_sliceTo {s : Slice} {pos : s.Pos} :
/-- Given a slice `s` and a position on `s.copy`, obtain the corresponding position on `s`. -/
@[inline]
def ValidPos.ofCopy {s : Slice} (pos : s.copy.ValidPos) : s.Pos where
def Pos.ofCopy {s : Slice} (pos : s.copy.Pos) : s.Pos where
offset := pos.offset
isValidForSlice := Pos.Raw.isValid_copy_iff.1 pos.isValid
@[simp]
theorem ValidPos.offset_ofCopy {s : Slice} {pos : s.copy.ValidPos} : pos.ofCopy.offset = pos.offset := (rfl)
theorem Pos.offset_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.offset = pos.offset := (rfl)
/-- 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.ValidPos where
def Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos where
offset := pos.offset
isValid := Pos.Raw.isValid_copy_iff.2 pos.isValidForSlice
@ -1396,41 +1391,41 @@ theorem Slice.Pos.ofCopy_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.ofCopy =
Slice.Pos.ext (by simp)
@[simp]
theorem ValidPos.toCopy_ofCopy {s : Slice} {pos : s.copy.ValidPos} : pos.ofCopy.toCopy = pos :=
ValidPos.ext (by simp)
theorem Pos.toCopy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.toCopy = pos :=
Pos.ext (by simp)
theorem ValidPos.ofCopy_inj {s : Slice} {pos pos' : s.copy.ValidPos} : pos.ofCopy = pos'.ofCopy ↔ pos = pos' :=
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)⟩
@[simp]
theorem Slice.startValidPos_copy {s : Slice} : s.copy.startValidPos = s.startPos.toCopy :=
ValidPos.ext (by simp)
theorem Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.toCopy :=
String.Pos.ext (by simp)
@[simp]
theorem Slice.endValidPos_copy {s : Slice} : s.copy.endValidPos = s.endPos.toCopy :=
ValidPos.ext (by simp)
theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.toCopy :=
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
rw [ValidPos.get, Slice.Pos.get_eq_utf8DecodeChar, Slice.Pos.get_eq_utf8DecodeChar]
simp only [str_toSlice, bytes_copy, startInclusive_toSlice, startValidPos_copy, offset_toCopy,
Slice.offset_startPos, Pos.Raw.byteIdx_zero, ValidPos.offset_toSlice, Nat.zero_add]
rw [String.Pos.get, Slice.Pos.get_eq_utf8DecodeChar, Slice.Pos.get_eq_utf8DecodeChar]
simp only [str_toSlice, bytes_copy, startInclusive_toSlice, startPos_copy, offset_toCopy,
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 ValidPos.ofCopy (by simp [h])) :=
pos.get h = pos.toCopy.get (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(get_toCopy _).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
rw [ValidPos.byte, Slice.Pos.byte, Slice.Pos.byte]
rw [String.Pos.byte, Slice.Pos.byte, Slice.Pos.byte]
simp [getUTF8Byte, String.getUTF8Byte, bytes_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 ValidPos.ofCopy (by simp [h])) :=
pos.byte h = pos.toCopy.byte (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(byte_toCopy _).symm
/-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`. -/
@ -1516,16 +1511,16 @@ theorem Slice.Pos.offset_sliceTo {s : Slice} {p₀ : s.Pos} {pos : s.Pos} {h : p
theorem Slice.Pos.copy_eq_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) :
∃ 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 [← ValidPos.ofCopy_inj, ← ofSliceFrom_inj])
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.startValidPos_copy, get_toCopy, get_eq_get_ofSliceFrom, ofSliceFrom_startPos] at ht₂
simp only [Slice.startPos_copy, get_toCopy, 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} :
(pos.byte h).utf8ByteSize pos.isUTF8FirstByte_byte = (pos.get h).utf8Size := by
simp [getUTF8Byte, byte, String.getUTF8Byte, get_eq_utf8DecodeChar, ByteArray.utf8Size_utf8DecodeChar]
theorem ValidPos.utf8ByteSize_byte {s : String} {pos : s.ValidPos} {h : pos ≠ s.endValidPos} :
theorem Pos.utf8ByteSize_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} :
(pos.byte h).utf8ByteSize pos.isUTF8FirstByte_byte = (pos.get h).utf8Size :=
Slice.Pos.utf8ByteSize_byte
@ -1665,60 +1660,60 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
/-- Advances a valid position on a string to the next valid position, given a proof that the
position is not the past-the-end position, which guarantees that such a position exists. -/
@[expose, extern "lean_string_utf8_next_fast"]
def ValidPos.next {s : @& String} (pos : @& s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
(Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
@[simp]
theorem Slice.Pos.str_inj {s : Slice} (p₁ p₂ : s.Pos) : p₁.str = p₂.str ↔ p₁ = p₂ := by
simp [Slice.Pos.ext_iff, ValidPos.ext_iff, Pos.Raw.ext_iff]
simp [Slice.Pos.ext_iff, String.Pos.ext_iff, Pos.Raw.ext_iff]
@[expose, extern "lean_string_utf8_next_fast"]
def Pos.next {s : @& String} (pos : @& s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
def String.Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
(Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
/-- Advances a valid position on a string to the next valid position, or returns `none` if the
given position is the past-the-end position. -/
@[inline, expose]
def ValidPos.next? {s : String} (pos : s.ValidPos) : Option s.ValidPos :=
def Pos.next? {s : String} (pos : s.Pos) : Option s.Pos :=
pos.toSlice.next?.map Slice.Pos.ofSlice
/-- Advances a valid position on a string to the next valid position, or panics if the given
position is the past-the-end position. -/
@[inline, expose]
def ValidPos.next! {s : String} (pos : s.ValidPos) : s.ValidPos :=
def Pos.next! {s : String} (pos : s.Pos) : s.Pos :=
pos.toSlice.next!.ofSlice
/-- Returns the previous valid position before the given position, given a proof that the position
is not the start position, which guarantees that such a position exists. -/
@[inline, expose]
def ValidPos.prev {s : String} (pos : s.ValidPos) (h : pos ≠ s.startValidPos) : s.ValidPos :=
def Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos :=
(pos.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
/-- Returns the previous valid position before the given position, or `none` if the position is
the start position. -/
@[inline, expose]
def ValidPos.prev? {s : String} (pos : s.ValidPos) : Option s.ValidPos :=
def Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos :=
pos.toSlice.prev?.map Slice.Pos.ofSlice
/-- Returns the previous valid position before the given position, or panics if the position is
the start position. -/
@[inline, expose]
def ValidPos.prev! {s : String} (pos : s.ValidPos) : s.ValidPos :=
def Pos.prev! {s : String} (pos : s.Pos) : s.Pos :=
pos.toSlice.prev!.ofSlice
/-- Constructs a valid position on `s` from a position and a proof that it is valid. -/
@[inline, expose]
def pos (s : String) (off : Pos.Raw) (h : off.IsValid s) : s.ValidPos :=
def pos (s : String) (off : Pos.Raw) (h : off.IsValid s) : s.Pos :=
(s.toSlice.pos off h.toSlice).ofSlice
/-- Constructs a valid position on `s` from a position, returning `none` if the position is not valid. -/
@[inline, expose]
def pos? (s : String) (off : Pos.Raw) : Option s.ValidPos :=
def pos? (s : String) (off : Pos.Raw) : Option s.Pos :=
(s.toSlice.pos? off).map Slice.Pos.ofSlice
/-- Constructs a valid position `s` from a position, panicking if the position is not valid. -/
@[inline, expose]
def pos! (s : String) (off : Pos.Raw) : s.ValidPos :=
def pos! (s : String) (off : Pos.Raw) : s.Pos :=
(s.toSlice.pos! off).ofSlice
@[simp]
@ -1740,21 +1735,21 @@ theorem Slice.Pos.cast_rfl {s : Slice} {pos : s.Pos} : pos.cast rfl = pos :=
/-- Constructs a valid position on `t` from a valid position on `s` and a proof that `s = t`. -/
@[inline]
def ValidPos.cast {s t : String} (pos : s.ValidPos) (h : s = t) : t.ValidPos where
def Pos.cast {s t : String} (pos : s.Pos) (h : s = t) : t.Pos where
offset := pos.offset
isValid := h ▸ pos.isValid
@[simp]
theorem ValidPos.offset_cast {s t : String} {pos : s.ValidPos} {h : s = t} :
theorem Pos.offset_cast {s t : String} {pos : s.Pos} {h : s = t} :
(pos.cast h).offset = pos.offset := (rfl)
@[simp]
theorem ValidPos.cast_rfl {s : String} {pos : s.ValidPos} : pos.cast rfl = pos :=
ValidPos.ext (by simp)
theorem Pos.cast_rfl {s : String} {pos : s.Pos} : pos.cast rfl = pos :=
Pos.ext (by simp)
theorem ValidPos.toCopy_toSlice_eq_cast {s : String} (p : s.ValidPos) :
theorem Pos.toCopy_toSlice_eq_cast {s : String} (p : s.Pos) :
p.toSlice.toCopy = p.cast copy_toSlice.symm :=
ValidPos.ext (by simp)
Pos.ext (by simp)
/-- Given a byte position within a string slice, obtains the smallest valid position that is
strictly greater than the given byte position. -/
@ -1818,10 +1813,10 @@ theorem Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.en
simpa [Pos.ext_iff, prev] using Pos.Raw.ne_of_lt prevAux_lt_rawEndPos
@[simp]
theorem ValidPos.prev_ne_endValidPos {s : String} {p : s.ValidPos} {h} : p.prev h ≠ s.endValidPos :=
theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg (·.ofSlice)) h))
theorem ValidPos.toSlice_prev {s : String} {p : s.ValidPos} {h} :
theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} :
(p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
simp [prev]
@ -1833,7 +1828,7 @@ theorem Slice.Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p :=
lt_iff.2 offset_prev_lt_offset
@[simp]
theorem ValidPos.prev_lt {s : String} {p : s.ValidPos} {h} : p.prev h < p := by
theorem Pos.prev_lt {s : String} {p : s.Pos} {h} : p.prev h < p := by
simp [← toSlice_lt, toSlice_prev]
@ -1853,8 +1848,8 @@ fallback value `(default : Char)`, which is `'A'`, but does not panic.
This function is overridden with an efficient implementation in runtime code. See
`String.Pos.Raw.utf8GetAux` for the reference implementation.
This is a legacy function. The recommended alternative is `String.ValidPos.get`, combined with
`String.pos` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos` or another means of obtaining a `String.Pos`.
Examples:
* `"abc".get ⟨1⟩ = 'b'`
@ -1884,8 +1879,8 @@ Returns the character at position `p` of a string. If `p` is not a valid positio
This function is overridden with an efficient implementation in runtime code. See
`String.utf8GetAux?` for the reference implementation.
This is a legacy function. The recommended alternative is `String.ValidPos.get`, combined with
`String.pos?` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos?` or another means of obtaining a `String.Pos`.
Examples:
* `"abc".get? ⟨1⟩ = some 'b'`
@ -1904,13 +1899,13 @@ def get? : (@& String) → (@& Pos.Raw) → Option Char
/--
Returns the character at position `p` of a string. Panics if `p` is not a valid position.
See `String.pos?` and `String.ValidPos.get` for a safer alternative.
See `String.pos?` and `String.Pos.get` for a safer alternative.
This function is overridden with an efficient implementation in runtime code. See
`String.utf8GetAux` for the reference implementation.
This is a legacy function. The recommended alternative is `String.ValidPos.get`, combined with
`String.pos!` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos!` or another means of obtaining a `String.Pos`.
Examples
* `"abc".get! ⟨1⟩ = 'b'`
@ -1936,48 +1931,48 @@ abbrev utf8SetAux (c' : Char) : List Char → Pos.Raw → Pos.Raw → List Char
Pos.Raw.utf8SetAux c'
@[simp]
theorem ValidPos.get_toSlice {s : String} {p : s.ValidPos} {h} :
theorem Pos.get_toSlice {s : String} {p : s.Pos} {h} :
p.toSlice.get h = p.get (ne_of_apply_ne (·.toSlice) (by simp_all)) := by
rfl
theorem ValidPos.get_eq_get_toSlice {s : String} {p : s.ValidPos} {h} :
theorem Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h} :
p.get h = p.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) := rfl
@[simp]
theorem ValidPos.offset_next {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) :
theorem Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
(p.next h).offset = p.offset + p.get h := by
simp [next]
theorem ValidPos.byteIdx_offset_next {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) :
theorem Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
(p.next h).offset.byteIdx = p.offset.byteIdx + (p.get h).utf8Size := by
simp
theorem ValidPos.toSlice_next {s : String} {p : s.ValidPos} {h} :
theorem Pos.toSlice_next {s : String} {p : s.Pos} {h} :
(p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
simp [next]
theorem ValidPos.byteIdx_lt_utf8ByteSize {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) :
theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
p.offset.byteIdx < s.utf8ByteSize := by
have := byteIdx_rawEndPos ▸ Pos.Raw.le_iff.1 p.isValid.le_rawEndPos
simp only [ne_eq, ValidPos.ext_iff, offset_endValidPos, Pos.Raw.ext_iff, byteIdx_rawEndPos] at h
simp only [ne_eq, Pos.ext_iff, offset_endPos, Pos.Raw.ext_iff, byteIdx_rawEndPos] at h
omega
@[simp]
theorem ValidPos.lt_next {s : String} {p : s.ValidPos} {h} : p < p.next h := by
simp [← ValidPos.toSlice_lt, toSlice_next]
theorem Pos.lt_next {s : String} {p : s.Pos} {h} : p < p.next h := by
simp [← Pos.toSlice_lt, toSlice_next]
theorem ValidPos.ne_startPos_of_lt {s : String} {p q : s.ValidPos} :
p < q → q ≠ s.startValidPos := by
simp only [lt_iff, Pos.Raw.lt_iff, ne_eq, ValidPos.ext_iff, offset_startValidPos, Pos.Raw.ext_iff,
theorem Pos.ne_startPos_of_lt {s : String} {p q : s.Pos} :
p < q → q ≠ s.startPos := by
simp only [lt_iff, Pos.Raw.lt_iff, ne_eq, Pos.ext_iff, offset_startPos, Pos.Raw.ext_iff,
Pos.Raw.byteIdx_zero]
omega
theorem ValidPos.next_ne_startValidPos {s : String} {p : s.ValidPos} {h} :
p.next h ≠ s.startValidPos :=
theorem Pos.next_ne_startPos {s : String} {p : s.Pos} {h} :
p.next h ≠ s.startPos :=
ne_startPos_of_lt p.lt_next
@[simp]
theorem ValidPos.str_toSlice {s : String} {p : s.ValidPos} : p.toSlice.str = p := by
theorem Pos.str_toSlice {s : String} {p : s.Pos} : p.toSlice.str = p := by
ext
simp
@ -1985,41 +1980,41 @@ theorem Slice.Pos.str_le_endExclusive {s : Slice} (p : s.Pos) :
p.str ≤ s.endExclusive := by
have := p.isValidForSlice.le_utf8ByteSize
have := s.startInclusive_le_endExclusive
simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
omega
theorem ValidPos.lt_of_le_of_ne {s : String} {p q : s.ValidPos} :
theorem Pos.lt_of_le_of_ne {s : String} {p q : s.Pos} :
p ≤ q → p ≠ q → p < q := by
simp [ValidPos.le_iff, ValidPos.lt_iff, ValidPos.ext_iff, Pos.Raw.le_iff, Pos.Raw.lt_iff,
simp [Pos.le_iff, Pos.lt_iff, Pos.ext_iff, Pos.Raw.le_iff, Pos.Raw.lt_iff,
Pos.Raw.ext_iff]
omega
@[simp]
theorem Slice.Pos.str_endPos {s : Slice} : s.endPos.str = s.endExclusive := by
simp [ValidPos.ext_iff]
simp [String.Pos.ext_iff]
theorem Slice.Pos.str_lt_endExclusive {s : Slice} (p : s.Pos) (h : p ≠ s.endPos) :
p.str < s.endExclusive :=
ValidPos.lt_of_le_of_ne p.str_le_endExclusive (by rwa [← str_endPos, ne_eq, str_inj])
Pos.lt_of_le_of_ne p.str_le_endExclusive (by rwa [← str_endPos, ne_eq, str_inj])
theorem ValidPos.ne_of_lt {s : String} {p q : s.ValidPos} : p < q → p ≠ q := by
simpa [ValidPos.lt_iff, ValidPos.ext_iff] using Pos.Raw.ne_of_lt
theorem Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q := by
simpa [Pos.lt_iff, Pos.ext_iff] using Pos.Raw.ne_of_lt
theorem ValidPos.lt_of_lt_of_le {s : String} {p q r : s.ValidPos} : p < q → q ≤ r → p < r := by
simpa [ValidPos.lt_iff, ValidPos.le_iff] using Pos.Raw.lt_of_lt_of_le
theorem Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
simpa [Pos.lt_iff, Pos.le_iff] using Pos.Raw.lt_of_lt_of_le
theorem ValidPos.le_endValidPos {s : String} (p : s.ValidPos) : p ≤ s.endValidPos := by
simpa [ValidPos.le_iff] using p.isValid.le_rawEndPos
theorem Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos := by
simpa [Pos.le_iff] using p.isValid.le_rawEndPos
theorem Slice.Pos.str_ne_endValidPos {s : Slice} (p : s.Pos) (h : p ≠ s.endPos) :
p.str ≠ s.str.endValidPos :=
ValidPos.ne_of_lt (ValidPos.lt_of_lt_of_le (p.str_lt_endExclusive h) (ValidPos.le_endValidPos _))
theorem Slice.Pos.str_ne_endPos {s : Slice} (p : s.Pos) (h : p ≠ s.endPos) :
p.str ≠ s.str.endPos :=
Pos.ne_of_lt (Pos.lt_of_lt_of_le (p.str_lt_endExclusive h) (Pos.le_endPos _))
theorem ValidPos.le_trans {s : String} {p q r : s.ValidPos} : p ≤ q → q ≤ r → p ≤ r := by
simpa [ValidPos.le_iff] using Pos.Raw.le_trans
theorem Pos.le_trans {s : String} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r := by
simpa [Pos.le_iff] using Pos.Raw.le_trans
theorem ValidPos.le_of_lt {s : String} {p q : s.ValidPos} : p < q → p ≤ q := by
simpa [ValidPos.le_iff, ValidPos.lt_iff] using Pos.Raw.le_of_lt
theorem Pos.le_of_lt {s : String} {p q : s.Pos} : p < q → p ≤ q := by
simpa [Pos.le_iff, Pos.lt_iff] using Pos.Raw.le_of_lt
theorem Slice.Pos.le_of_not_lt {s : Slice} {p q : s.Pos} : ¬q < p → p ≤ q := by
simp [Slice.Pos.le_iff, Slice.Pos.lt_iff, Pos.Raw.le_iff, Pos.Raw.lt_iff]
@ -2057,26 +2052,26 @@ theorem Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h} : p < q → p.next
· have := (p.next h).str.isValid.le_utf8ByteSize
simpa [Nat.add_assoc] using this
theorem Slice.Pos.ofSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.ValidPos} :
theorem Slice.Pos.ofSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} :
p.ofSlice ≤ q ↔ p ≤ q.toSlice := Iff.rfl
@[simp]
theorem ValidPos.toSlice_lt_toSlice_iff {s : String} {p q : s.ValidPos} :
theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} :
p.toSlice < q.toSlice ↔ p < q := Iff.rfl
theorem ValidPos.next_le_of_lt {s : String} {p q : s.ValidPos} {h} : p < q → p.next h ≤ q := by
rw [next, Slice.Pos.ofSlice_le_iff, ← ValidPos.toSlice_lt_toSlice_iff]
theorem Pos.next_le_of_lt {s : String} {p q : s.Pos} {h} : p < q → p.next h ≤ q := by
rw [next, Slice.Pos.ofSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
exact Slice.Pos.next_le_of_lt
theorem Slice.Pos.get_eq_get_str {s : Slice} {p : s.Pos} {h} :
p.get h = p.str.get (str_ne_endValidPos _ h) := by
simp [ValidPos.get, Slice.Pos.get]
p.get h = p.str.get (str_ne_endPos _ h) := by
simp [String.Pos.get, Slice.Pos.get]
@[inline]
def Slice.Pos.nextFast {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
ofStr (pos.str.next (str_ne_endValidPos _ h))
(ValidPos.le_trans Slice.Pos.startInclusive_le_str (ValidPos.le_of_lt ValidPos.lt_next))
(ValidPos.next_le_of_lt (Slice.Pos.str_lt_endExclusive _ h))
ofStr (pos.str.next (str_ne_endPos _ h))
(Pos.le_trans Slice.Pos.startInclusive_le_str (Pos.le_of_lt String.Pos.lt_next))
(String.Pos.next_le_of_lt (Slice.Pos.str_lt_endExclusive _ h))
@[csimp]
theorem Slice.Pos.next_eq_nextFast : @Slice.Pos.next = @Slice.Pos.nextFast := by
@ -2086,55 +2081,55 @@ theorem Slice.Pos.next_eq_nextFast : @Slice.Pos.next = @Slice.Pos.nextFast := by
/-- The slice from the beginning of `s` up to `p` (exclusive). -/
@[inline, expose]
def sliceTo (s : String) (p : s.ValidPos) : Slice :=
def sliceTo (s : String) (p : s.Pos) : Slice :=
s.toSlice.sliceTo p.toSlice
@[deprecated sliceTo (since :="2025-11-20")]
def replaceEnd (s : String) (p : s.ValidPos) : Slice :=
def replaceEnd (s : String) (p : s.Pos) : Slice :=
s.sliceTo p
@[simp]
theorem str_sliceTo {s : String} {p : s.ValidPos} : (s.sliceTo p).str = s := rfl
theorem str_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).str = s := rfl
@[simp]
theorem startInclusive_sliceTo {s : String} {p : s.ValidPos} :
(s.sliceTo p).startInclusive = s.startValidPos := by
theorem startInclusive_sliceTo {s : String} {p : s.Pos} :
(s.sliceTo p).startInclusive = s.startPos := by
simp [sliceTo]
@[simp]
theorem endExclusive_sliceTo {s : String} {p : s.ValidPos} :
theorem endExclusive_sliceTo {s : String} {p : s.Pos} :
(s.sliceTo p).endExclusive = p := by
simp [sliceTo]
@[simp]
theorem rawEndPos_sliceTo {s : String} {p : s.ValidPos} :
theorem rawEndPos_sliceTo {s : String} {p : s.Pos} :
(s.sliceTo p).rawEndPos = p.offset := by
simp [sliceTo]
theorem Pos.Raw.isValidForSlice_stringSliceTo {s : String} {p : s.ValidPos} {q : Pos.Raw} :
theorem Pos.Raw.isValidForSlice_stringSliceTo {s : String} {p : s.Pos} {q : Pos.Raw} :
q.IsValidForSlice (s.sliceTo p) ↔ q ≤ p.offset ∧ q.IsValid s := by
rw [sliceTo, isValidForSlice_sliceTo, ValidPos.offset_toSlice, isValidForSlice_toSlice_iff]
rw [sliceTo, isValidForSlice_sliceTo, Pos.offset_toSlice, isValidForSlice_toSlice_iff]
/-- The slice from `p` (inclusive) up to the end of `s`. -/
@[inline, expose]
def sliceFrom (s : String) (p : s.ValidPos) : Slice :=
def sliceFrom (s : String) (p : s.Pos) : Slice :=
s.toSlice.sliceFrom p.toSlice
@[deprecated sliceFrom (since := "2025-11-20")]
def replaceStart (s : String) (p : s.ValidPos) : Slice :=
def replaceStart (s : String) (p : s.Pos) : Slice :=
s.sliceFrom p
@[simp]
theorem str_sliceFrom {s : String} {p : s.ValidPos} : (s.sliceFrom p).str = s := rfl
theorem str_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).str = s := rfl
@[simp]
theorem startInclusive_sliceFrom {s : String} {p : s.ValidPos} :
theorem startInclusive_sliceFrom {s : String} {p : s.Pos} :
(s.sliceFrom p).startInclusive = p := by
simp [sliceFrom]
@[simp]
theorem endExclusive_sliceFrom {s : String} {p : s.ValidPos} :
(s.sliceFrom p).endExclusive = s.endValidPos := by
theorem endExclusive_sliceFrom {s : String} {p : s.Pos} :
(s.sliceFrom p).endExclusive = s.endPos := by
simp [sliceFrom]
@[simp]
@ -2142,19 +2137,19 @@ theorem utf8ByteSize_toSlice {s : String} : s.toSlice.utf8ByteSize = s.utf8ByteS
simp [Slice.utf8ByteSize_eq]
@[simp]
theorem utf8ByteSize_sliceFrom {s : String} {p : s.ValidPos} :
theorem utf8ByteSize_sliceFrom {s : String} {p : s.Pos} :
(s.sliceFrom p).utf8ByteSize = s.utf8ByteSize - p.offset.byteIdx := by
simp [sliceFrom]
@[simp]
theorem utf8ByteSize_sliceTo {s : String} {p : s.ValidPos} :
theorem utf8ByteSize_sliceTo {s : String} {p : s.Pos} :
(s.sliceTo p).utf8ByteSize = p.offset.byteIdx := by
simp [sliceTo]
theorem Pos.Raw.isValidForSlice_stringSliceFrom {s : String} {p : s.ValidPos} {q : Pos.Raw} :
theorem Pos.Raw.isValidForSlice_stringSliceFrom {s : String} {p : s.Pos} {q : Pos.Raw} :
q.IsValidForSlice (s.sliceFrom p) ↔ (q.offsetBy p.offset).IsValid s := by
rw [sliceFrom, isValidForSlice_sliceFrom, isValidForSlice_toSlice_iff,
ValidPos.offset_toSlice]
Pos.offset_toSlice]
/--
Given a string and two valid positions within the string, obtain a slice on the string formed by
@ -2163,7 +2158,7 @@ the two positions.
This happens to be equivalent to the constructor of `String.Slice`.
-/
@[inline, expose] -- For the defeq `(s.slice p₁ p₂).str = s`
def slice (s : String) (startInclusive endExclusive : s.ValidPos)
def slice (s : String) (startInclusive endExclusive : s.Pos)
(h : startInclusive ≤ endExclusive) : String.Slice where
str := s
startInclusive
@ -2184,7 +2179,7 @@ theorem endExclusive_slice {s : String} {startInclusive endExclusive h} :
/-- Given a string and two valid positions within the string, obtain a slice on the string formed
by the new bounds, or return `none` if the given end is strictly less then the given start. -/
def slice? (s : String) (startInclusive endExclusive : s.ValidPos) :=
def slice? (s : String) (startInclusive endExclusive : s.Pos) :=
if h : startInclusive ≤ endExclusive then
some (s.slice startInclusive endExclusive h)
else
@ -2194,106 +2189,106 @@ def slice? (s : String) (startInclusive endExclusive : s.ValidPos) :=
Given a string and two valid positions within the string, obtain a slice on the string formed by
the new bounds, or panic if the given end is strictly less than the given start.
-/
def slice! (s : String) (p₁ p₂ : s.ValidPos) : Slice :=
def slice! (s : String) (p₁ p₂ : s.Pos) : Slice :=
s.toSlice.slice! p₁.toSlice p₂.toSlice
@[deprecated slice! (since := "2025-11-20")]
def replaceStartEnd! (s : String) (p₁ p₂ : s.ValidPos) : Slice :=
def replaceStartEnd! (s : String) (p₁ p₂ : s.Pos) : Slice :=
s.slice! p₁ p₂
theorem ValidPos.utf8Encode_get_eq_extract {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) :
theorem Pos.utf8Encode_get_eq_extract {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) :
List.utf8Encode [pos.get h] = s.bytes.extract pos.offset.byteIdx (pos.offset.byteIdx + (pos.get h).utf8Size) := by
rw [get_eq_get_toSlice, Slice.Pos.utf8Encode_get_eq_extract]
simp
theorem ValidPos.eq_copy_sliceTo_append_get {s : String} {pos : s.ValidPos} (h : pos ≠ s.endValidPos) :
theorem Pos.eq_copy_sliceTo_append_get {s : String} {pos : s.Pos} (h : pos ≠ s.endPos) :
s = (s.sliceTo pos).copy ++ singleton (pos.get h) ++ (s.sliceFrom (pos.next h)).copy := by
simp [← bytes_inj, utf8Encode_get_eq_extract pos h, Slice.bytes_copy, ← size_bytes]
/-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`. -/
@[inline]
def ValidPos.ofSliceFrom {s : String} {p₀ : s.ValidPos} (pos : (s.sliceFrom p₀).Pos) :
s.ValidPos where
def Pos.ofSliceFrom {s : String} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) :
s.Pos where
offset := pos.offset.offsetBy p₀.offset
isValid := Pos.Raw.isValidForSlice_stringSliceFrom.1 pos.isValidForSlice
@[deprecated ValidPos.ofSliceFrom (since := "2025-11-20")]
def ValidPos.ofReplaceStart {s : String} {p₀ : s.ValidPos} (pos : (s.sliceFrom p₀).Pos) :
s.ValidPos :=
@[deprecated Pos.ofSliceFrom (since := "2025-11-20")]
def Pos.ofReplaceStart {s : String} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) :
s.Pos :=
ofSliceFrom pos
@[simp]
theorem ValidPos.offset_ofSliceFrom {s : String} {p₀ : s.ValidPos}
theorem Pos.offset_ofSliceFrom {s : String} {p₀ : s.Pos}
{pos : (s.sliceFrom p₀).Pos} : (ofSliceFrom pos).offset = pos.offset.offsetBy p₀.offset :=
(rfl)
/-- Given a position in `s` that is at least `p₀`, obtain the corresponding position in
`s.sliceFrom p₀`. -/
@[inline]
def ValidPos.sliceFrom {s : String} (p₀ : s.ValidPos) (pos : s.ValidPos) (h : p₀ ≤ pos) :
def Pos.sliceFrom {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : p₀ ≤ pos) :
(s.sliceFrom p₀).Pos where
offset := pos.offset.unoffsetBy p₀.offset
isValidForSlice := Pos.Raw.isValidForSlice_stringSliceFrom.2 (by
simpa [Pos.Raw.offsetBy_unoffsetBy_of_le (Pos.Raw.le_iff.1 h)] using pos.isValid)
@[deprecated ValidPos.sliceFrom (since := "2025-11-20")]
def ValidPos.toReplaceStart {s : String} (p₀ : s.ValidPos) (pos : s.ValidPos) (h : p₀ ≤ pos) :
@[deprecated Pos.sliceFrom (since := "2025-11-20")]
def Pos.toReplaceStart {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : p₀ ≤ pos) :
(s.sliceFrom p₀).Pos :=
sliceFrom p₀ pos h
@[simp]
theorem ValidPos.offset_sliceFrom {s : String} {p₀ : s.ValidPos} {pos : s.ValidPos} {h} :
theorem Pos.offset_sliceFrom {s : String} {p₀ : s.Pos} {pos : s.Pos} {h} :
(sliceFrom p₀ pos h).offset = pos.offset.unoffsetBy p₀.offset := (rfl)
@[simp]
theorem ValidPos.ofSliceFrom_startPos {s : String} {pos : s.ValidPos} :
theorem Pos.ofSliceFrom_startPos {s : String} {pos : s.Pos} :
ofSliceFrom (s.sliceFrom pos).startPos = pos :=
ValidPos.ext (by simp)
Pos.ext (by simp)
@[simp]
theorem ValidPos.ofSliceFrom_endPos {s : String} {pos : s.ValidPos} :
ofSliceFrom (s.sliceFrom pos).endPos = s.endValidPos := by
theorem Pos.ofSliceFrom_endPos {s : String} {pos : s.Pos} :
ofSliceFrom (s.sliceFrom pos).endPos = s.endPos := by
have := pos.isValid.le_rawEndPos
simp_all [ValidPos.ext_iff, String.Pos.Raw.ext_iff, Pos.Raw.le_iff]
simp_all [Pos.ext_iff, String.Pos.Raw.ext_iff, Pos.Raw.le_iff]
theorem ValidPos.ofSliceFrom_inj {s : String} {p₀ : s.ValidPos}
theorem Pos.ofSliceFrom_inj {s : String} {p₀ : s.Pos}
{pos pos' : (s.sliceFrom p₀).Pos} :
ofSliceFrom pos = ofSliceFrom pos' ↔ pos = pos' := by
simp [ValidPos.ext_iff, String.Pos.Raw.ext_iff, Slice.Pos.ext_iff]
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, Slice.Pos.ext_iff]
theorem ValidPos.get_eq_get_ofSliceFrom {s : String} {p₀ : s.ValidPos}
theorem Pos.get_eq_get_ofSliceFrom {s : String} {p₀ : s.Pos}
{pos : (s.sliceFrom p₀).Pos} {h} :
pos.get h = (ofSliceFrom pos).get (by rwa [← ofSliceFrom_endPos, ne_eq, ofSliceFrom_inj]) := by
simp [ValidPos.get, Slice.Pos.get]
simp [Pos.get, Slice.Pos.get]
/-- Given a position in `s.sliceTo p₀`, obtain the corresponding position in `s`. -/
@[inline]
def ValidPos.ofSliceTo {s : String} {p₀ : s.ValidPos} (pos : (s.sliceTo p₀).Pos) : s.ValidPos where
def Pos.ofSliceTo {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos where
offset := pos.offset
isValid := (Pos.Raw.isValidForSlice_stringSliceTo.1 pos.isValidForSlice).2
@[deprecated ValidPos.ofSliceTo (since := "2025-11-20")]
def ValidPos.ofReplaceEnd {s : String} {p₀ : s.ValidPos} (pos : (s.sliceTo p₀).Pos) : s.ValidPos :=
@[deprecated Pos.ofSliceTo (since := "2025-11-20")]
def Pos.ofReplaceEnd {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos :=
ofSliceTo pos
@[simp]
theorem ValidPos.offset_ofSliceTo {s : String} {p₀ : s.ValidPos} {pos : (s.sliceTo p₀).Pos} :
theorem Pos.offset_ofSliceTo {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} :
(ofSliceTo pos).offset = pos.offset := (rfl)
/-- Given a position in `s` that is at most `p₀`, obtain the corresponding position in `s.sliceTo p₀`. -/
@[inline]
def ValidPos.sliceTo {s : String} (p₀ : s.ValidPos) (pos : s.ValidPos) (h : pos ≤ p₀) :
def Pos.sliceTo {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀) :
(s.sliceTo p₀).Pos where
offset := pos.offset
isValidForSlice := Pos.Raw.isValidForSlice_stringSliceTo.2 ⟨h, pos.isValid⟩
@[deprecated ValidPos.sliceTo (since := "2025-11-20")]
def ValidPos.toReplaceEnd {s : String} (p₀ : s.ValidPos) (pos : s.ValidPos) (h : pos ≤ p₀) :
@[deprecated Pos.sliceTo (since := "2025-11-20")]
def Pos.toReplaceEnd {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀) :
(s.sliceTo p₀).Pos :=
sliceTo p₀ pos h
@[simp]
theorem ValidPos.offset_sliceTo {s : String} {p₀ : s.ValidPos} {pos : s.ValidPos} {h : pos ≤ p₀} :
theorem Pos.offset_sliceTo {s : String} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} :
(sliceTo p₀ pos h).offset = pos.offset := (rfl)
/--
@ -2327,19 +2322,19 @@ def Slice.Pos.prevn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos :=
/--
Advances the position `p` `n` times.
If this would move `p` past the end of `s`, the result is `s.endValidPos`.
If this would move `p` past the end of `s`, the result is `s.endPos`.
-/
@[inline]
def ValidPos.nextn {s : String} (p : s.ValidPos) (n : Nat) : s.ValidPos :=
def Pos.nextn {s : String} (p : s.Pos) (n : Nat) : s.Pos :=
(p.toSlice.nextn n).ofSlice
/--
Iterates `p.prev` `n` times.
If this would move `p` past the start of `s`, the result is `s.startValidPos`.
If this would move `p` past the start of `s`, the result is `s.startPos`.
-/
@[inline]
def ValidPos.prevn {s : String} (p : s.ValidPos) (n : Nat) : s.ValidPos :=
def Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos :=
(p.toSlice.prevn n).ofSlice
theorem Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n := by
@ -2350,9 +2345,9 @@ theorem Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n :
exact Pos.Raw.le_of_lt (Pos.Raw.lt_of_lt_of_le lt_next ih)
| case3 => simp [Slice.Pos.le_iff]
theorem ValidPos.le_nextn {s : String} {p : s.ValidPos} {n : Nat} :
theorem Pos.le_nextn {s : String} {p : s.Pos} {n : Nat} :
p ≤ p.nextn n := by
simpa [nextn, ValidPos.le_iff, ← offset_toSlice] using Slice.Pos.le_nextn
simpa [nextn, Pos.le_iff, ← offset_toSlice] using Slice.Pos.le_nextn
theorem Slice.Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p := by
fun_induction prevn with
@ -2362,9 +2357,9 @@ theorem Slice.Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p :
exact Pos.Raw.le_of_lt (Pos.Raw.lt_of_le_of_lt ih prev_lt)
| case3 => simp [le_iff]
theorem ValidPos.prevn_le {s : String} {p : s.ValidPos} {n : Nat} :
theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
p.prevn n ≤ p := by
simpa [nextn, ValidPos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
simpa [nextn, Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
/--
Returns the next position in a string after position `p`. If `p` is not a valid position or
`p = s.endPos`, returns the position one byte after `p`.
@ -2372,8 +2367,8 @@ Returns the next position in a string after position `p`. If `p` is not a valid
A run-time bounds check is performed to determine whether `p` is at the end of the string. If a
bounds check has already been performed, use `String.next'` to avoid a repeated check.
This is a legacy function. The recommended alternative is `String.ValidPos.next` or one of its
variants like `String.ValidPos.next?`, combined with `String.pos` or another means of obtaining
This is a legacy function. The recommended alternative is `String.Pos.next` or one of its
variants like `String.Pos.next?`, combined with `String.pos` or another means of obtaining
a `String.ValisPos`.
Some examples of edge cases:
@ -2413,9 +2408,9 @@ middle of a multi-byte character, returns the beginning position of that charact
For example, `"L∃∀N".prev ⟨3⟩` is `⟨1⟩`, since byte 3 occurs in the middle of the multi-byte
character `'∃'` that starts at byte 1.
This is a legacy function. The recommended alternative is `String.ValidPos.prev` or one of its
variants like `String.ValidPos.prev?`, combined with `String.pos` or another means of obtaining
a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.prev` or one of its
variants like `String.Pos.prev?`, combined with `String.pos` or another means of obtaining
a `String.Pos`.
Examples:
* `"abc".get ("abc".rawEndPos |> "abc".prev) = 'c'`
@ -2466,8 +2461,8 @@ def getInBounds? (s : String) (p : String.Pos) : Option Char :=
Even with evidence of `¬ s.atEnd p`, `p` may be invalid if a byte index points into the middle of a
multi-byte UTF-8 character. For example, `"L∃∀N".get' ⟨2⟩ (by decide) = (default : Char)`.
This is a legacy function. The recommended alternative is `String.ValidPos.get`, combined with
`String.pos` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos` or another means of obtaining a `String.Pos`.
Examples:
* `"abc".get' 0 (by decide) = 'a'`
@ -2497,8 +2492,8 @@ def next? (s : String) (p : String.Pos) : Option Char :=
if h : s.atEnd p then none else s.get (s.next' p h)
```
This is a legacy function. The recommended alternative is `String.ValidPos.next`, combined with
`String.pos` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.next`, combined with
`String.pos` or another means of obtaining a `String.Pos`.
Example:
* `let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'`
@ -2571,7 +2566,7 @@ The result is `""` if the start position is greater than or equal to the end pos
start position is at the end of the string. If either position is invalid (that is, if either points
at the middle of a multi-byte UTF-8 character) then the result is unspecified.
This is a legacy function. The recommended alternative is `String.ValidPos.extract`, but usually
This is a legacy function. The recommended alternative is `String.Pos.extract`, but usually
it is even better to operate on `String.Slice` instead and call `String.Slice.copy` (only) if
required.

3
src/Init/Data/String/Bootstrap.lean
View file

@ -13,9 +13,6 @@ public section
namespace String
@[deprecated Pos.Raw (since := "2025-09-30")]
abbrev Pos := Pos.Raw
instance : OfNat String.Pos.Raw (nat_lit 0) where
ofNat := {}

86
src/Init/Data/String/Defs.lean
View file

@ -142,10 +142,6 @@ theorem String.bytes_push {s : String} {c : Char} : (s.push c).bytes = s.bytes +
namespace String
@[deprecated rawEndPos (since := "2025-10-20")]
def endPos (s : String) : String.Pos.Raw :=
s.rawEndPos
/-- The start position of the string, as a `String.Pos.Raw.` -/
def rawStartPos (_s : String) : String.Pos.Raw :=
0
@ -341,55 +337,55 @@ theorem Pos.Raw.isValid_empty_iff {p : Pos.Raw} : p.IsValid "" ↔ p = 0 := by
simp
/--
A `ValidPos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
A `Pos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
character boundary.
-/
@[ext]
structure ValidPos (s : String) where
/-- The underlying byte offset of the `ValidPos`. -/
structure Pos (s : String) where
/-- The underlying byte offset of the `Pos`. -/
offset : Pos.Raw
/-- The proof that `offset` is valid for the string `s`. -/
isValid : offset.IsValid s
deriving @[expose] DecidableEq
/-- The start position of `s`, as an `s.ValidPos`. -/
/-- The start position of `s`, as an `s.Pos`. -/
@[inline, expose]
def startValidPos (s : String) : s.ValidPos where
def startPos (s : String) : s.Pos where
offset := 0
isValid := by simp
@[simp]
theorem offset_startValidPos {s : String} : s.startValidPos.offset = 0 := (rfl)
theorem offset_startPos {s : String} : s.startPos.offset = 0 := (rfl)
instance {s : String} : Inhabited s.ValidPos where
default := s.startValidPos
instance {s : String} : Inhabited s.Pos where
default := s.startPos
/-- The past-the-end position of `s`, as an `s.ValidPos`. -/
/-- The past-the-end position of `s`, as an `s.Pos`. -/
@[inline, expose]
def endValidPos (s : String) : s.ValidPos where
def endPos (s : String) : s.Pos where
offset := s.rawEndPos
isValid := by simp
@[simp]
theorem offset_endValidPos {s : String} : s.endValidPos.offset = s.rawEndPos := (rfl)
theorem offset_endPos {s : String} : s.endPos.offset = s.rawEndPos := (rfl)
instance {s : String} : LE s.ValidPos where
instance {s : String} : LE s.Pos where
le l r := l.offset ≤ r.offset
instance {s : String} : LT s.ValidPos where
instance {s : String} : LT s.Pos where
lt l r := l.offset < r.offset
theorem ValidPos.le_iff {s : String} {l r : s.ValidPos} : l ≤ r ↔ l.offset ≤ r.offset :=
theorem Pos.le_iff {s : String} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset :=
Iff.rfl
theorem ValidPos.lt_iff {s : String} {l r : s.ValidPos} : l < r ↔ l.offset < r.offset :=
theorem Pos.lt_iff {s : String} {l r : s.Pos} : l < r ↔ l.offset < r.offset :=
Iff.rfl
instance {s : String} (l r : s.ValidPos) : Decidable (l ≤ r) :=
decidable_of_iff' _ ValidPos.le_iff
instance {s : String} (l r : s.Pos) : Decidable (l ≤ r) :=
decidable_of_iff' _ Pos.le_iff
instance {s : String} (l r : s.ValidPos) : Decidable (l < r) :=
decidable_of_iff' _ ValidPos.lt_iff
instance {s : String} (l r : s.Pos) : Decidable (l < r) :=
decidable_of_iff' _ Pos.lt_iff
/--
A region or slice of some underlying string.
@ -406,14 +402,14 @@ structure Slice where
/-- The underlying strings. -/
str : String
/-- The byte position of the start of the string slice. -/
startInclusive : str.ValidPos
startInclusive : str.Pos
/-- The byte position of the end of the string slice. -/
endExclusive : str.ValidPos
endExclusive : str.Pos
/-- The slice is not degenerate (but it may be empty). -/
startInclusive_le_endExclusive : startInclusive ≤ endExclusive
instance : Inhabited Slice where
default := ⟨"", "".startValidPos, "".startValidPos, by simp [ValidPos.le_iff]⟩
default := ⟨"", "".startPos, "".startPos, by simp [Pos.le_iff]⟩
/--
Returns a slice that contains the entire string.
@ -421,15 +417,15 @@ Returns a slice that contains the entire string.
@[inline, expose] -- expose for the defeq `s.toSlice.str = s`.
def toSlice (s : String) : Slice where
str := s
startInclusive := s.startValidPos
endExclusive := s.endValidPos
startInclusive_le_endExclusive := by simp [ValidPos.le_iff, Pos.Raw.le_iff]
startInclusive := s.startPos
endExclusive := s.endPos
startInclusive_le_endExclusive := by simp [Pos.le_iff, Pos.Raw.le_iff]
@[simp]
theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos := rfl
theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos := rfl
@[simp]
theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos := rfl
theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endPos := rfl
@[simp]
theorem str_toSlice {s : String} : s.toSlice.str = s := rfl
@ -532,7 +528,7 @@ instance {s : Slice} : Inhabited s.Pos where
theorem Slice.offset_startInclusive_add_self {s : Slice} :
s.startInclusive.offset + s = s.endExclusive.offset := by
have := s.startInclusive_le_endExclusive
simp_all [String.Pos.Raw.ext_iff, ValidPos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
simp_all [String.Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
@[simp]
theorem Pos.Raw.offsetBy_rawEndPos_left {p : Pos.Raw} {s : String} :
@ -591,18 +587,18 @@ instance {s : Slice} (l r : s.Pos) : Decidable (l < r) :=
decidable_of_iff' _ Slice.Pos.lt_iff
/--
`pos.IsAtEnd` is just shorthand for `pos = s.endValidPos` that is easier to write if `s` is long.
`pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
-/
abbrev ValidPos.IsAtEnd {s : String} (pos : s.ValidPos) : Prop :=
pos = s.endValidPos
abbrev Pos.IsAtEnd {s : String} (pos : s.Pos) : Prop :=
pos = s.endPos
@[simp]
theorem ValidPos.isAtEnd_iff {s : String} {pos : s.ValidPos} :
pos.IsAtEnd ↔ pos = s.endValidPos := Iff.rfl
theorem Pos.isAtEnd_iff {s : String} {pos : s.Pos} :
pos.IsAtEnd ↔ pos = s.endPos := Iff.rfl
@[inline]
instance {s : String} {pos : s.ValidPos} : Decidable pos.IsAtEnd :=
decidable_of_iff _ ValidPos.isAtEnd_iff
instance {s : String} {pos : s.Pos} : Decidable pos.IsAtEnd :=
decidable_of_iff _ Pos.isAtEnd_iff
/--
`pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
@ -639,4 +635,16 @@ def toSubstring (s : String) : Substring.Raw :=
def toSubstring' (s : String) : Substring.Raw :=
s.toRawSubstring'
@[deprecated String.Pos (since := "2025-11-24")]
abbrev ValidPos (s : String) : Type :=
s.Pos
@[deprecated String.startPos (since := "2025-11-24")]
abbrev startValidPos (s : String) : s.Pos :=
s.startPos
@[deprecated String.endPos (since := "2025-11-24")]
abbrev endValidPos (s : String) : s.Pos :=
s.endPos
end String

14
src/Init/Data/String/Extra.lean
View file

@ -29,28 +29,28 @@ abbrev validateUTF8 (a : ByteArray) : Bool :=
a.validateUTF8
private def findLeadingSpacesSize (s : String) : Nat :=
let it := s.startValidPos
let it := it.find? (· == '\n') |>.bind String.ValidPos.next?
let it := s.startPos
let it := it.find? (· == '\n') |>.bind String.Pos.next?
match it with
| some it => consumeSpaces it 0 s.length
| none => 0
where
consumeSpaces {s : String} (it : s.ValidPos) (curr min : Nat) : Nat :=
consumeSpaces {s : String} (it : s.Pos) (curr min : Nat) : Nat :=
if h : it.IsAtEnd then min
else if it.get h == ' ' || it.get h == '\t' then consumeSpaces (it.next h) (curr + 1) min
else if it.get h == '\n' then findNextLine (it.next h) min
else findNextLine (it.next h) (Nat.min curr min)
termination_by it
findNextLine {s : String} (it : s.ValidPos) (min : Nat) : Nat :=
findNextLine {s : String} (it : s.Pos) (min : Nat) : Nat :=
if h : it.IsAtEnd then min
else if it.get h == '\n' then consumeSpaces (it.next h) 0 min
else findNextLine (it.next h) min
termination_by it
private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
consumeSpaces n s.startValidPos ""
consumeSpaces n s.startPos ""
where
consumeSpaces (n : Nat) {s : String} (it : s.ValidPos) (r : String) : String :=
consumeSpaces (n : Nat) {s : String} (it : s.Pos) (r : String) : String :=
match n with
| 0 => saveLine it r
| n+1 =>
@ -58,7 +58,7 @@ where
else if it.get h == ' ' || it.get h == '\t' then consumeSpaces n (it.next h) r
else saveLine it r
termination_by (it, 1)
saveLine {s : String} (it : s.ValidPos) (r : String) : String :=
saveLine {s : String} (it : s.Pos) (r : String) : String :=
if h : it.IsAtEnd then r
else if it.get h == '\n' then consumeSpaces n (it.next h) (r.push '\n')
else saveLine (it.next h) (r.push (it.get h))

24
src/Init/Data/String/Iterator.lean
View file

@ -25,9 +25,9 @@ An iterator over the characters (Unicode code points) in a `String`. Typically c
`String.iter`.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
String iterators pair a string with a valid byte index. This allows efficient character-by-character
processing of strings while avoiding the need to manually ensure that byte indices are used with the
@ -57,9 +57,9 @@ structure Iterator where
/-- Creates an iterator at the beginning of the string.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
-/
@[inline] def mkIterator (s : String) : Iterator :=
⟨s, 0⟩
@ -95,9 +95,9 @@ def pos := Iterator.i
Gets the character at the iterator's current position.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
A run-time bounds check is performed. Use `String.Iterator.curr'` to avoid redundant bounds checks.
@ -110,9 +110,9 @@ If the position is invalid, returns `(default : Char)`.
Moves the iterator's position forward by one character, unconditionally.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
It is only valid to call this function if the iterator is not at the end of the string (i.e.
if `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.

6
src/Init/Data/String/Lemmas/Basic.lean
View file

@ -41,11 +41,11 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
@[simp]
theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂ := by
simp [Pos.ext_iff, ValidPos.ext_iff]
simp [String.Pos.ext_iff, Pos.ext_iff]
@[simp]
theorem ValidPos.startValidPos_le {s : String} (p : s.ValidPos) : s.startValidPos ≤ p := by
simp [ValidPos.le_iff, Pos.Raw.le_iff]
theorem Pos.startPos_le {s : String} (p : s.Pos) : s.startPos ≤ p := by
simp [Pos.le_iff, Pos.Raw.le_iff]
@[simp]
theorem Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p := by

20
src/Init/Data/String/Lemmas/Modify.lean
View file

@ -22,22 +22,22 @@ public section
namespace String
/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String}
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem Pos.Splits.pastSet {s : String} {p : s.Pos} {t₁ t₂ : String}
{c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
(p.pastSet d h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
generalize h.ne_endValidPos_of_singleton = hp
(p.pastSet d h.ne_endPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
generalize h.ne_endPos_of_singleton = hp
obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (p.splits_next_right hp)
apply splits_pastSet
/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem ValidPos.Splits.pastModify {s : String} {p : s.ValidPos} {t₁ t₂ : String}
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem Pos.Splits.pastModify {s : String} {p : s.Pos} {t₁ t₂ : String}
{c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
(p.pastModify f h.ne_endValidPos_of_singleton).Splits
(t₁ ++ singleton (f (p.get h.ne_endValidPos_of_singleton))) t₂ :=
(p.pastModify f h.ne_endPos_of_singleton).Splits
(t₁ ++ singleton (f (p.get h.ne_endPos_of_singleton))) t₂ :=
h.pastSet
theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos}
(h : p.Splits t₁ t₂) : (mapAux f s p).toList = t₁.toList ++ t₂.toList.map f := by
fun_induction mapAux generalizing t₁ t₂ with
| case1 s => simp_all
@ -47,7 +47,7 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
@[simp]
theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by
simp [map, toList_mapAux s.splits_startValidPos]
simp [map, toList_mapAux s.splits_startPos]
@[simp]
theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by

100
src/Init/Data/String/Lemmas/Splits.lean
View file

@ -11,7 +11,7 @@ import Init.Data.ByteArray.Lemmas
import Init.Data.String.Lemmas.Basic
/-!
# `Splits` predicates on `String.ValidPos` and `String.Slice.Pos`.
# `Splits` predicates on `String.Pos` and `String.Slice.Pos`.
We introduce the predicate `p.Splits t₁ t₂` for a position `p` on a string or slice `s`, which means
that `s = t₁ ++ t₂` with `p` lying between the two parts. This is a useful primitive when verifying
@ -26,7 +26,7 @@ namespace String
We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
and `t₂`.
-/
structure ValidPos.Splits {s : String} (p : s.ValidPos) (t₁ t₂ : String) : Prop where
structure Pos.Splits {s : String} (p : s.Pos) (t₁ t₂ : String) : Prop where
eq_append : s = t₁ ++ t₂
offset_eq_rawEndPos : p.offset = t₁.rawEndPos
@ -39,11 +39,11 @@ structure Slice.Pos.Splits {s : Slice} (p : s.Pos) (t₁ t₂ : String) : Prop w
offset_eq_rawEndPos : p.offset = t₁.rawEndPos
@[simp]
theorem ValidPos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.ValidPos} {t₁ t₂ : String} :
theorem Pos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String} :
(p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂ := by
subst h; simp
theorem ValidPos.Splits.cast {s₁ s₂ : String} {p : s₁.ValidPos} {t₁ t₂ : String} (h : s₁ = s₂) :
theorem Pos.Splits.cast {s₁ s₂ : String} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂) :
p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂ :=
splits_cast_iff.mpr
@ -72,15 +72,15 @@ theorem Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String}
⟨splits_of_splits_toCopy, (·.toCopy)⟩
@[simp]
theorem ValidPos.splits_toSlice_iff {s : String} {p : s.ValidPos} {t₁ t₂ : String} :
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]
theorem ValidPos.Splits.toSlice {s : String} {p : s.ValidPos} {t₁ t₂ : String}
theorem Pos.Splits.toSlice {s : String} {p : s.Pos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂ :=
splits_toSlice_iff.mpr h
theorem ValidPos.splits {s : String} (p : s.ValidPos) :
theorem Pos.splits {s : String} (p : s.Pos) :
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
@ -90,23 +90,23 @@ theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
eq_append := copy_eq_copy_sliceTo
offset_eq_rawEndPos := by simp
theorem ValidPos.Splits.bytes_left_eq {s : String} {p : s.ValidPos} {t₁ t₂}
theorem Pos.Splits.bytes_left_eq {s : String} {p : s.Pos} {t₁ t₂}
(h : p.Splits t₁ t₂) : t₁.bytes = s.bytes.extract 0 p.offset.byteIdx := by
simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_left]
theorem ValidPos.Splits.bytes_right_eq {s : String} {p : s.ValidPos} {t₁ t₂}
theorem Pos.Splits.bytes_right_eq {s : String} {p : s.Pos} {t₁ t₂}
(h : p.Splits t₁ t₂) : t₂.bytes = s.bytes.extract p.offset.byteIdx s.utf8ByteSize := by
simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_right]
theorem ValidPos.Splits.eq_left {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
theorem Pos.Splits.eq_left {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ := by
rw [← String.bytes_inj, h₁.bytes_left_eq, h₂.bytes_left_eq]
theorem ValidPos.Splits.eq_right {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
theorem Pos.Splits.eq_right {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ := by
rw [← String.bytes_inj, h₁.bytes_right_eq, h₂.bytes_right_eq]
theorem ValidPos.Splits.eq {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
theorem Pos.Splits.eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
⟨h₁.eq_left h₂, h₁.eq_right h₂⟩
@ -123,35 +123,35 @@ theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
(splits_toCopy_iff.2 h₁).eq (splits_toCopy_iff.2 h₂)
@[simp]
theorem splits_endValidPos (s : String) : s.endValidPos.Splits s "" where
theorem splits_endPos (s : String) : s.endPos.Splits s "" where
eq_append := by simp
offset_eq_rawEndPos := by simp
@[simp]
theorem splits_endValidPos_iff {s : String} :
s.endValidPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = "" :=
⟨fun h => ⟨h.eq_left s.splits_endValidPos, h.eq_right s.splits_endValidPos⟩,
by rintro ⟨rfl, rfl⟩; exact t₁.splits_endValidPos⟩
theorem splits_endPos_iff {s : String} :
s.endPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = "" :=
⟨fun h => ⟨h.eq_left s.splits_endPos, h.eq_right s.splits_endPos⟩,
by rintro ⟨rfl, rfl⟩; exact t₁.splits_endPos⟩
theorem ValidPos.Splits.eq_endValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
p = s.endValidPos ↔ t₂ = "" :=
⟨fun h' => h.eq_right (h' ▸ s.splits_endValidPos),
by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos, h.eq_append]⟩
theorem Pos.Splits.eq_endPos_iff {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
p = s.endPos ↔ t₂ = "" :=
⟨fun h' => h.eq_right (h' ▸ s.splits_endPos),
by rintro rfl; simp [Pos.ext_iff, h.offset_eq_rawEndPos, h.eq_append]⟩
theorem splits_startValidPos (s : String) : s.startValidPos.Splits "" s where
theorem splits_startPos (s : String) : s.startPos.Splits "" s where
eq_append := by simp
offset_eq_rawEndPos := by simp
@[simp]
theorem splits_startValidPos_iff {s : String} :
s.startValidPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s :=
⟨fun h => ⟨h.eq_left s.splits_startValidPos, h.eq_right s.splits_startValidPos⟩,
by rintro ⟨rfl, rfl⟩; exact t₂.splits_startValidPos⟩
theorem splits_startPos_iff {s : String} :
s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s :=
⟨fun h => ⟨h.eq_left s.splits_startPos, h.eq_right s.splits_startPos⟩,
by rintro ⟨rfl, rfl⟩; exact t₂.splits_startPos⟩
theorem ValidPos.Splits.eq_startValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
p = s.startValidPos ↔ t₁ = "" :=
⟨fun h' => h.eq_left (h' ▸ s.splits_startValidPos),
by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos]⟩
theorem Pos.Splits.eq_startPos_iff {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
p = s.startPos ↔ t₁ = "" :=
⟨fun h' => h.eq_left (h' ▸ s.splits_startPos),
by rintro rfl; simp [Pos.ext_iff, h.offset_eq_rawEndPos]⟩
@[simp]
theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" 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, ← endValidPos_copy, splits_endValidPos_iff]
rw [← Pos.splits_toCopy_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, ← endValidPos_copy, h.toCopy.eq_endValidPos_iff]
rw [← toCopy_inj, ← endPos_copy, h.toCopy.eq_endPos_iff]
@[simp]
theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
@ -175,18 +175,18 @@ 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, ← startValidPos_copy, splits_startValidPos_iff]
rw [← Pos.splits_toCopy_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, ← startValidPos_copy, h.toCopy.eq_startValidPos_iff]
rw [← toCopy_inj, ← startPos_copy, h.toCopy.eq_startPos_iff]
theorem ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
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
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) :
theorem Pos.splits_next {s : String} (p : s.Pos) (hp : p ≠ s.endPos) :
(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
@ -201,12 +201,12 @@ theorem Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
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₂' :=
theorem Pos.Splits.exists_eq_singleton_append {s : String} {p : s.Pos}
(hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
⟨(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) :=
theorem Pos.Splits.exists_eq_append_singleton {s : String} {p : s.Pos}
(hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get 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}
@ -217,13 +217,13 @@ 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.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
simp [h.eq_endValidPos_iff]
theorem Pos.Splits.ne_endPos_of_singleton {s : String} {p : s.Pos}
(h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by
simp [h.eq_endPos_iff]
theorem ValidPos.Splits.ne_startValidPos_of_singleton {s : String} {p : s.ValidPos}
(h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startValidPos := by
simp [h.eq_startValidPos_iff]
theorem Pos.Splits.ne_startPos_of_singleton {s : String} {p : s.Pos}
(h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos := by
simp [h.eq_startPos_iff]
theorem Slice.Pos.Splits.ne_endPos_of_singleton {s : Slice} {p : s.Pos}
(h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by
@ -233,10 +233,10 @@ theorem Slice.Pos.Splits.ne_startPos_of_singleton {s : Slice} {p : s.Pos}
(h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos := by
simp [h.eq_startPos_iff]
/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem ValidPos.Splits.next {s : String} {p : s.ValidPos}
(h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
generalize h.ne_endValidPos_of_singleton = hp
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
theorem Pos.Splits.next {s : String} {p : s.Pos}
(h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
generalize h.ne_endPos_of_singleton = hp
obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
exact splits_next p hp

70
src/Init/Data/String/Modify.lean
View file

@ -33,17 +33,17 @@ Examples:
* `("L∃∀N".pos ⟨4⟩ (by decide)).set 'X' (by decide) = "L∃XN"`
-/
@[extern "lean_string_utf8_set", expose]
def ValidPos.set {s : String} (p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) : String :=
def Pos.set {s : String} (p : s.Pos) (c : Char) (hp : p ≠ s.endPos) : String :=
if hc : c.utf8Size = 1 ∧ (p.byte hp).utf8ByteSize isUTF8FirstByte_byte = 1 then
.ofByteArray (s.bytes.set p.offset.byteIdx c.toUInt8 (p.byteIdx_lt_utf8ByteSize hp)) (by
rw [ByteArray.set_eq_push_extract_append_extract, ← hc.2, utf8ByteSize_byte,
← ValidPos.byteIdx_offset_next]
← Pos.byteIdx_offset_next]
refine ByteArray.IsValidUTF8.append ?_ (p.next hp).isValid.isValidUTF8_extract_utf8ByteSize
exact p.isValid.isValidUTF8_extract_zero.push hc.1)
else
(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} :
theorem Pos.set_eq_append {s : String} {p : s.Pos} {c : Char} {hp} :
p.set c hp = (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy := by
rw [set]
split
@ -52,9 +52,9 @@ theorem ValidPos.set_eq_append {s : String} {p : s.ValidPos} {c : Char} {hp} :
List.utf8Encode_singleton, String.utf8EncodeChar_eq_singleton h.1, utf8ByteSize_byte ▸ h.2]
· rfl
theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos}
{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]
rw [Pos.set_eq_append, String.append_assoc]
apply append_right
rw [isValid_copy_iff, isValidForSlice_stringSliceTo]
exact ⟨hpq, hq⟩
@ -62,40 +62,40 @@ theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp :
/-- Given a valid position in a string, obtain the corresponding position after setting a character on
that string, provided that the position was before the changed position. -/
@[inline]
def ValidPos.toSetOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos)
(hpq : q ≤ p) : (p.set c hp).ValidPos where
def Pos.toSetOfLE {s : String} (q p : s.Pos) (c : Char) (hp : p ≠ s.endPos)
(hpq : q ≤ p) : (p.set c hp).Pos where
offset := q.offset
isValid := q.isValid.set_of_le hpq
@[simp]
theorem ValidPos.offset_toSetOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
theorem Pos.offset_toSetOfLE {s : String} {q p : s.Pos} {c : Char} {hp : p ≠ s.endPos}
{hpq : q ≤ p} : (q.toSetOfLE p c hp hpq).offset = q.offset := (rfl)
theorem Pos.Raw.isValid_add_char_set {s : String} {p : s.ValidPos} {c : Char} {hp} :
theorem Pos.Raw.isValid_add_char_set {s : String} {p : s.Pos} {c : Char} {hp} :
(p.offset + c).IsValid (p.set c hp) :=
ValidPos.set_eq_append ▸ IsValid.append_right (isValid_of_eq_rawEndPos (by simp)) _
Pos.set_eq_append ▸ IsValid.append_right (isValid_of_eq_rawEndPos (by simp)) _
/-- The position just after the position that changed in a `ValidPos.set` call. -/
/-- The position just after the position that changed in a `Pos.set` call. -/
@[inline]
def ValidPos.pastSet {s : String} (p : s.ValidPos) (c : Char) (hp) : (p.set c hp).ValidPos where
def Pos.pastSet {s : String} (p : s.Pos) (c : Char) (hp) : (p.set c hp).Pos where
offset := p.offset + c
isValid := Pos.Raw.isValid_add_char_set
@[simp]
theorem ValidPos.offset_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
theorem Pos.offset_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
(p.pastSet c hp).offset = p.offset + c := (rfl)
@[inline]
def ValidPos.appendRight {s : String} (p : s.ValidPos) (t : String) : (s ++ t).ValidPos where
def Pos.appendRight {s : String} (p : s.Pos) (t : String) : (s ++ t).Pos where
offset := p.offset
isValid := p.isValid.append_right t
theorem ValidPos.splits_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
theorem Pos.splits_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
(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
theorem remainingBytes_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
theorem remainingBytes_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
(p.pastSet c hp).remainingBytes = (p.next hp).remainingBytes := by
rw [(p.next hp).splits.remainingBytes_eq, p.splits_pastSet.remainingBytes_eq]
@ -110,34 +110,34 @@ Examples:
* `("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"`
-/
@[inline]
def ValidPos.modify {s : String} (p : s.ValidPos) (f : Char → Char) (hp : p ≠ s.endValidPos) :
def Pos.modify {s : String} (p : s.Pos) (f : Char → Char) (hp : p ≠ s.endPos) :
String :=
p.set (f <| p.get hp) hp
theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char → Char}
{hp : p ≠ s.endValidPos} {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) :
theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.Pos} {f : Char → Char}
{hp : p ≠ s.endPos} {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) :
q.IsValid (p.modify f hp) :=
set_of_le hq hpq
/-- Given a valid position in a string, obtain the corresponding position after modifying a character
in that string, provided that the position was before the changed position. -/
@[inline]
def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char)
(hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.modify f hp).ValidPos where
def Pos.toModifyOfLE {s : String} (q p : s.Pos) (f : Char → Char)
(hp : p ≠ s.endPos) (hpq : q ≤ p) : (p.modify f hp).Pos where
offset := q.offset
isValid := q.isValid.modify_of_le hpq
@[simp]
theorem ValidPos.offset_toModifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char}
{hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
theorem Pos.offset_toModifyOfLE {s : String} {q p : s.Pos} {f : Char → Char}
{hp : p ≠ s.endPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
/-- The position just after the position that was modified in a `ValidPos.modify` call. -/
/-- The position just after the position that was modified in a `Pos.modify` call. -/
@[inline]
def ValidPos.pastModify {s : String} (p : s.ValidPos) (f : Char → Char)
(hp : p ≠ s.endValidPos) : (p.modify f hp).ValidPos :=
def Pos.pastModify {s : String} (p : s.Pos) (f : Char → Char)
(hp : p ≠ s.endPos) : (p.modify f hp).Pos :=
p.pastSet _ _
theorem remainingBytes_pastModify {s : String} {p : s.ValidPos} {f : Char → Char} {hp} :
theorem remainingBytes_pastModify {s : String} {p : s.Pos} {f : Char → Char} {hp} :
(p.pastModify f hp).remainingBytes = (p.next hp).remainingBytes :=
remainingBytes_pastSet
@ -148,8 +148,8 @@ invalid, the string is returned unchanged.
If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.
This is a legacy function. The recommended alternative is `String.ValidPos.set`, combined with
`String.pos` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
`String.pos` or another means of obtaining a `String.Pos`.
Examples:
* `"abc".set ⟨1⟩ 'B' = "aBc"`
@ -173,8 +173,8 @@ character. If `p` is an invalid position, the string is returned unchanged.
If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.
This is a legacy function. The recommended alternative is `String.ValidPos.set`, combined with
`String.pos` or another means of obtaining a `String.ValidPos`.
This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
`String.pos` or another means of obtaining a `String.Pos`.
Examples:
* `"abc".modify ⟨1⟩ Char.toUpper = "aBc"`
@ -188,14 +188,14 @@ def Pos.Raw.modify (s : String) (i : Pos.Raw) (f : Char → Char) : String :=
def modify (s : String) (i : Pos.Raw) (f : Char → Char) : String :=
i.set s (f (i.get s))
@[specialize] def mapAux (f : Char → Char) (s : String) (p : s.ValidPos) : String :=
if h : p = s.endValidPos then
@[specialize] def mapAux (f : Char → Char) (s : String) (p : s.Pos) : String :=
if h : p = s.endPos then
s
else
mapAux f (p.modify f h) (p.pastModify f h)
termination_by p.remainingBytes
decreasing_by
simp [remainingBytes_pastModify, ← ValidPos.lt_iff_remainingBytes_lt]
simp [remainingBytes_pastModify, ← Pos.lt_iff_remainingBytes_lt]
/--
Applies the function `f` to every character in a string, returning a string that contains the
@ -206,7 +206,7 @@ Examples:
* `"".map Char.toUpper = ""`
-/
@[inline] def map (f : Char → Char) (s : String) : String :=
mapAux f s s.startValidPos
mapAux f s s.startPos
/--
Replaces each character in `s` with the result of applying `Char.toUpper` to it.

4
src/Init/Data/String/Pattern/Basic.lean
View file

@ -112,12 +112,12 @@ def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos
(by
have := lhs.startInclusive_le_endExclusive
have := lhs.endExclusive.isValid.le_utf8ByteSize
simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
omega)
(by
have := rhs.startInclusive_le_endExclusive
have := rhs.endExclusive.isValid.le_utf8ByteSize
simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
omega)
end Internal

4
src/Init/Data/String/PosRaw.lean
View file

@ -216,7 +216,7 @@ theorem Pos.Raw.increaseBy_charUtf8Size {p : Pos.Raw} {c : Char} :
p.increaseBy c.utf8Size = p + c := by
simp [Pos.Raw.ext_iff]
/-- Increases the byte offset of the position by `1`. Not to be confused with `ValidPos.next`. -/
/-- Increases the byte offset of the position by `1`. Not to be confused with `Pos.next`. -/
@[inline, expose]
def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
⟨p.byteIdx + 1⟩
@ -224,7 +224,7 @@ def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
@[simp]
theorem Pos.Raw.byteIdx_inc {p : Pos.Raw} : p.inc.byteIdx = p.byteIdx + 1 := (rfl)
/-- Decreases the byte offset of the position by `1`. Not to be confused with `ValidPos.prev`. -/
/-- Decreases the byte offset of the position by `1`. Not to be confused with `Pos.prev`. -/
@[inline, expose]
def Pos.Raw.dec (p : Pos.Raw) : Pos.Raw :=
⟨p.byteIdx - 1⟩

70
src/Init/Data/String/Search.lean
View file

@ -88,27 +88,27 @@ Finds the position of the first match of the pattern {name}`pattern` in after th
This function is generic over all currently supported patterns.
Examples:
* {lean}`("coffee tea water".startValidPos.find? Char.isWhitespace).map (·.get!) == some ' '`
* {lean}`("coffee tea water".startPos.find? Char.isWhitespace).map (·.get!) == some ' '`
* {lean}`("tea".pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none`
-/
@[inline]
def ValidPos.find? {s : String} (pos : s.ValidPos) (pattern : ρ)
[ToForwardSearcher pattern σ] : Option s.ValidPos :=
def Pos.find? {s : String} (pos : s.Pos) (pattern : ρ)
[ToForwardSearcher pattern σ] : Option s.Pos :=
(pos.toSlice.find? pattern).map (·.ofSlice)
/--
Finds the position of the first match of the pattern {name}`pattern` in after the position
{name}`pos`. If there is no match {lean}`s.endValidPos` is returned.
{name}`pos`. If there is no match {lean}`s.endPos` is returned.
This function is generic over all currently supported patterns.
Examples:
* {lean}`("coffee tea water".startValidPos.find Char.isWhitespace).get! == ' '`
* {lean}`("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endValidPos`
* {lean}`("coffee tea water".startPos.find Char.isWhitespace).get! == ' '`
* {lean}`("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endPos`
-/
@[inline]
def ValidPos.find {s : String} (pos : s.ValidPos) (pattern : ρ) [ToForwardSearcher pattern σ] :
s.ValidPos :=
def Pos.find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :
s.Pos :=
(pos.toSlice.find pattern).ofSlice
/--
@ -123,23 +123,23 @@ Examples:
* {lean}`("coffee tea water".find? "tea").map (·.get!) == some 't'`
-/
@[inline]
def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.ValidPos :=
s.startValidPos.find? pattern
def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.Pos :=
s.startPos.find? pattern
/--
Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s`. If there
is no match {lean}`s.endValidPos` is returned.
is no match {lean}`s.endPos` is returned.
This function is generic over all currently supported patterns.
Examples:
* {lean}`("coffee tea water".find Char.isWhitespace).get! == ' '`
* {lean}`"tea".find (fun (c : Char) => c == 'X') == "tea".endValidPos`
* {lean}`"tea".find (fun (c : Char) => c == 'X') == "tea".endPos`
* {lean}`("coffee tea water".find "tea").get! == 't'`
-/
@[inline]
def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.ValidPos :=
s.startValidPos.find pattern
def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.Pos :=
s.startPos.find pattern
/--
Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s` that is
@ -166,12 +166,12 @@ This function is generic over all currently supported patterns except
{name}`String`/{name}`String.Slice`.
Examples:
* {lean}`(("ab1c".endValidPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`
* {lean}`"abc".startValidPos.revFind? Char.isAlpha == none`
* {lean}`(("ab1c".endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`
* {lean}`"abc".startPos.revFind? Char.isAlpha == none`
-/
@[inline]
def ValidPos.revFind? {s : String} (pos : s.ValidPos) (pattern : ρ) [ToBackwardSearcher pattern σ] :
Option s.ValidPos :=
def Pos.revFind? {s : String} (pos : s.Pos) (pattern : ρ) [ToBackwardSearcher pattern σ] :
Option s.Pos :=
(pos.toSlice.revFind? pattern).map (·.ofSlice)
/--
@ -187,32 +187,32 @@ Examples:
* {lean}`"tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none`
-/
@[inline]
def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.ValidPos :=
s.endValidPos.revFind? pattern
def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.Pos :=
s.endPos.revFind? pattern
@[export lean_string_posof]
def Internal.posOfImpl (s : String) (c : Char) : Pos.Raw :=
(s.find c).offset
@[deprecated String.ValidPos.find (since := "2025-11-19")]
@[deprecated String.Pos.find (since := "2025-11-19")]
def findAux (s : String) (p : Char → Bool) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
if h : pos ≤ stopPos ∧ pos.IsValid s ∧ stopPos.IsValid s then
(String.Slice.mk s (s.pos pos h.2.1) (s.pos stopPos h.2.2)
(by simp [ValidPos.le_iff, h.1])).find p |>.str.offset
(by simp [Pos.le_iff, h.1])).find p |>.str.offset
else stopPos
@[deprecated String.ValidPos.find (since := "2025-11-19")]
@[deprecated String.Pos.find (since := "2025-11-19")]
def posOfAux (s : String) (c : Char) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
if h : pos ≤ stopPos ∧ pos.IsValid s ∧ stopPos.IsValid s then
(String.Slice.mk s (s.pos pos h.2.1) (s.pos stopPos h.2.2)
(by simp [ValidPos.le_iff, h.1])).find c |>.str.offset
(by simp [Pos.le_iff, h.1])).find c |>.str.offset
else stopPos
@[deprecated String.find (since := "2025-11-19")]
def posOf (s : String) (c : Char) : Pos.Raw :=
(s.find c).offset
@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
@[deprecated String.Pos.revFind? (since := "2025-11-19")]
def revPosOfAux (s : String) (c : Char) (pos : Pos.Raw) : Option Pos.Raw :=
s.pos? pos |>.bind (·.revFind? c) |>.map (·.offset)
@ -220,7 +220,7 @@ def revPosOfAux (s : String) (c : Char) (pos : Pos.Raw) : Option Pos.Raw :=
def revPosOf (s : String) (c : Char) : Option Pos.Raw :=
s.revFind? c |>.map (·.offset)
@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
@[deprecated String.Pos.revFind? (since := "2025-11-19")]
def revFindAux (s : String) (p : Char → Bool) (pos : Pos.Raw) : Option Pos.Raw :=
s.pos? pos |>.bind (·.revFind? p) |>.map (·.offset)
@ -234,9 +234,9 @@ Returns the position of the beginning of the line that contains the position {na
Lines are ended by {lean}`'\n'`, and the returned position is either {lean}`0 : String.Pos.Raw` or
immediately after a {lean}`'\n'` character.
-/
@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
@[deprecated String.Pos.revFind? (since := "2025-11-19")]
def findLineStart (s : String) (pos : String.Pos.Raw) : String.Pos.Raw :=
s.pos? pos |>.bind (·.revFind? '\n') |>.map (·.offset) |>.getD s.startValidPos.offset
s.pos? pos |>.bind (·.revFind? '\n') |>.map (·.offset) |>.getD s.startPos.offset
/--
Splits a string at each subslice that matches the pattern {name}`pat`.
@ -405,14 +405,14 @@ Examples:
@[inline, expose] def back (s : String) : Char :=
s.toSlice.back
theorem Slice.Pos.ofSlice_ne_endValidPos {s : String} {p : s.toSlice.Pos}
(h : p ≠ s.toSlice.endPos) : p.ofSlice ≠ s.endValidPos := by
rwa [ne_eq, ← ValidPos.toSlice_inj, toSlice_ofSlice, ← endPos_toSlice]
theorem Slice.Pos.ofSlice_ne_endPos {s : String} {p : s.toSlice.Pos}
(h : p ≠ s.toSlice.endPos) : p.ofSlice ≠ s.endPos := by
rwa [ne_eq, ← Pos.toSlice_inj, toSlice_ofSlice, ← endPos_toSlice]
@[inline]
def Internal.toSliceWithProof {s : String} :
{ p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.ValidPos // p ≠ s.endValidPos } :=
fun ⟨p, h⟩ => ⟨p.ofSlice, Slice.Pos.ofSlice_ne_endValidPos h⟩
{ p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos } :=
fun ⟨p, h⟩ => ⟨p.ofSlice, Slice.Pos.ofSlice_ne_endPos h⟩
/--
Creates an iterator over all valid positions within {name}`s`.
@ -425,7 +425,7 @@ Examples
-/
@[inline]
def positions (s : String) :=
(s.toSlice.positions.map Internal.toSliceWithProof : Std.Iter { p : s.ValidPos // p ≠ s.endValidPos })
(s.toSlice.positions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos })
/--
Creates an iterator over all characters (Unicode code points) in {name}`s`.
@ -450,7 +450,7 @@ Examples
-/
@[inline]
def revPositions (s : String) :=
(s.toSlice.revPositions.map Internal.toSliceWithProof : Std.Iter { p : s.ValidPos // p ≠ s.endValidPos })
(s.toSlice.revPositions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos })
/--
Creates an iterator over all characters (Unicode code points) in {name}`s`, starting from the end

2
src/Init/Data/String/Substring.lean
View file

@ -35,7 +35,7 @@ Converts a `Substring.Raw` into a `String.Slice`, returning `none` if the substr
def toSlice (s : Substring.Raw) : Option String.Slice :=
if h : s.startPos.IsValid s.str ∧ s.stopPos.IsValid s.str ∧ s.startPos ≤ s.stopPos then
some (String.Slice.mk s.str (s.str.pos s.startPos h.1) (s.str.pos s.stopPos h.2.1)
(by simp [String.ValidPos.le_iff, h.2.2]))
(by simp [String.Pos.le_iff, h.2.2]))
else
none

108
src/Init/Data/String/Termination.lean
View file

@ -113,119 +113,119 @@ theorem prev_prev_lt {s : Slice} {p : s.Pos} {h h'} : (p.prev h).prev h' < p :=
end Slice.Pos
namespace ValidPos
namespace Pos
/-- The number of bytes between `p` and the end position. This number decreases as `p` advances. -/
def remainingBytes {s : String} (p : s.ValidPos) : Nat :=
def remainingBytes {s : String} (p : s.Pos) : Nat :=
p.toSlice.remainingBytes
@[simp]
theorem remainingBytes_toSlice {s : String} {p : s.ValidPos} :
theorem remainingBytes_toSlice {s : String} {p : s.Pos} :
p.toSlice.remainingBytes = p.remainingBytes := (rfl)
theorem remainingBytes_eq_byteDistance {s : String} {p : s.ValidPos} :
p.remainingBytes = p.offset.byteDistance s.endValidPos.offset := (rfl)
theorem remainingBytes_eq_byteDistance {s : String} {p : s.Pos} :
p.remainingBytes = p.offset.byteDistance s.endPos.offset := (rfl)
theorem remainingBytes_eq {s : String} {p : s.ValidPos} :
theorem remainingBytes_eq {s : String} {p : s.Pos} :
p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx := by
simp [remainingBytes_eq_byteDistance, Pos.Raw.byteDistance_eq]
theorem remainingBytes_inj {s : String} {p q : s.ValidPos} :
theorem remainingBytes_inj {s : String} {p q : s.Pos} :
p.remainingBytes = q.remainingBytes ↔ p = q := by
simp [← remainingBytes_toSlice, ValidPos.toSlice_inj, Slice.Pos.remainingBytes_inj]
simp [← remainingBytes_toSlice, Pos.toSlice_inj, Slice.Pos.remainingBytes_inj]
theorem le_iff_remainingBytes_le {s : String} (p q : s.ValidPos) :
theorem le_iff_remainingBytes_le {s : String} (p q : s.Pos) :
p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes := by
simp [← remainingBytes_toSlice, ← Slice.Pos.le_iff_remainingBytes_le]
theorem lt_iff_remainingBytes_lt {s : String} (p q : s.ValidPos) :
theorem lt_iff_remainingBytes_lt {s : String} (p q : s.Pos) :
p < q ↔ q.remainingBytes < p.remainingBytes := by
simp [← remainingBytes_toSlice, ← Slice.Pos.lt_iff_remainingBytes_lt]
theorem wellFounded_lt {s : String} : WellFounded (fun (p : s.ValidPos) q => p < q) := by
theorem wellFounded_lt {s : String} : WellFounded (fun (p : s.Pos) q => p < q) := by
simpa [lt_iff, Pos.Raw.lt_iff] using
InvImage.wf (Pos.Raw.byteIdx ∘ ValidPos.offset) Nat.lt_wfRel.wf
InvImage.wf (Pos.Raw.byteIdx ∘ Pos.offset) Nat.lt_wfRel.wf
theorem wellFounded_gt {s : String} : WellFounded (fun (p : s.ValidPos) q => q < p) := by
theorem wellFounded_gt {s : String} : WellFounded (fun (p : s.Pos) q => q < p) := by
simpa [lt_iff_remainingBytes_lt] using
InvImage.wf ValidPos.remainingBytes Nat.lt_wfRel.wf
InvImage.wf Pos.remainingBytes Nat.lt_wfRel.wf
instance {s : String} : WellFoundedRelation s.ValidPos where
instance {s : String} : WellFoundedRelation s.Pos where
rel p q := q < p
wf := ValidPos.wellFounded_gt
wf := Pos.wellFounded_gt
/-- Type alias for `String.ValidPos` representing that the given position is expected to decrease
/-- Type alias for `String.Pos` representing that the given position is expected to decrease
in recursive calls. -/
structure Down (s : String) : Type where
inner : s.ValidPos
inner : s.Pos
/-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
expected to decrease. -/
def down {s : String} (p : s.ValidPos) : ValidPos.Down s where
def down {s : String} (p : s.Pos) : Pos.Down s where
inner := p
@[simp]
theorem inner_down {s : String} {p : s.ValidPos} : p.down.inner = p := (rfl)
theorem inner_down {s : String} {p : s.Pos} : p.down.inner = p := (rfl)
instance {s : String} : WellFoundedRelation (ValidPos.Down s) where
instance {s : String} : WellFoundedRelation (Pos.Down s) where
rel p q := p.inner < q.inner
wf := InvImage.wf ValidPos.Down.inner ValidPos.wellFounded_lt
wf := InvImage.wf Pos.Down.inner Pos.wellFounded_lt
theorem map_toSlice_next? {s : String} {p : s.ValidPos} :
p.next?.map ValidPos.toSlice = p.toSlice.next? := by
theorem map_toSlice_next? {s : String} {p : s.Pos} :
p.next?.map Pos.toSlice = p.toSlice.next? := by
simp [next?]
theorem map_toSlice_prev? {s : String} {p : s.ValidPos} :
p.prev?.map ValidPos.toSlice = p.toSlice.prev? := by
theorem map_toSlice_prev? {s : String} {p : s.Pos} :
p.prev?.map Pos.toSlice = p.toSlice.prev? := by
simp [prev?]
theorem ne_endValidPos_of_next?_eq_some {s : String} {p q : s.ValidPos}
(h : p.next? = some q) : p ≠ s.endValidPos :=
ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_endPos_of_next?_eq_some
(by simpa only [ValidPos.map_toSlice_next?, Option.map_some] using congrArg (·.map toSlice) h))
theorem ne_endPos_of_next?_eq_some {s : String} {p q : s.Pos}
(h : p.next? = some q) : p ≠ s.endPos :=
ne_of_apply_ne Pos.toSlice (Slice.Pos.ne_endPos_of_next?_eq_some
(by simpa only [Pos.map_toSlice_next?, Option.map_some] using congrArg (·.map toSlice) h))
theorem eq_next_of_next?_eq_some {s : String} {p q : s.ValidPos} (h : p.next? = some q) :
q = p.next (ne_endValidPos_of_next?_eq_some h) := by
theorem eq_next_of_next?_eq_some {s : String} {p q : s.Pos} (h : p.next? = some q) :
q = p.next (ne_endPos_of_next?_eq_some h) := by
simpa only [← toSlice_inj, toSlice_next] using Slice.Pos.eq_next_of_next?_eq_some
(by simpa [ValidPos.map_toSlice_next?] using congrArg (·.map toSlice) h)
(by simpa [Pos.map_toSlice_next?] using congrArg (·.map toSlice) h)
theorem ne_startValidPos_of_prev?_eq_some {s : String} {p q : s.ValidPos}
(h : p.prev? = some q) : p ≠ s.startValidPos :=
ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_startPos_of_prev?_eq_some
(by simpa only [ValidPos.map_toSlice_prev?, Option.map_some] using congrArg (·.map toSlice) h))
theorem ne_startPos_of_prev?_eq_some {s : String} {p q : s.Pos}
(h : p.prev? = some q) : p ≠ s.startPos :=
ne_of_apply_ne Pos.toSlice (Slice.Pos.ne_startPos_of_prev?_eq_some
(by simpa only [Pos.map_toSlice_prev?, Option.map_some] using congrArg (·.map toSlice) h))
theorem eq_prev_of_prev?_eq_some {s : String} {p q : s.ValidPos} (h : p.prev? = some q) :
q = p.prev (ne_startValidPos_of_prev?_eq_some h) := by
theorem eq_prev_of_prev?_eq_some {s : String} {p q : s.Pos} (h : p.prev? = some q) :
q = p.prev (ne_startPos_of_prev?_eq_some h) := by
simpa only [← toSlice_inj, toSlice_prev] using Slice.Pos.eq_prev_of_prev?_eq_some
(by simpa [ValidPos.map_toSlice_prev?] using congrArg (·.map toSlice) h)
(by simpa [Pos.map_toSlice_prev?] using congrArg (·.map toSlice) h)
@[simp]
theorem le_refl {s : String} (p : s.ValidPos) : p ≤ p := by
simp [ValidPos.le_iff]
theorem le_refl {s : String} (p : s.Pos) : p ≤ p := by
simp [Pos.le_iff]
theorem lt_trans {s : String} {p q r : s.ValidPos} : p < q → q < r → p < r := by
simpa [ValidPos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
theorem lt_trans {s : String} {p q r : s.Pos} : p < q → q < r → p < r := by
simpa [Pos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
@[simp]
theorem lt_next_next {s : String} {p : s.ValidPos} {h h'} : p < (p.next h).next h' :=
theorem lt_next_next {s : String} {p : s.Pos} {h h'} : p < (p.next h).next h' :=
lt_trans p.lt_next (p.next h).lt_next
@[simp]
theorem prev_prev_lt {s : String} {p : s.ValidPos} {h h'} : (p.prev h).prev h' < p :=
theorem prev_prev_lt {s : String} {p : s.Pos} {h h'} : (p.prev h).prev h' < p :=
lt_trans (p.prev h).prev_lt p.prev_lt
theorem Splits.remainingBytes_eq {s : String} {p : s.ValidPos} {t₁ t₂}
theorem Splits.remainingBytes_eq {s : String} {p : s.Pos} {t₁ t₂}
(h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize := by
simp [ValidPos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos]
simp [Pos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos]
end ValidPos
end Pos
namespace Slice.Pos
@[simp]
theorem remainingBytes_toCopy {s : Slice} {p : s.Pos} :
p.toCopy.remainingBytes = p.remainingBytes := by
simp [remainingBytes_eq, ValidPos.remainingBytes_eq, Slice.utf8ByteSize_eq]
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
@ -244,14 +244,14 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
Slice.Pos.eq_prev_of_prev?_eq_some (by assumption),
]) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : String.ValidPos _) < _
(with_reducible change (_ : String.Pos _) < _
simp [
ValidPos.eq_next_of_next?_eq_some (by assumption),
Pos.eq_next_of_next?_eq_some (by assumption),
]) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : String.ValidPos _) < _
(with_reducible change (_ : String.Pos _) < _
simp [
ValidPos.eq_prev_of_prev?_eq_some (by assumption),
Pos.eq_prev_of_prev?_eq_some (by assumption),
]) <;> done)
end String

2
src/Init/Prelude.lean
View file

@ -3482,7 +3482,7 @@ be translated internally to byte positions, which takes linear time.
A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.rawEndPos` and `p` lies on a UTF-8
character boundary, see `String.Pos.IsValid`.
There is another type, `String.ValidPos`, which bundles the validity predicate. Using `String.ValidPos`
There is another type, `String.Pos`, which bundles the validity predicate. Using `String.Pos`
instead of `String.Pos.Raw` is recommended because it will lead to less error handling and fewer edge cases.
-/
structure String.Pos.Raw where

8
src/Init/System/FilePath.lean
View file

@ -93,7 +93,7 @@ An absolute path starts at the root directory or a drive letter. Accessing files
path does not depend on the current working directory.
-/
def isAbsolute (p : FilePath) : Bool :=
pathSeparators.contains p.toString.front || (isWindows && p.toString.length > 1 && p.toString.startValidPos.next?.bind (·.get?) == some ':')
pathSeparators.contains p.toString.front || (isWindows && p.toString.length > 1 && p.toString.startPos.next?.bind (·.get?) == some ':')
/--
A relative path is one that depends on the current working directory for interpretation. Relative
@ -122,7 +122,7 @@ instance : HDiv FilePath String FilePath where
hDiv p sub := FilePath.join p ⟨sub⟩
private def posOfLastSep (p : FilePath) : Option String.Pos.Raw :=
p.toString.revFind? pathSeparators.contains |>.map String.ValidPos.offset
p.toString.revFind? pathSeparators.contains |>.map String.Pos.offset
/--
Returns the parent directory of a path, if there is one.
@ -173,7 +173,7 @@ Examples:
-/
def fileStem (p : FilePath) : Option String :=
p.fileName.map fun fname =>
match fname.revFind? '.' |>.map String.ValidPos.offset with
match fname.revFind? '.' |>.map String.Pos.offset with
| some ⟨0⟩ => fname
| some pos => String.Pos.Raw.extract fname 0 pos
| none => fname
@ -192,7 +192,7 @@ Examples:
-/
def extension (p : FilePath) : Option String :=
p.fileName.bind fun fname =>
match fname.revFind? '.' |>.map String.ValidPos.offset with
match fname.revFind? '.' |>.map String.Pos.offset with
| some 0 => none
| some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.rawEndPos
| none => none

6
src/Lean/Compiler/ExternAttr.lean
View file

@ -76,7 +76,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=
externAttr.getParam? env n
private def parseOptNum : Nat → (pattern : String) → (it : pattern.ValidPos) → Nat → pattern.ValidPos × Nat
private def parseOptNum : Nat → (pattern : String) → (it : pattern.Pos) → Nat → pattern.Pos × Nat
| 0, _ , it, r => (it, r)
| n+1, pattern, it, r =>
if h : it.IsAtEnd then (it, r)
@ -86,7 +86,7 @@ private def parseOptNum : Nat → (pattern : String) → (it : pattern.ValidPos)
then parseOptNum n pattern (it.next h) (r*10 + (c.toNat - '0'.toNat))
else (it, r)
def expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.ValidPos) → String → String
def expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.Pos) → String → String
| 0, _, _, r => r
| i+1, pattern, it, r =>
if h : it.IsAtEnd then r
@ -99,7 +99,7 @@ def expandExternPatternAux (args : List String) : Nat → (pattern : String) →
expandExternPatternAux args i pattern it (r ++ args.getD j "")
def expandExternPattern (pattern : String) (args : List String) : String :=
expandExternPatternAux args pattern.length pattern pattern.startValidPos ""
expandExternPatternAux args pattern.length pattern pattern.startPos ""
def mkSimpleFnCall (fn : String) (args : List String) : String :=
fn ++ "(" ++ ((args.intersperse ", ").foldl (·++·) "") ++ ")"

54
src/Lean/Compiler/NameMangling.lean
View file

@ -29,8 +29,8 @@ where finally
simp [i, UInt32.lt_iff_toNat_lt, this]; omega
def mangleAux (s : String) (pos : s.ValidPos) (r : String) : String :=
if h : pos = s.endValidPos then r else
def mangleAux (s : String) (pos : s.Pos) (r : String) : String :=
if h : pos = s.endPos then r else
let c := pos.get h
let pos := pos.next h
if c.isAlpha || c.isDigit then
@ -46,16 +46,16 @@ def mangleAux (s : String) (pos : s.ValidPos) (r : String) : String :=
termination_by pos
public def mangle (s : String) : String :=
mangleAux s s.startValidPos ""
mangleAux s s.startPos ""
end String
namespace Lean
def checkLowerHex : Nat → (s : String) → s.ValidPos → Bool
def checkLowerHex : Nat → (s : String) → s.Pos → Bool
| 0, _, _ => true
| k + 1, s, pos =>
if h : pos = s.endValidPos then
if h : pos = s.endPos then
false
else
let ch := pos.get h
@ -69,19 +69,19 @@ def fromHex? (c : Char) : Option Nat :=
some (c.val - 87).toNat
else none
def parseLowerHex? (k : Nat) (s : String) (p : s.ValidPos) (acc : Nat) :
Option (s.ValidPos × Nat) :=
def parseLowerHex? (k : Nat) (s : String) (p : s.Pos) (acc : Nat) :
Option (s.Pos × Nat) :=
match k with
| 0 => some (p, acc)
| k + 1 =>
if h : p = s.endValidPos then
if h : p = s.endPos then
none
else
match fromHex? (p.get h) with
| some d => parseLowerHex? k s (p.next h) (acc <<< 4 ||| d)
| none => none
theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.ValidPos} {acc : Nat}
theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.Pos} {acc : Nat}
{r : Nat} (hk : 0 < k) : parseLowerHex? k s p acc = some (q, r) → p < q := by
fun_induction parseLowerHex? with
| case1 => simp at hk
@ -89,10 +89,10 @@ theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.ValidPos} {
| case3 p acc k h d x ih =>
match k with
| 0 => simpa [parseLowerHex?] using fun h _ => h ▸ p.lt_next
| k + 1 => exact fun h => String.ValidPos.lt_trans p.lt_next (ih (by simp) h)
| k + 1 => exact fun h => String.Pos.lt_trans p.lt_next (ih (by simp) h)
| case4 => simp
def checkDisambiguation (s : String) (p : s.ValidPos) : Bool :=
def checkDisambiguation (s : String) (p : s.Pos) : Bool :=
if h : _ then
let b := p.get h
if b = '_' then
@ -111,8 +111,8 @@ termination_by p
def needDisambiguation (prev : Name) (next : String) : Bool :=
(match prev with
| .str _ s => ∃ h, (s.endValidPos.prev h).get (by simp) = '_'
| _ => false) || checkDisambiguation next next.startValidPos
| .str _ s => ∃ h, (s.endPos.prev h).get (by simp) = '_'
| _ => false) || checkDisambiguation next next.startPos
def Name.mangleAux : Name → String
| Name.anonymous => ""
@ -120,7 +120,7 @@ def Name.mangleAux : Name → String
let m := String.mangle s
match p with
| Name.anonymous =>
if checkDisambiguation m m.startValidPos then "00" ++ m else m
if checkDisambiguation m m.startPos then "00" ++ m else m
| p =>
let m1 := mangleAux p
m1 ++ (if needDisambiguation p m then "_00" else "_") ++ m
@ -149,9 +149,9 @@ public def mkPackageSymbolPrefix (pkg? : Option PkgId) : String :=
pkg?.elim "l_" (s!"lp_{·.mangle}_")
-- assumes `s` has been generated `Name.mangle n ""`
def Name.demangleAux (s : String) (p₀ : s.ValidPos) (res : Name)
def Name.demangleAux (s : String) (p₀ : s.Pos) (res : Name)
(acc : String) (ucount : Nat) : Name :=
if hp₀ : p₀ = s.endValidPos then res.str (acc.pushn '_' (ucount / 2)) else
if hp₀ : p₀ = s.endPos then res.str (acc.pushn '_' (ucount / 2)) else
let ch := p₀.get hp₀
let p := p₀.next hp₀
if ch = '_' then demangleAux s p res acc (ucount + 1) else
@ -159,7 +159,7 @@ def Name.demangleAux (s : String) (p₀ : s.ValidPos) (res : Name)
demangleAux s p res (acc.pushn '_' (ucount / 2) |>.push ch) 0
else if ch.isDigit then
let res := res.str (acc.pushn '_' (ucount / 2))
if h : ch = '0' ∧ ∃ h : p ≠ s.endValidPos, p.get h = '0' then
if h : ch = '0' ∧ ∃ h : p ≠ s.endPos, p.get h = '0' then
demangleAux s (p.next h.2.1) res "" 0
else
decodeNum s p res (ch.val - 48).toNat
@ -167,40 +167,40 @@ def Name.demangleAux (s : String) (p₀ : s.ValidPos) (res : Name)
match ch, h₁ : parseLowerHex? 2 s p 0 with
| 'x', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₁)
have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₁)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ =>
match ch, h₂ : parseLowerHex? 4 s p 0 with
| 'u', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₂)
have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₂)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ =>
match ch, h₃ : parseLowerHex? 8 s p 0 with
| 'U', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₃)
have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₃)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ => demangleAux s p (res.str acc) ("".pushn '_' (ucount / 2) |>.push ch) 0
termination_by p₀
where
decodeNum (s : String) (p : s.ValidPos) (res : Name) (n : Nat) : Name :=
if h : p = s.endValidPos then res.num n else
decodeNum (s : String) (p : s.Pos) (res : Name) (n : Nat) : Name :=
if h : p = s.endPos then res.num n else
let ch := p.get h
let p := p.next h
if ch.isDigit then
decodeNum s p res (n * 10 + (ch.val - 48).toNat)
else -- assume ch = '_'
let res := res.num n
if h : p = s.endValidPos then res else
if h : p = s.endPos then res else
nameStart s (p.next h) res -- assume s.get' p h = '_'
termination_by p
nameStart (s : String) (p : s.ValidPos) (res : Name) : Name :=
if h : p = s.endValidPos then res else
nameStart (s : String) (p : s.Pos) (res : Name) : Name :=
if h : p = s.endPos then res else
let ch := p.get h
let p := p.next h
if ch.isDigit then
if h : ch = '0' ∧ ∃ h : p ≠ s.endValidPos, p.get h = '0' then
if h : ch = '0' ∧ ∃ h : p ≠ s.endPos, p.get h = '0' then
demangleAux s (p.next h.2.1) res "" 0
else
decodeNum s p res (ch.val - 48).toNat
@ -212,7 +212,7 @@ where
/-- Assuming `s` has been produced by `Name.mangle _ ""`, return the original name. -/
public def Name.demangle (s : String) : Name :=
demangleAux.nameStart s s.startValidPos .anonymous
demangleAux.nameStart s s.startPos .anonymous
/--
Returns the demangled version of `s`, if it's the result of `Name.mangle _ ""`. Otherwise returns

4
src/Lean/Data/EditDistance.lean
View file

@ -32,11 +32,11 @@ public def levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat := Id.ru
for h : i in [0:v0.size] do
v0 := v0.set i i
let mut iter1 := str1.startValidPos
let mut iter1 := str1.startPos
let mut i := 0
while h1 : ¬iter1.IsAtEnd do
v1 := v1.set 0 (i+1)
let mut iter2 := str2.startValidPos
let mut iter2 := str2.startPos
let mut j : Fin (len2 + 1) := 0
while h2 : ¬iter2.IsAtEnd do
let j' : Fin _ := j + 1

4
src/Lean/DocString/Links.lean
View file

@ -106,7 +106,7 @@ def rewriteManualLinksCore (s : String) : Id (Array (Lean.Syntax.Range × String
let scheme := "lean-manual://"
let mut out := ""
let mut errors := #[]
let mut iter := s.startValidPos
let mut iter := s.startPos
while h : ¬iter.IsAtEnd do
let c := iter.get h
let pre := iter
@ -155,7 +155,7 @@ where
/--
Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
-/
lookingAt (goal : String) {s : String} (iter : s.ValidPos) : Bool :=
lookingAt (goal : String) {s : String} (iter : s.Pos) : Bool :=
String.Pos.Raw.substrEq s iter.offset goal 0 goal.rawEndPos.byteIdx
/--

6
src/Lean/DocString/Markdown.lean
View file

@ -151,7 +151,7 @@ public instance : MarkdownBlock i Empty where
private def escape (s : String) : String := Id.run do
let mut s' := ""
let mut iter := s.startValidPos
let mut iter := s.startPos
while h : ¬iter.IsAtEnd do
let c := iter.get h
iter := iter.next h
@ -165,7 +165,7 @@ where
private def quoteCode (str : String) : String := Id.run do
let mut longest := 0
let mut current := 0
let mut iter := str.startValidPos
let mut iter := str.startPos
while h : ¬iter.IsAtEnd do
let c := iter.get h
iter := iter.next h
@ -273,7 +273,7 @@ public instance [MarkdownInline i] : ToMarkdown (Inline i) where
private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
let mut longest := 2
let mut current := 0
let mut iter := str.startValidPos
let mut iter := str.startPos
let mut out := ""
while h : ¬iter.IsAtEnd do
let c := iter.get h

6
src/Lean/DocString/Parser.lean
View file

@ -123,7 +123,7 @@ private def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) :
private def unescapeStr (str : String) : String := Id.run do
let mut out := ""
let mut iter := str.startValidPos
let mut iter := str.startPos
while h : ¬iter.IsAtEnd do
let c := iter.get h
iter := iter.next h
@ -246,7 +246,7 @@ private def pushMissing : ParserFn := fun _c s =>
s.pushSyntax .missing
private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
let rec go (iter : str.ValidPos) (s : ParserState) :=
let rec go (iter : str.Pos) (s : ParserState) :=
if h : iter.IsAtEnd then s
else
let ch := iter.get h
@ -254,7 +254,7 @@ private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
termination_by iter
let iniPos := s.pos
let iniSz := s.stxStack.size
let s := go str.startValidPos s
let s := go str.startPos s
if s.hasError then s.mkErrorAt s!"'{str}'" iniPos (some iniSz) else s
/--

2
src/Lean/ErrorExplanation.lean
View file

@ -94,7 +94,7 @@ where
prior to the next whitespace.
-/
upToWs (nonempty : Bool) : Parser String := fun it =>
let it' := (it.2.find? fun (c : Char) => c.isWhitespace).getD it.1.endValidPos
let it' := (it.2.find? fun (c : Char) => c.isWhitespace).getD it.1.endPos
if nonempty && it' == it.2 then
.error ⟨_, it'⟩ (.other "Expected a nonempty string")
else

4
src/Lean/Meta/TryThis.lean
View file

@ -190,8 +190,8 @@ def getIndentAndColumn (map : FileMap) (range : Lean.Syntax.Range) : Nat × Nat
let body := (map.source.slice! start rangeStart).find (fun c => c != ' ') |>.str.offset
(start.offset.byteDistance body, start.offset.byteDistance range.start)
where
findLineStart {s : String} (p : s.ValidPos) : s.ValidPos :=
p.revFind? '\n' |>.map (·.next!) |>.getD s.startValidPos
findLineStart {s : String} (p : s.Pos) : s.Pos :=
p.revFind? '\n' |>.map (·.next!) |>.getD s.startPos
/--
An option allowing the user to customize the ideal input width. Defaults to 100.

4
src/Lean/Server/FileWorker/ExampleHover.lean
View file

@ -30,7 +30,7 @@ line comment marker.
-/
private def addCommentAt (indent : Nat) (line : String) : String := Id.run do
let s := "".pushn ' ' indent ++ "-- "
let mut iter := line.startValidPos
let mut iter := line.startPos
for _i in *...indent do
if h : ¬iter.IsAtEnd then
if iter.get h == ' ' then
@ -53,7 +53,7 @@ Splits a string into lines, preserving newline characters.
-/
private def lines (s : String) : Array String := Id.run do
let mut result := #[]
let mut lineStart := s.startValidPos
let mut lineStart := s.startPos
let mut iter := lineStart
while h : ¬iter.IsAtEnd do
let c := iter.get h

2
src/Lean/Server/FileWorker/SignatureHelp.lean
View file

@ -84,7 +84,7 @@ inductive SearchControl where
/-- Stop the search through a syntax stack. -/
| stop
private def lineCommentPosition? (s : String) : Option s.ValidPos :=
private def lineCommentPosition? (s : String) : Option s.Pos :=
s.find? "--"
private def isPositionInLineComment (text : FileMap) (pos : String.Pos.Raw) : Bool := Id.run do

14
src/Std/Internal/Parsec/String.lean
View file

@ -16,7 +16,7 @@ namespace Std.Internal
namespace Parsec
namespace String
instance : Input (Sigma String.ValidPos) Char String.Pos.Raw where
instance : Input (Sigma String.Pos) Char String.Pos.Raw where
pos it := it.2.offset
next it := ⟨it.1, it.2.next!⟩
curr it := it.2.get!
@ -25,15 +25,15 @@ instance : Input (Sigma String.ValidPos) Char String.Pos.Raw where
curr' it h := it.2.get (by simpa using h)
/--
`Parser α` is a parser that consumes a `String` input using a `Sigma String.ValidPos` and returns a result of type `α`.
`Parser α` is a parser that consumes a `String` input using a `Sigma String.Pos` and returns a result of type `α`.
-/
abbrev Parser (α : Type) : Type := Parsec (Sigma String.ValidPos) α
abbrev Parser (α : Type) : Type := Parsec (Sigma String.Pos) α
/--
Run a `Parser` on a `String`, returns either the result or an error string with offset.
-/
protected def Parser.run (p : Parser α) (s : String) : Except String α :=
match p ⟨s, s.startValidPos⟩ with
match p ⟨s, s.startPos⟩ with
| .success _ res => Except.ok res
| .error it err => Except.error s!"offset {repr it.2.offset.byteIdx}: {err}"
@ -88,7 +88,7 @@ private def digitsCore (acc : Nat) : Parser Nat := fun it =>
let ⟨res, it⟩ := go it.2 acc
.success ⟨_, it⟩ res
where
go {s : String} (it : s.ValidPos) (acc : Nat) : (Nat × s.ValidPos) :=
go {s : String} (it : s.Pos) (acc : Nat) : (Nat × s.Pos) :=
if h : ¬it.IsAtEnd then
let candidate := it.get h
if '0' ≤ candidate ∧ candidate ≤ '9' then
@ -127,7 +127,7 @@ def asciiLetter : Parser Char := attempt do
let c ← any
if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then return c else fail s!"ASCII letter expected"
private def skipWs {s : String} (it : s.ValidPos) : s.ValidPos :=
private def skipWs {s : String} (it : s.Pos) : s.Pos :=
if h : ¬it.IsAtEnd then
let c := it.get h
if c = '\u0009' ∨ c = '\u000a' ∨ c = '\u000d' ∨ c = '\u0020' then
@ -150,7 +150,7 @@ Takes a fixed amount of chars from the iterator.
-/
def take (n : Nat) : Parser String := fun it =>
let right := it.2.nextn n
let substr := String.Slice.mk it.1 it.2 right String.ValidPos.le_nextn |>.copy
let substr := String.Slice.mk it.1 it.2 right String.Pos.le_nextn |>.copy
if substr.length != n then
.error it .eof
else

2
src/lake/Lake/CLI/Main.lean
View file

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

4
src/lake/Lake/Config/Artifact.lean
View file

@ -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.startValidPos.extract pos
let some hash := Hash.ofString? <| s.startPos.extract pos
| throw "expected artifact file name to be a content hash"
let ext := (pos.next h).extract s.endValidPos
let ext := (pos.next h).extract s.endPos
return {hash, ext}
public protected def fromJson? (data : Json) : Except String ArtifactDescr := do

2
src/lake/Lake/Config/Cache.lean
View file

@ -47,7 +47,7 @@ def checkSchemaVersion (inputName : String) (line : String) : LogIO Unit := do
/-- Parse a `Cache` from a JSON Lines string. -/
public partial def parse (inputName : String) (contents : String) : LoggerIO CacheMap := do
let rec loop (i : Nat) (cache : CacheMap) {contents : String} (pos : contents.ValidPos) := do
let rec loop (i : Nat) (cache : CacheMap) {contents : String} (pos : contents.Pos) := do
let lfPos := pos.find '\n'
let line := contents.slice! pos lfPos
if line.trimAscii.isEmpty then

12
src/lake/Lake/Util/Cli.lean
View file

@ -99,20 +99,20 @@ variable [Monad m] [MonadStateOf ArgList m]
/-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/
@[inline] public def longOptionOrSpace (handle : String → m α) (opt : String) : m α :=
let pos := opt.find ' '
if h : pos = opt.endValidPos then
if h : pos = opt.endPos then
handle opt
else do
consArg <| (pos.next h).extract opt.endValidPos
handle <| opt.startValidPos.extract pos
consArg <| (pos.next h).extract opt.endPos
handle <| opt.startPos.extract 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.endValidPos then
if h : pos = opt.endPos then
handle opt
else do
consArg <| (pos.next h).extract opt.endValidPos
handle <| opt.startValidPos.extract pos
consArg <| (pos.next h).extract opt.endPos
handle <| opt.startPos.extract pos
/-- Process a long option of the form `--long`, `--long=arg`, `"--long arg"`. -/
@[inline] public def longOption (handle : String → m α) : String → m α :=

46
src/lake/Lake/Util/Version.lean
View file

@ -31,11 +31,11 @@ Components are composed of alphanumerics or a `*`.
-/
@[inline] def parseVerComponents
(s : String)
: EStateM String s.ValidPos (Array String.Slice) :=
fun p => go #[] p p (String.ValidPos.le_refl _)
: EStateM String s.Pos (Array String.Slice) :=
fun p => go #[] p p (String.Pos.le_refl _)
where
go cs iniPos p (iniPos_le : iniPos ≤ p) :=
if h : p = s.endValidPos then
if h : p = s.endPos then
let c := String.Slice.mk s iniPos p iniPos_le
.ok (cs.push c) p
else
@ -45,7 +45,7 @@ where
go (cs.push c) (p.next h) (p.next h) (Nat.le_refl _)
else if c.isAlphanum || c == '*' then
go cs iniPos (p.next h)
(String.ValidPos.le_trans iniPos_le (String.ValidPos.le_of_lt p.lt_next))
(String.Pos.le_trans iniPos_le (String.Pos.le_of_lt p.lt_next))
else
let c := String.Slice.mk s iniPos p iniPos_le
.ok (cs.push c) p
@ -78,9 +78,9 @@ private def parseVerComponent {σ} (what : String) (s? : Option String.Slice) :
| throw s!"invalid {what} version: expected numeral or wildcard, got '{s.copy}'"
return .nat n
def parseSpecialDescr? (s : String) : EStateM String s.ValidPos (Option String) := do
def parseSpecialDescr? (s : String) : EStateM String s.Pos (Option String) := do
let p ← get
if h : p = s.endValidPos then
if h : p = s.endPos then
return none
else
let c := p.get h
@ -94,7 +94,7 @@ def parseSpecialDescr? (s : String) : EStateM String s.ValidPos (Option String)
return none
where
nextUntilWhitespace p :=
if h : p = s.endValidPos then
if h : p = s.endPos then
p
else if (p.get h).isWhitespace then
p
@ -102,7 +102,7 @@ where
nextUntilWhitespace (p.next h)
termination_by p
private def parseSpecialDescr (s : String) : EStateM String s.ValidPos String := do
private def parseSpecialDescr (s : String) : EStateM String s.Pos String := do
let some specialDescr ← parseSpecialDescr? s
| return ""
if specialDescr.isEmpty then
@ -110,8 +110,8 @@ private def parseSpecialDescr (s : String) : EStateM String s.ValidPos String :=
return specialDescr
private def runVerParse
(s : String) (x : (s : String) → EStateM String s.ValidPos α)
(startPos := s.startValidPos) (endPos := s.endValidPos)
(s : String) (x : (s : String) → EStateM String s.Pos α)
(startPos := s.startPos) (endPos := s.endPos)
: Except String α :=
match x s startPos with
| .ok v p =>
@ -138,7 +138,7 @@ public instance : LE SemVerCore := leOfOrd
public instance : Min SemVerCore := minOfLe
public instance : Max SemVerCore := maxOfLe
def parseM (s : String) : EStateM String s.ValidPos SemVerCore := do
def parseM (s : String) : EStateM String s.Pos SemVerCore := do
try
let cs ← parseVerComponents s
if h : cs.size = 3 then
@ -202,7 +202,7 @@ public instance : LE StdVer := leOfOrd
public instance : Min StdVer := minOfLe
public instance : Max StdVer := maxOfLe
public def parseM (s : String) : EStateM String s.ValidPos StdVer := do
public def parseM (s : String) : EStateM String s.Pos StdVer := do
let core ← SemVerCore.parseM s
let specialDescr ← parseSpecialDescr s
return {toSemVerCore := core, specialDescr}
@ -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.startValidPos.extract colonPos, pos.extract ver.endValidPos)
(ver.startPos.extract colonPos, pos.extract ver.endPos)
else
("", ver)
let noOrigin := origin.isEmpty
@ -348,7 +348,7 @@ namespace ComparatorOp
def parseM
(s : String)
: EStateM String s.ValidPos ComparatorOp := fun p =>
: EStateM String s.Pos ComparatorOp := fun p =>
if let some (tk, op) := trie.matchPrefix s p.offset then
let p' := p.offset + tk
if h : p'.IsValid s then
@ -371,8 +371,8 @@ where trie :=
|> add "≠" .ne
public def ofString? (s : String) : Option ComparatorOp :=
match parseM s s.startValidPos with
| .ok op p => if p = s.endValidPos then some op else none
match parseM s s.startPos with
| .ok op p => if p = s.endPos then some op else none
| .error .. => none
public protected def toString (self : ComparatorOp) : String :=
@ -403,7 +403,7 @@ public def wild : VerComparator :=
public instance : Inhabited VerComparator := ⟨.wild⟩
def parseM (s : String) : EStateM String s.ValidPos VerComparator := do
def parseM (s : String) : EStateM String s.Pos VerComparator := do
let op ← ComparatorOp.parseM s
let core ← SemVerCore.parseM s
if let some specialDescr ← parseSpecialDescr? s then
@ -480,12 +480,12 @@ where
ands.foldl (init := ands[0].toString) (start := 1) fun s v =>
s!"{s}, {v}"
partial def parseM (s : String) : EStateM String s.ValidPos VerRange := do
partial def parseM (s : String) : EStateM String s.Pos VerRange := do
let clauses ← go true #[] #[]
return {toString := s, clauses}
where
go needsRange ors (ands : Array VerComparator) p :=
if h : p = s.endValidPos then
if h : p = s.endPos then
if needsRange || ands.size == 0 then
.error "expected version range" p
else
@ -516,7 +516,7 @@ where
go true ors ands (p.next h)
else if c == '|' then
let p := p.next h
if h : p = s.endValidPos then
if h : p = s.endPos then
.error "expected '|' after first '|'" p
else if p.get h = '|' then
if ands.size = 0 then
@ -534,7 +534,7 @@ where
let minVer := StdVer.mk minVer specialDescr
let maxVer := StdVer.ofSemVerCore maxVer
ands.push {op := .ge, ver := minVer} |>.push {op := .lt, ver := maxVer, includeSuffixes := true}
parseWild (s : String) ands : EStateM String s.ValidPos _ := do
parseWild (s : String) ands : EStateM String s.Pos _ := do
let cs ← parseVerComponents s
if (← get).get?.any (· == '-') then
throw s!"invalid wildcard range: wildcard versions do not support suffixes"
@ -559,7 +559,7 @@ where
otherwise, use '≥' to support it and future versions"
| _, _, _ =>
return ands.push .wild
parseCaret (s : String) ands : EStateM String s.ValidPos _ := do
parseCaret (s : String) ands : EStateM String s.Pos _ := do
let cs ← parseVerComponents s
let specialDescr ← parseSpecialDescr s
if h : cs.size = 1 then
@ -588,7 +588,7 @@ where
return appendRange ands {major, minor, patch} {major := major + 1} specialDescr
else
throw s!"invalid caret range: incorrect number of components: got {cs.size}, expected 1-3"
parseTilde (s : String) ands : EStateM String s.ValidPos _ := do
parseTilde (s : String) ands : EStateM String s.Pos _ := do
let cs ← parseVerComponents s
let specialDescr ← parseSpecialDescr s
if h : cs.size = 1 then

2
tests/compiler/partial.lean
View file

@ -2,7 +2,7 @@
set_option pp.explicit true
-- set_option trace.compiler.boxed true
partial def contains : String → Char → String.Pos → Bool
partial def contains : String → Char → String.Pos.Raw → Bool
| s, c, i =>
if s.atEnd i then false
else if s.get i == c then true

2
tests/compiler/trie.lean
View file

@ -70,7 +70,7 @@ def T.check : T → IO Unit := fun (t,a) => do
unless t.matchPrefix s 0 = a.matchPrefix s do
IO.println s!"matchPrefix differs: key = {s}, got: {t.matchPrefix s 0} exp: {a.matchPrefix s} "
let s' := "somePrefix" ++ s
unless t.matchPrefix s' ((0 : String.Pos) + "somePrefix") = a.matchPrefix s do
unless t.matchPrefix s' ((0 : String.Pos.Raw) + "somePrefix") = a.matchPrefix s do
IO.println s!"matchPrefix differs (with prefix): key = {s}"
def main : IO Unit := do

2
tests/lean/1363.lean
View file

@ -19,7 +19,7 @@ def h : Nat → Nat → Nat
termination_by x y => x
@[macro_inline] -- Error
partial def skipMany (p : Parser α) (it : Sigma String.ValidPos) : Parser PUnit := do
partial def skipMany (p : Parser α) (it : Sigma String.Pos) : Parser PUnit := do
match p it with
| .success it _ => skipMany p it
| .error _ _ => pure ()

2
tests/lean/docparse/run.lean
View file

@ -57,7 +57,7 @@ def test (p : ParserFn) (input : String) : IO String := do
s!" {repr <| input.extract p input.rawEndPos}\n"
return s!"{s'.allErrors.size} failures:\n{errors}\nFinal stack:\n{stk.pretty 50}"
where
errLt (x y : String.Pos × SyntaxStack × Error) : Bool :=
errLt (x y : String.Pos.Raw × SyntaxStack × Error) : Bool :=
let (p1, _, e1) := x
let (p2, _, e2) := y
p1 < p2 || p1 == p2 && toString e1 < toString e2

8
tests/lean/run/matchCongrEqns.lean
View file

@ -91,14 +91,14 @@ info: matchOptionUnit.match_1.congr_eq_1.{u_1} (motive : Option Unit → Sort u_
#check matchOptionUnit.match_1.congr_eq_1
set_option linter.unusedVariables false in
partial def utf16PosToCodepointPosFromAux (s : String) : Nat → String.Pos → Nat → Bool
partial def utf16PosToCodepointPosFromAux (s : String) : Nat → String.Pos.Raw → Nat → Bool
| 0, _, cp => true
| utf16pos, utf8pos, cp => false
/--
info: utf16PosToCodepointPosFromAux.match_1.congr_eq_1.{u_1} (motive : Nat → String.Pos → Nat → Sort u_1) (x✝ : Nat)
(x✝¹ : String.Pos) (x✝² : Nat) (h_1 : (x : String.Pos) → (cp : Nat) → motive 0 x cp)
(h_2 : (utf16pos : Nat) → (utf8pos : String.Pos) → (cp : Nat) → motive utf16pos utf8pos cp) (x✝³ : String.Pos)
info: utf16PosToCodepointPosFromAux.match_1.congr_eq_1.{u_1} (motive : Nat → String.Pos.Raw → Nat → Sort u_1) (x✝ : Nat)
(x✝¹ : String.Pos.Raw) (x✝² : Nat) (h_1 : (x : String.Pos.Raw) → (cp : Nat) → motive 0 x cp)
(h_2 : (utf16pos : Nat) → (utf8pos : String.Pos.Raw) → (cp : Nat) → motive utf16pos utf8pos cp) (x✝³ : String.Pos.Raw)
(cp : Nat) (heq_1 : x✝ = 0) (heq_2 : x✝¹ = x✝³) (heq_3 : x✝² = cp) :
(match x✝, x✝¹, x✝² with
| 0, x, cp => h_1 x cp

4
tests/lean/run/partial_fixpoint_monadic.lean
View file

@ -6,7 +6,7 @@ Testing `partial_fixpoint` with monad transformers
Using an `Option`-based monad
-/
abbrev M1 := ReaderT String (StateT String.Pos Option)
abbrev M1 := ReaderT String (StateT String.Pos.Raw Option)
def parseAll1 (x : M1 α) : M1 (List α) := do
if (← read).atEnd (← get) then
@ -37,7 +37,7 @@ theorem parseAll1.eq_1 : ∀ {α : Type} (x : M1 α),
Using an `IO`-based monad
-/
abbrev M2 := ReaderT String (StateRefT String.Pos IO)
abbrev M2 := ReaderT String (StateRefT String.Pos.Raw IO)
def parseAll2 (x : M2 α) : M2 (List α) := do
if (← read).atEnd (← get) then

14
tests/lean/run/string_termination.lean
View file

@ -2,17 +2,17 @@ module
-- Test that termination proofs for stepping through a string with `next` and `prev` works.
def isConsonant (i : String.ValidPos str) : Bool :=
def isConsonant (i : String.Pos str) : Bool :=
match i.get! with
| 'a' | 'e' | 'i' | 'o' | 'u' => false
| 'y' =>
if h : i = str.startValidPos then true
if h : i = str.startPos then true
else !isConsonant (i.prev h)
| _ => true
termination_by i.down
def measure₁ (word : String) : Nat :=
let rec aux (pos : String.ValidPos word) (inVowel : Bool) (count : Nat) : Nat :=
let rec aux (pos : String.Pos word) (inVowel : Bool) (count : Nat) : Nat :=
match h : pos.next? with
| some next =>
if !isConsonant pos then
@ -24,11 +24,11 @@ def measure₁ (word : String) : Nat :=
| none => count
termination_by pos
aux word.startValidPos false 0
aux word.startPos false 0
def measure₂ (word : String) : Nat :=
let rec aux (pos : String.ValidPos word) (inVowel : Bool) (count : Nat) : Nat :=
if h : pos = word.endValidPos then count
let rec aux (pos : String.Pos word) (inVowel : Bool) (count : Nat) : Nat :=
if h : pos = word.endPos then count
else
let next := pos.next h
if !isConsonant pos then
@ -39,4 +39,4 @@ def measure₂ (word : String) : Nat :=
aux next false count
termination_by pos
aux word.startValidPos false 0
aux word.startPos false 0