From b28daa6d608ba0bd29f45b42743b403e0a915fce Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 21 Oct 2025 13:25:30 +0200 Subject: [PATCH] chore: rename `String.endPos` -> `String.rawEndPos` (#10853) This PR renames `String.endPos` to `String.rawEndPos`, as in a future release the name `String.endPos` will be taken by the function that is currently called `String.endValidPos`. --- script/Modulize.lean | 6 +- script/Shake.lean | 4 +- src/Init/Data/Format/Basic.lean | 6 +- src/Init/Data/String/Basic.lean | 251 ++++++++++-------- src/Init/Meta/Defs.lean | 2 +- src/Init/Prelude.lean | 10 +- src/Init/System/FilePath.lean | 4 +- src/Lean/Data/Lsp/LanguageFeatures.lean | 4 +- src/Lean/DocString/Add.lean | 4 +- src/Lean/DocString/Extension.lean | 4 +- src/Lean/DocString/Links.lean | 2 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 2 +- src/Lean/Elab/DocString.lean | 2 +- src/Lean/Elab/DocString/Builtin.lean | 2 +- src/Lean/Elab/DocString/Builtin/Parsing.lean | 4 +- src/Lean/Elab/StructInstHint.lean | 2 +- src/Lean/Elab/Syntax.lean | 2 +- src/Lean/ErrorExplanation.lean | 2 +- src/Lean/Language/Basic.lean | 2 +- src/Lean/Meta/Hint.lean | 2 +- src/Lean/Meta/Tactic/Grind/Intro.lean | 4 +- src/Lean/Parser/Basic.lean | 2 +- src/Lean/Parser/Extension.lean | 6 +- src/Lean/Parser/Term.lean | 2 +- src/Lean/Parser/Types.lean | 16 +- src/Lean/PrettyPrinter/Formatter.lean | 4 +- src/Lean/Server/FileWorker.lean | 6 +- .../Server/FileWorker/RequestHandling.lean | 4 +- .../Server/FileWorker/WidgetRequests.lean | 6 +- src/Lean/Server/InfoUtils.lean | 2 +- src/Lean/Server/Requests.lean | 6 +- src/Lean/Server/Test/Runner.lean | 4 +- src/Lean/Server/Utils.lean | 4 +- src/Lean/Shell.lean | 2 +- src/lake/Lake/CLI/Main.lean | 4 +- src/lake/Lake/Config/Artifact.lean | 2 +- src/lake/Lake/Config/Cache.lean | 4 +- src/lake/Lake/Toml/Elab/Value.lean | 6 +- src/lake/Lake/Util/Cli.lean | 8 +- src/lake/Lake/Util/FilePath.lean | 2 +- src/lake/Lake/Util/Version.lean | 8 +- tests/bench/workspaceSymbolsNewRanges.lean | 2 +- tests/compiler/str.lean | 2 +- tests/lean/docparse/run.lean | 8 +- .../lean/run/frontend_meeting_2022_09_13.lean | 2 +- tests/lean/run/parseEnd.lean | 2 +- tests/lean/run/string.lean | 6 +- 48 files changed, 238 insertions(+), 205 deletions(-) diff --git a/script/Modulize.lean b/script/Modulize.lean index 766073b8b6..9f55f2b7e8 100644 --- a/script/Modulize.lean +++ b/script/Modulize.lean @@ -57,19 +57,19 @@ def main (args : List String) : IO Unit := do sec := "\n\n" ++ sec if insertPos?.isNone then sec := sec ++ "\n\n" - text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos + text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos -- prepend each import with `public ` for imp in imps.reverse do let insertPos := imp.raw.getPos?.get! let prfx := if doMeta then "public meta " else "public " - text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos + text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos -- insert `module` header let mut initText := text.extract 0 startPos if !initText.trim.isEmpty then -- If there is a header comment, preserve it and put `module` in the line after initText := initText.trimRight ++ "\n" - text := initText ++ "module\n\n" ++ text.extract startPos text.endPos + text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos IO.FS.writeFile path text diff --git a/script/Shake.lean b/script/Shake.lean index ea853993e7..0378a944c1 100644 --- a/script/Shake.lean +++ b/script/Shake.lean @@ -563,14 +563,14 @@ def main (args : List String) : IO UInt32 := do if remove.contains mod || seen.contains mod then out := out ++ text.extract 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.endPos stx.raw.getTailPos?.get! + ⟨1⟩ + pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + ⟨1⟩ seen := seen.insert mod out := out ++ text.extract 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.endPos + out := out ++ text.extract insertion text.rawEndPos IO.FS.writeFile path out return count + 1 diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index c6ee0e995f..4f61c1465d 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -170,7 +170,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult | text s, flatten, _, _ => let p := String.Internal.posOf s '\n' let off := String.Internal.offsetOfPos s p - { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off } + { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off } | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m) | nest n f, flatten, m, w => spaceUptoLine f flatten (m - n) w | group f _, _, m, w => spaceUptoLine f true m w @@ -264,14 +264,14 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou | nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is)) | text s => let p := String.Internal.posOf s '\n' - if p == s.endPos then + if p == s.rawEndPos then pushOutput s endTags i.activeTags be w (gs' is) else pushOutput (String.Internal.extract s {} p) pushNewline i.indent.toNat - let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is + let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is -- after a hard line break, re-evaluate whether to flatten the remaining group -- note that we shouldn't start flattening after a hard break outside a group if g.fla == .disallow then diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index b657235f6c..6a081cffc5 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -520,8 +520,22 @@ theorem Pos.Raw.le_iff {i₁ i₂ : Pos.Raw} : i₁ ≤ i₂ ↔ i₁.byteIdx theorem Pos.Raw.lt_iff {i₁ i₂ : Pos.Raw} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx := .rfl +@[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 + @[simp] -theorem byteIdx_endPos {s : String} : s.endPos.byteIdx = s.utf8ByteSize := rfl +theorem rawStartPos_eq {s : String} : s.rawStartPos = 0 := (rfl) + +@[simp] +theorem byteIdx_rawEndPos {s : String} : s.rawEndPos.byteIdx = s.utf8ByteSize := rfl + +@[deprecated byteIdx_rawEndPos (since := "2025-10-20")] +theorem byteIdx_endPos {s : String} : s.rawEndPos.byteIdx = s.utf8ByteSize := rfl @[simp] theorem utf8ByteSize_ofByteArray {b : ByteArray} {h} : @@ -595,9 +609,14 @@ Examples: * `String.Pos.IsValid "𝒫(A)" ⟨4⟩` -/ structure Pos.Raw.IsValid (s : String) (off : String.Pos.Raw) : Prop where private mk :: - le_endPos : off ≤ s.endPos + le_rawEndPos : off ≤ s.rawEndPos isValidUTF8_extract_zero : (s.bytes.extract 0 off.byteIdx).IsValidUTF8 +@[deprecated le_rawEndPos (since := "2025-10-20")] +theorem Pos.Raw.IsValid.le_endPos {s : String} {off : String.Pos.Raw} (h : off.IsValid s) : + off ≤ s.rawEndPos := + h.le_rawEndPos + theorem _root_.List.isPrefix_of_utf8Encode_append_eq_utf8Encode {l m : List Char} (b : ByteArray) (h : l.utf8Encode ++ b = m.utf8Encode) : l <+: m := by induction l generalizing m with @@ -628,7 +647,7 @@ theorem Pos.Raw.IsValid.exists {s : String} {p : Pos.Raw} (h : p.IsValid s) : apply List.isPrefix_of_utf8Encode_append_eq_utf8Encode (s.bytes.extract p.byteIdx s.bytes.size) rw [← hl, ← hm₁, ← ByteArray.extract_eq_extract_append_extract _ (by simp), ByteArray.extract_zero_size] - simpa using h.le_endPos + simpa using h.le_rawEndPos theorem Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize {s : String} {p : Pos.Raw} (h : p.IsValid s) : ByteArray.IsValidUTF8 (s.bytes.extract p.byteIdx s.utf8ByteSize) := by @@ -640,16 +659,16 @@ theorem Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize {s : String} {p : Pos.R simp only [List.asString_append, bytes_append, List.bytes_asString, ByteArray.size_extract, ByteArray.size_append, Nat.sub_zero] refine (Nat.min_eq_left ?_).symm - simpa [utf8ByteSize, Pos.Raw.le_iff] using h.le_endPos + simpa [utf8ByteSize, Pos.Raw.le_iff] using h.le_rawEndPos · simp [utf8ByteSize] theorem Pos.Raw.isValid_iff_exists_append {s : String} {p : Pos.Raw} : - p.IsValid s ↔ ∃ s₁ s₂ : String, s = s₁ ++ s₂ ∧ p = s₁.endPos := by + p.IsValid s ↔ ∃ s₁ s₂ : String, s = s₁ ++ s₂ ∧ p = s₁.rawEndPos := by refine ⟨fun h => ⟨⟨_, h.isValidUTF8_extract_zero⟩, ⟨_, h.isValidUTF8_extract_utf8ByteSize⟩, ?_, ?_⟩, ?_⟩ · apply String.bytes_inj.1 - have := Pos.Raw.le_iff.1 h.le_endPos + have := Pos.Raw.le_iff.1 h.le_rawEndPos simp_all [← size_bytes] - · have := byteIdx_endPos ▸ Pos.Raw.le_iff.1 h.le_endPos + · have := byteIdx_rawEndPos ▸ Pos.Raw.le_iff.1 h.le_rawEndPos apply String.Pos.Raw.ext simp [Nat.min_eq_left this] · rintro ⟨s₁, s₂, rfl, rfl⟩ @@ -661,19 +680,19 @@ theorem Pos.Raw.byteIdx_zero : (0 : Pos.Raw).byteIdx = 0 := rfl @[simp] theorem Pos.Raw.isValid_zero {s : String} : (0 : Pos.Raw).IsValid s where - le_endPos := by simp [Pos.Raw.le_iff] + le_rawEndPos := by simp [Pos.Raw.le_iff] isValidUTF8_extract_zero := by simp @[simp] -theorem Pos.Raw.isValid_endPos {s : String} : s.endPos.IsValid s where - le_endPos := by simp [Pos.Raw.le_iff] +theorem Pos.Raw.isValid_rawEndPos {s : String} : s.rawEndPos.IsValid s where + le_rawEndPos := by simp [Pos.Raw.le_iff] isValidUTF8_extract_zero := by simp [← size_bytes, s.isValidUTF8] @[simp] theorem Pos.Raw.isValid_empty_iff {p : Pos.Raw} : p.IsValid "" ↔ p = 0 := by refine ⟨?_, ?_⟩ · rintro ⟨h₁, h₂⟩ - simp only [le_iff, byteIdx_endPos, utf8ByteSize_empty, Nat.le_zero_eq] at h₁ + simp only [le_iff, byteIdx_rawEndPos, utf8ByteSize_empty, Nat.le_zero_eq] at h₁ ext omega · rintro rfl @@ -752,7 +771,7 @@ theorem Pos.Raw.byteIdx_add_char {p : Pos.Raw} {c : Char} : (p + c).byteIdx = p. theorem Pos.Raw.byteIdx_char_add {c : Char} {p : Pos.Raw} : (c + p).byteIdx = c.utf8Size + p.byteIdx := rfl theorem Pos.Raw.isValid_append {s t : String} {p : Pos.Raw} : - p.IsValid (s ++ t) ↔ p.IsValid s ∨ (s.endPos ≤ p ∧ (p - s).IsValid t) := by + p.IsValid (s ++ t) ↔ p.IsValid s ∨ (s.rawEndPos ≤ p ∧ (p - s).IsValid t) := by obtain ⟨s, rfl⟩ := exists_eq_asString s obtain ⟨t, rfl⟩ := exists_eq_asString t rw [← List.asString_append, Pos.Raw.isValid_asString, Pos.Raw.isValid_asString, Pos.Raw.isValid_asString] @@ -767,7 +786,7 @@ theorem Pos.Raw.isValid_append {s t : String} {p : Pos.Raw} : · refine ⟨min j s.length, ?_⟩ rw [List.take_append_of_le_length (Nat.min_le_right ..), ← List.take_eq_take_min, hj] · refine ⟨s.length + j, ?_⟩ - simp only [Pos.Raw.byteIdx_sub_string, byteIdx_endPos, Pos.Raw.le_iff] at hj h + simp only [Pos.Raw.byteIdx_sub_string, byteIdx_rawEndPos, Pos.Raw.le_iff] at hj h simp only [List.take_append, List.take_of_length_le (i := s.length + j) (l := s) (by omega), Nat.add_sub_cancel_left, List.asString_append, utf8ByteSize_append] omega @@ -787,14 +806,14 @@ theorem append_singleton {s : String} {c : Char} : s ++ singleton c = s.push c : simp [← bytes_inj] theorem Pos.Raw.isValid_push {s : String} {c : Char} {p : Pos.Raw} : - p.IsValid (s.push c) ↔ p.IsValid s ∨ p = s.endPos + c := by + p.IsValid (s.push c) ↔ p.IsValid s ∨ p = s.rawEndPos + c := by rw [← append_singleton, isValid_append, isValid_singleton] - simp only [le_iff, byteIdx_endPos, Pos.Raw.ext_iff, byteIdx_sub_string, byteIdx_zero, byteIdx_add_char] + simp only [le_iff, byteIdx_rawEndPos, Pos.Raw.ext_iff, byteIdx_sub_string, byteIdx_zero, byteIdx_add_char] refine ⟨?_, ?_⟩ · rintro (h|⟨h₁,(h₂|h₂)⟩) · exact Or.inl h - · suffices p = s.endPos by simp [this] - simp only [Pos.Raw.ext_iff, byteIdx_endPos] + · suffices p = s.rawEndPos by simp [this] + simp only [Pos.Raw.ext_iff, byteIdx_rawEndPos] omega · omega · rintro (h|h) @@ -806,9 +825,13 @@ theorem utf8ByteSize_push {s : String} {c : Char} : (s.push c).utf8ByteSize = s.utf8ByteSize + c.utf8Size := by simp [← size_bytes, List.utf8Encode_singleton] -theorem endPos_push {s : String} {c : Char} : (s.push c).endPos = s.endPos + c := by +theorem rawEndPos_push {s : String} {c : Char} : (s.push c).rawEndPos = s.rawEndPos + c := by simp [Pos.Raw.ext_iff] +@[deprecated rawEndPos_push (since := "2025-10-20")] +theorem endPos_push {s : String} {c : Char} : (s.push c).rawEndPos = s.rawEndPos + c := + rawEndPos_push + theorem push_induction (s : String) (motive : String → Prop) (empty : motive "") (push : ∀ b c, motive b → motive (b.push c)) : motive s := by obtain ⟨m, rfl⟩ := s.exists_eq_asString @@ -834,18 +857,21 @@ Accesses the indicated byte in the UTF-8 encoding of a string. At runtime, this function is implemented by efficient, constant-time code. -/ @[extern "lean_string_get_byte_fast", expose] -def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.endPos) : UInt8 := +def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 := s.bytes[p.byteIdx] @[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast", expose] -abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.endPos) : UInt8 := +abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 := s.getUTF8Byte p h @[simp] -theorem endPos_empty : "".endPos = 0 := rfl +theorem rawEndPos_empty : "".rawEndPos = 0 := rfl + +@[deprecated rawEndPos_empty (since := "2025-10-20")] +theorem endPos_empty : "".rawEndPos = 0 := rfl theorem Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Pos.Raw} : - p.IsValid s ↔ p = s.endPos ∨ ∃ (h : p < s.endPos), (s.getUTF8Byte p h).IsUTF8FirstByte := by + p.IsValid s ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte := by induction s using push_induction with | empty => simp [Pos.Raw.lt_iff] | push s c ih => @@ -853,30 +879,30 @@ theorem Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Pos.Raw} : refine ⟨?_, ?_⟩ · rintro ((rfl|⟨h, hb⟩)|h) · refine Or.inr ⟨by simp [Pos.Raw.lt_iff, Char.utf8Size_pos], ?_⟩ - simp only [getUTF8Byte, bytes_push, byteIdx_endPos] + simp only [getUTF8Byte, bytes_push, byteIdx_rawEndPos] rw [ByteArray.getElem_append_right (by simp)] simp [List.isUTF8FirstByte_getElem_utf8Encode_singleton] · refine Or.inr ⟨by simp [lt_iff] at h ⊢; omega, ?_⟩ simp only [getUTF8Byte, bytes_push] rwa [ByteArray.getElem_append_left, ← getUTF8Byte] - · exact Or.inl (by simpa [endPos_push]) + · exact Or.inl (by simpa [rawEndPos_push]) · rintro (h|⟨h, hb⟩) - · exact Or.inr (by simpa [endPos_push] using h) + · exact Or.inr (by simpa [rawEndPos_push] using h) · simp only [getUTF8Byte, bytes_push] at hb - by_cases h' : p < s.endPos + by_cases h' : p < s.rawEndPos · refine Or.inl (Or.inr ⟨h', ?_⟩) rwa [ByteArray.getElem_append_left h', ← getUTF8Byte] at hb · refine Or.inl (Or.inl ?_) rw [ByteArray.getElem_append_right (by simp [lt_iff] at h' ⊢; omega)] at hb simp only [size_bytes, List.isUTF8FirstByte_getElem_utf8Encode_singleton] at hb ext - simp only [lt_iff, byteIdx_endPos, Nat.not_lt] at ⊢ h' + simp only [lt_iff, byteIdx_rawEndPos, Nat.not_lt] at ⊢ h' omega /-- Returns `true` if `p` is a valid UTF-8 position in the string `s`. -This means that `p ≤ s.endPos` and `p` lies on a UTF-8 character boundary. At runtime, this +This means that `p ≤ s.rawEndPos` and `p` lies on a UTF-8 character boundary. At runtime, this operation takes constant time. Examples: @@ -892,10 +918,10 @@ Examples: -/ @[extern "lean_string_is_valid_pos", expose] def Pos.Raw.isValid (s : @&String) (p : @& Pos.Raw) : Bool := - if h : p < s.endPos then + if h : p < s.rawEndPos then (s.getUTF8Byte p h).IsUTF8FirstByte else - p = s.endPos + p = s.rawEndPos @[simp] theorem Pos.Raw.isValid_eq_true_iff {s : String} {p : Pos.Raw} : p.isValid s = true ↔ p.IsValid s := by @@ -915,7 +941,7 @@ instance {s : String} {p : Pos.Raw} : Decidable (p.IsValid s) := decidable_of_iff (p.isValid s = true) Pos.Raw.isValid_eq_true_iff theorem Pos.Raw.isValid_iff_isSome_utf8DecodeChar? {s : String} {p : Pos.Raw} : - p.IsValid s ↔ p = s.endPos ∨ (s.bytes.utf8DecodeChar? p.byteIdx).isSome := by + p.IsValid s ↔ p = s.rawEndPos ∨ (s.bytes.utf8DecodeChar? p.byteIdx).isSome := by refine ⟨?_, fun h => h.elim (by rintro rfl; simp) (fun h => ?_)⟩ · induction s using push_induction with | empty => simp [ByteArray.utf8DecodeChar?] @@ -926,13 +952,13 @@ theorem Pos.Raw.isValid_iff_isSome_utf8DecodeChar? {s : String} {p : Pos.Raw} : · rw [ByteArray.utf8DecodeChar?_eq_utf8DecodeChar?_extract, ByteArray.extract_append_eq_right (by simp) (by simp)] simp · exact Or.inr (ByteArray.isSome_utf8DecodeChar?_append h _) - · simp [endPos_push] + · simp [rawEndPos_push] · refine isValid_iff_isUTF8FirstByte.2 (Or.inr ?_) obtain ⟨c, hc⟩ := Option.isSome_iff_exists.1 h refine ⟨?_, ?_⟩ · have := ByteArray.le_size_of_utf8DecodeChar?_eq_some hc have := c.utf8Size_pos - simp only [lt_iff, byteIdx_endPos, gt_iff_lt, ← size_bytes] + simp only [lt_iff, byteIdx_rawEndPos, gt_iff_lt, ← size_bytes] omega · rw [getUTF8Byte] exact ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? h @@ -957,7 +983,7 @@ protected theorem Pos.Raw.le_trans {a b c : Pos.Raw} : a ≤ b → b ≤ c → a protected theorem Pos.Raw.lt_of_lt_of_le {a b c : Pos.Raw} : a < b → b ≤ c → a < c := by simpa [le_iff, lt_iff] using Nat.lt_of_lt_of_le -theorem Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Pos.Raw) (hle : p₁ ≤ p₂) (hle' : p₂ ≤ s.endPos) : +theorem Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Pos.Raw) (hle : p₁ ≤ p₂) (hle' : p₂ ≤ s.rawEndPos) : (s.bytes.extract p₁.byteIdx p₂.byteIdx).IsValidUTF8 ↔ p₁ = p₂ ∨ (p₁.IsValid s ∧ p₂.IsValid s) := by have hle'' : p₂.byteIdx ≤ s.bytes.size := by simpa [le_iff] using hle' refine ⟨fun h => Classical.or_iff_not_imp_left.2 (fun h' => ?_), ?_⟩ @@ -987,13 +1013,13 @@ theorem Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Pos.Raw) (hle using ht.isValidUTF8_extract_utf8ByteSize theorem Pos.Raw.isValid_iff_isValidUTF8_extract_zero {s : String} {p : Pos.Raw} : - p.IsValid s ↔ p ≤ s.endPos ∧ (s.bytes.extract 0 p.byteIdx).IsValidUTF8 := + p.IsValid s ↔ p ≤ s.rawEndPos ∧ (s.bytes.extract 0 p.byteIdx).IsValidUTF8 := ⟨fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩⟩ theorem Pos.Raw.isValid_iff_isValidUTF8_extract_utf8ByteSize {s : String} {p : Pos.Raw} : - p.IsValid s ↔ p ≤ s.endPos ∧ (s.bytes.extract p.byteIdx s.utf8ByteSize).IsValidUTF8 := by - refine ⟨fun h => ⟨h.le_endPos, h.isValidUTF8_extract_utf8ByteSize⟩, fun ⟨h₁, h₂⟩ => ?_⟩ - rw [← byteIdx_endPos, isValidUTF8_extract_iff _ _ h₁ (by simp [le_iff])] at h₂ + p.IsValid s ↔ p ≤ s.rawEndPos ∧ (s.bytes.extract p.byteIdx s.utf8ByteSize).IsValidUTF8 := by + refine ⟨fun h => ⟨h.le_rawEndPos, h.isValidUTF8_extract_utf8ByteSize⟩, fun ⟨h₁, h₂⟩ => ?_⟩ + rw [← byteIdx_rawEndPos, isValidUTF8_extract_iff _ _ h₁ (by simp [le_iff])] at h₂ obtain (rfl|h₂) := h₂ · simp · exact h₂.1 @@ -1025,7 +1051,7 @@ theorem offset_startValidPos {s : String} : s.startValidPos.offset = 0 := (rfl) /-- The past-the-end position of `s`, as an `s.ValidPos`. -/ @[inline, expose] def endValidPos (s : String) : s.ValidPos where - offset := s.endPos + offset := s.rawEndPos isValid := by simp instance {s : String} : LE s.ValidPos where @@ -1049,14 +1075,14 @@ instance {s : String} (l r : s.ValidPos) : Decidable (l < r) := theorem ValidPos.isValidUTF8_extract {s : String} (pos₁ pos₂ : s.ValidPos) : (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_endPos).2 (Or.inr ⟨pos₁.isValid, pos₂.isValid⟩) + · 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 omega - · have := Pos.Raw.le_iff.1 pos₂.isValid.le_endPos - rwa [size_bytes, ← byteIdx_endPos] + · have := Pos.Raw.le_iff.1 pos₂.isValid.le_rawEndPos + rwa [size_bytes, ← byteIdx_rawEndPos] /-- A region or slice of some underlying string. @@ -1175,8 +1201,8 @@ At runtime, this function is implemented by efficient, constant-time code. @[inline, expose] def Slice.getUTF8Byte (s : Slice) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 := s.str.getUTF8Byte (p.offsetBy s.startInclusive.offset) (by - have := s.endExclusive.isValid.le_endPos - simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.le_iff, byteIdx_endPos, + have := s.endExclusive.isValid.le_rawEndPos + simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.le_iff, byteIdx_rawEndPos, Pos.Raw.byteIdx_offsetBy] at * omega) @@ -1208,10 +1234,10 @@ theorem Slice.bytes_copy {s : Slice} : theorem Slice.utf8ByteSize_copy {s : Slice} : s.copy.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx:= by simp [← size_bytes, bytes_copy] - rw [Nat.min_eq_left (by simpa [Pos.Raw.le_iff] using s.endExclusive.isValid.le_endPos)] + rw [Nat.min_eq_left (by simpa [Pos.Raw.le_iff] using s.endExclusive.isValid.le_rawEndPos)] @[simp] -theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.rawEndPos := by +theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by simp [Pos.Raw.ext_iff, utf8ByteSize_eq] theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : @@ -1232,7 +1258,7 @@ theorem Pos.Raw.isValid_copy_iff {s : Slice} {p : Pos.Raw} : refine ⟨fun ⟨h₁, h₂⟩ => ⟨?_, ?_⟩, fun ⟨h₁, h₂⟩ => ⟨?_, ?_⟩⟩ · simpa using h₁ · have := s.startInclusive_le_endExclusive - simp_all only [Slice.endPos_copy, le_iff, Slice.byteIdx_rawEndPos, Slice.utf8ByteSize_eq, + simp_all only [Slice.rawEndPos_copy, le_iff, Slice.byteIdx_rawEndPos, Slice.utf8ByteSize_eq, ValidPos.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₂ @@ -1241,7 +1267,7 @@ theorem Pos.Raw.isValid_copy_iff {s : Slice} {p : Pos.Raw} : exact s.startInclusive.isValid · exact h₂ · simp [le_iff] - · have := s.endExclusive.isValid.le_endPos + · have := s.endExclusive.isValid.le_rawEndPos simp_all [le_iff] omega · simpa using h₁ @@ -1251,7 +1277,7 @@ theorem Pos.Raw.isValid_copy_iff {s : Slice} {p : Pos.Raw} : rw [← byteIdx_offsetBy, Pos.Raw.isValidUTF8_extract_iff] · exact Or.inr ⟨s.startInclusive.isValid, h₂⟩ · simp [le_iff] - · have := s.endExclusive.isValid.le_endPos + · have := s.endExclusive.isValid.le_rawEndPos simp_all [le_iff] omega @@ -1286,13 +1312,13 @@ theorem Slice.offset_startInclusive_add_self {s : Slice} : simp_all [String.Pos.Raw.ext_iff, ValidPos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq] @[simp] -theorem Pos.Raw.offsetBy_endPos_left {p : Pos.Raw} {s : String} : - s.endPos.offsetBy p = p + s := by +theorem Pos.Raw.offsetBy_rawEndPos_left {p : Pos.Raw} {s : String} : + s.rawEndPos.offsetBy p = p + s := by simp [Pos.Raw.ext_iff] @[simp] -theorem Pos.Raw.offsetBy_endPos_right {p : Pos.Raw} {s : String} : - p.offsetBy s.endPos = s + p := by +theorem Pos.Raw.offsetBy_rawEndPos_right {p : Pos.Raw} {s : String} : + p.offsetBy s.rawEndPos = s + p := by simp [Pos.Raw.ext_iff] @[simp] @@ -1365,7 +1391,7 @@ instance {s : Slice} {p : Pos.Raw} : Decidable (p.IsValidForSlice s) := theorem Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar?_copy {s : Slice} {p : Pos.Raw} : p.IsValidForSlice s ↔ p = s.rawEndPos ∨ (s.copy.bytes.utf8DecodeChar? p.byteIdx).isSome := by - rw [← isValid_copy_iff, isValid_iff_isSome_utf8DecodeChar?, Slice.endPos_copy] + rw [← isValid_copy_iff, isValid_iff_isSome_utf8DecodeChar?, Slice.rawEndPos_copy] theorem Slice.bytes_str_eq {s : Slice} : s.str.bytes = s.str.bytes.extract 0 s.startInclusive.offset.byteIdx ++ @@ -1373,7 +1399,7 @@ theorem Slice.bytes_str_eq {s : Slice} : rw [bytes_copy, ← ByteArray.extract_eq_extract_append_extract, ← ByteArray.extract_eq_extract_append_extract, ByteArray.extract_zero_size] · simp - · simpa [Pos.Raw.le_iff] using s.endExclusive.isValid.le_endPos + · simpa [Pos.Raw.le_iff] using s.endExclusive.isValid.le_rawEndPos · simp · simpa [Pos.Raw.le_iff] using s.startInclusive_le_endExclusive @@ -1391,7 +1417,7 @@ theorem Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar? {s : Slice} {p : Pos. simp only [ByteArray.size_append, ByteArray.size_extract, Nat.sub_zero, Nat.le_refl, Nat.min_eq_left] have h' : s.startInclusive.offset.byteIdx ≤ s.str.bytes.size := by - simpa [le_iff] using s.startInclusive.isValid.le_endPos + simpa [le_iff] using s.startInclusive.isValid.le_rawEndPos rw [Nat.min_eq_left h', ByteArray.extract_append_size_add' (by simp [size_bytes ▸ h']), ByteArray.extract_append, Nat.add_sub_cancel_left] rw [ByteArray.extract_eq_extract_append_extract s.copy.bytes.size] @@ -1612,7 +1638,7 @@ theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidP theorem str_toSlice {s : String} : s.toSlice.str = s := rfl @[simp] -theorem offset_endValidPos {s : String} : s.endValidPos.offset = s.endPos := (rfl) +theorem offset_endValidPos {s : String} : s.endValidPos.offset = s.rawEndPos := (rfl) @[simp] theorem copy_toSlice {s : String} : s.toSlice.copy = s := by @@ -1651,8 +1677,8 @@ def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.ValidPos where theorem Slice.Pos.ofset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl) @[simp] -theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.endPos := by - rw [← Slice.endPos_copy, copy_toSlice] +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 := @@ -1732,12 +1758,16 @@ theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := theorem Pos.Raw.eq_zero_iff {p : Pos.Raw} : p = 0 ↔ p.byteIdx = 0 := Pos.Raw.ext_iff -theorem endPos_eq_zero_iff {b : String} : b.endPos = 0 ↔ b = "" := by +theorem rawEndPos_eq_zero_iff {b : String} : b.rawEndPos = 0 ↔ b = "" := by simp +@[deprecated rawEndPos_eq_zero_iff (since := "2025-10-20")] +theorem endPos_eq_zero_iff {b : String} : b.rawEndPos = 0 ↔ b = "" := + rawEndPos_eq_zero_iff + @[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.endPos)] + simp [← utf8ByteSize_eq_zero_iff, ValidPos.ext_iff, Eq.comm (b := b.rawEndPos)] @[simp] theorem data_eq_nil_iff {b : String} : b.data = [] ↔ b = "" := by @@ -1753,7 +1783,7 @@ theorem _root_.List.length_asString {l : List Char} : l.asString.length = l.leng 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) - rw [eq_comm, endPos_eq_zero_iff] + rw [eq_comm, rawEndPos_eq_zero_iff] exact fun h => (hb h).elim theorem head_data {b : String} {h} : @@ -1985,7 +2015,7 @@ def Slice.Pos.next {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos wher offset := pos.offset.increaseBy ((pos.byte h).utf8ByteSize pos.isUTF8FirstByte_byte) isValidForSlice := by obtain ⟨t₁, t₂, ht, ht'⟩ := copy_eq_append_get h - replace ht' : pos.offset = t₁.endPos := Eq.symm (String.Pos.Raw.ext ht') + replace ht' : pos.offset = t₁.rawEndPos := Eq.symm (String.Pos.Raw.ext ht') rw [utf8ByteSize_byte, ← Pos.Raw.isValid_copy_iff, ht, ht'] refine Pos.Raw.IsValid.append_right ?_ t₂ rw [Pos.Raw.increaseBy_charUtf8Size] @@ -2414,8 +2444,8 @@ theorem ValidPos.byteIdx_offset_next {s : String} (p : s.ValidPos) (h : p ≠ s. theorem ValidPos.byteIdx_lt_utf8ByteSize {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) : p.offset.byteIdx < s.utf8ByteSize := by - have := byteIdx_endPos ▸ Pos.Raw.le_iff.1 p.isValid.le_endPos - simp only [ne_eq, ValidPos.ext_iff, offset_endValidPos, Pos.Raw.ext_iff, byteIdx_endPos] at h + 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 omega @[simp] @@ -2636,7 +2666,7 @@ abbrev utf8PrevAux : List Char → Pos.Raw → Pos.Raw → Pos.Raw := /-- Returns the position in a string before a specified position, `p`. If `p = ⟨0⟩`, returns `0`. If `p` -is greater than `endPos`, returns the position one byte before `p`. Otherwise, if `p` occurs in the +is greater than `rawEndPos`, returns the position one byte before `p`. Otherwise, if `p` occurs in the middle of a multi-byte character, returns the beginning position of that character. For example, `"L∃∀N".prev ⟨3⟩` is `⟨1⟩`, since byte 3 occurs in the middle of the multi-byte @@ -2647,8 +2677,8 @@ variants like `String.ValidPos.prev?`, combined with `String.pos` or another mea a `String.ValidPos`. Examples: -* `"abc".get ("abc".endPos |> "abc".prev) = 'c'` -* `"L∃∀N".get ("L∃∀N".endPos |> "L∃∀N".prev |> "L∃∀N".prev |> "L∃∀N".prev) = '∃'` +* `"abc".get ("abc".rawEndPos |> "abc".prev) = 'c'` +* `"L∃∀N".get ("L∃∀N".rawEndPos |> "L∃∀N".prev |> "L∃∀N".prev |> "L∃∀N".prev) = '∃'` -/ @[extern "lean_string_utf8_prev", expose] def Pos.Raw.prev : (@& String) → (@& Pos.Raw) → Pos.Raw @@ -2682,9 +2712,12 @@ Examples: * `"".back = (default : Char)` -/ @[inline, expose] def back (s : String) : Char := - (s.endPos.prev s).get s + (s.rawEndPos.prev s).get s -theorem back_eq_get_prev_endPos {s : String} : s.back = (s.endPos.prev s).get s := rfl +theorem back_eq_get_prev_rawEndPos {s : String} : s.back = (s.rawEndPos.prev s).get s := rfl + +@[deprecated back_eq_get_prev_rawEndPos (since := "2025-10-20")] +theorem back_eq_get_prev_endPos {s : String} : s.back = (s.rawEndPos.prev s).get s := rfl /-- Returns `true` if a specified byte position is greater than or equal to the position which points to @@ -2818,7 +2851,7 @@ termination_by stopPos.1 - pos.1 /-- Returns the position of the first occurrence of a character, `c`, in a string `s`. If `s` does not -contain `c`, returns `s.endPos`. +contain `c`, returns `s.rawEndPos`. Examples: * `"abcba".posOf 'a' = ⟨0⟩` @@ -2826,7 +2859,7 @@ Examples: * `"L∃∀N".posOf '∀' = ⟨4⟩` -/ @[inline] def posOf (s : String) (c : Char) : Pos.Raw := - posOfAux s c s.endPos 0 + posOfAux s c s.rawEndPos 0 @[export lean_string_posof] def Internal.posOfImpl (s : String) (c : Char) : Pos.Raw := @@ -2851,7 +2884,7 @@ Examples: * `"L∃∀N".revPosOf '∀' = some ⟨4⟩` -/ @[inline] def revPosOf (s : String) (c : Char) : Option Pos.Raw := - revPosOfAux s c s.endPos + revPosOfAux s c s.rawEndPos def findAux (s : String) (p : Char → Bool) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw := if h : pos < stopPos then @@ -2873,7 +2906,7 @@ Examples: * `"".find (· == 'X') = ⟨0⟩` -/ @[inline] def find (s : String) (p : Char → Bool) : Pos.Raw := - findAux s p s.endPos 0 + findAux s p s.rawEndPos 0 def revFindAux (s : String) (p : Char → Bool) (pos : Pos.Raw) : Option Pos.Raw := if h : pos = 0 then none @@ -2894,7 +2927,7 @@ Examples: * `"".revFind (· == 'X') = none` -/ @[inline] def revFind (s : String) (p : Char → Bool) : Option Pos.Raw := - revFindAux s p s.endPos + revFindAux s p s.rawEndPos /-- Returns either `p₁` or `p₂`, whichever has the least byte index. @@ -2920,7 +2953,7 @@ Examples: -/ @[expose] def firstDiffPos (a b : String) : Pos.Raw := - let stopPos := a.endPos.min b.endPos + let stopPos := a.rawEndPos.min b.rawEndPos let rec loop (i : Pos.Raw) : Pos.Raw := if h : i < stopPos then if i.get a != i.get b then i @@ -2977,7 +3010,7 @@ def extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String splitAux s p i' i' (b.extract s i :: r) else splitAux s p b (i.next s) r -termination_by s.endPos.1 - i.1 +termination_by s.rawEndPos.1 - i.1 /-- Splits a string at each character for which `p` returns `true`. @@ -3021,7 +3054,7 @@ def splitOnAux (s sep : String) (b : Pos.Raw) (i : Pos.Raw) (j : Pos.Raw) (r : L splitOnAux s sep b i j r else splitOnAux s sep b ((i.unoffsetBy j).next s) 0 r -termination_by (s.endPos.1 - (j.byteDistance i), sep.endPos.1 - j.1) +termination_by (s.rawEndPos.1 - (j.byteDistance i), sep.rawEndPos.1 - j.1) decreasing_by focus rename_i h _ _ @@ -3092,7 +3125,7 @@ Examples: * `" ".isEmpty = false` -/ @[inline] def isEmpty (s : String) : Bool := - s.endPos == 0 + s.rawEndPos == 0 @[export lean_string_isempty] def Internal.isEmptyImpl (s : String) : Bool := @@ -3138,8 +3171,8 @@ String iterators pair a string with a valid byte index. This allows efficient ch processing of strings while avoiding the need to manually ensure that byte indices are used with the correct strings. -An iterator is *valid* if the position `i` is *valid* for the string `s`, meaning `0 ≤ i ≤ s.endPos` -and `i` lies on a UTF8 byte boundary. If `i = s.endPos`, the iterator is at the end of the string. +An iterator is *valid* if the position `i` is *valid* for the string `s`, meaning `0 ≤ i ≤ s.rawEndPos` +and `i` lies on a UTF8 byte boundary. If `i = s.rawEndPos`, the iterator is at the end of the string. Most operations on iterators return unspecified values if the iterator is not valid. The functions in the `String.Iterator` API rule out the creation of invalid iterators, with two exceptions: @@ -3185,7 +3218,7 @@ def toString := Iterator.s The number of UTF-8 bytes remaining in the iterator. -/ @[inline] def remainingBytes : Iterator → Nat - | ⟨s, i⟩ => s.endPos.byteIdx - i.byteIdx + | ⟨s, i⟩ => s.rawEndPos.byteIdx - i.byteIdx @[inline, inherit_doc Iterator.i] def pos := Iterator.i @@ -3221,13 +3254,13 @@ The position is not changed if the iterator is at the beginning of the string. Checks whether the iterator is past its string's last character. -/ @[inline] def atEnd : Iterator → Bool - | ⟨s, i⟩ => i.byteIdx ≥ s.endPos.byteIdx + | ⟨s, i⟩ => i.byteIdx ≥ s.rawEndPos.byteIdx /-- Checks whether the iterator is at or before the string's last character. -/ @[inline] def hasNext : Iterator → Bool - | ⟨s, i⟩ => i.byteIdx < s.endPos.byteIdx + | ⟨s, i⟩ => i.byteIdx < s.rawEndPos.byteIdx /-- Checks whether the iterator is after the beginning of the string. @@ -3243,7 +3276,7 @@ function is faster that `String.Iterator.curr` due to avoiding a run-time bounds -/ @[inline] def curr' (it : Iterator) (h : it.hasNext) : Char := match it with - | ⟨s, i⟩ => i.get' s (by simpa only [hasNext, endPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h) + | ⟨s, i⟩ => i.get' s (by simpa only [hasNext, rawEndPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h) /-- Moves the iterator's position forward by one character, unconditionally. @@ -3253,7 +3286,7 @@ This function is faster that `String.Iterator.next` due to avoiding a run-time b -/ @[inline] def next' (it : Iterator) (h : it.hasNext) : Iterator := match it with - | ⟨s, i⟩ => ⟨s, i.next' s (by simpa only [hasNext, endPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h)⟩ + | ⟨s, i⟩ => ⟨s, i.next' s (by simpa only [hasNext, rawEndPos, decide_eq_true_eq, Pos.Raw.atEnd, ge_iff_le, Nat.not_le] using h)⟩ /-- Replaces the current character in the string. @@ -3269,7 +3302,7 @@ in-place and not copied. Moves the iterator's position to the end of the string, just past the last character. -/ @[inline] def toEnd : Iterator → Iterator - | ⟨s, _⟩ => ⟨s, s.endPos⟩ + | ⟨s, _⟩ => ⟨s, s.rawEndPos⟩ /-- Extracts the substring between the positions of two iterators. The first iterator's position is the @@ -3297,7 +3330,7 @@ def forward : Iterator → Nat → Iterator The remaining characters in an iterator, as a string. -/ @[inline] def remainingToString : Iterator → String - | ⟨s, i⟩ => i.extract s s.endPos + | ⟨s, i⟩ => i.extract s s.rawEndPos @[inherit_doc forward] def nextn : Iterator → Nat → Iterator @@ -3321,7 +3354,7 @@ def offsetOfPosAux (s : String) (pos : Pos.Raw) (i : Pos.Raw) (offset : Nat) : N else have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (Pos.Raw.lt_next s _) offsetOfPosAux s pos (i.next s) (offset+1) -termination_by s.endPos.1 - i.1 +termination_by s.rawEndPos.1 - i.1 /-- Returns the character index that corresponds to the provided position (i.e. UTF-8 byte index) in a @@ -3363,7 +3396,7 @@ Examples: * `"coffee tea water".foldl (·.push ·) "" = "coffee tea water"` -/ @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α := - foldlAux f s s.endPos 0 init + foldlAux f s s.rawEndPos 0 init @[export lean_string_foldl] def Internal.foldlImpl (f : String → Char → String) (init : String) (s : String) : String := @@ -3389,7 +3422,7 @@ Examples: * `"coffee tea water".foldr (fun c s => c.push s) "" = "retaw dna aet eeffoc"` -/ @[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α := - foldrAux f init s s.endPos 0 + foldrAux f init s s.rawEndPos 0 @[specialize] def anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) : Bool := if h : i < stopPos then @@ -3412,7 +3445,7 @@ Examples: * `"".any (fun _ => false) = false` -/ @[inline] def any (s : String) (p : Char → Bool) : Bool := - anyAux s s.endPos p 0 + anyAux s s.rawEndPos p 0 @[export lean_string_any] def Internal.anyImpl (s : String) (p : Char → Bool) := @@ -3453,9 +3486,9 @@ theorem Pos.Raw.utf8SetAux_of_gt (c' : Char) : ∀ (cs : List Char) {i p : Pos.R exact Nat.lt_of_lt_of_le h (Nat.le_add_right ..) theorem set_next_add (s : String) (i : Pos.Raw) (c : Char) (b₁ b₂) - (h : (i.next s).1 + b₁ = s.endPos.1 + b₂) : - (i.next (i.set s c)).1 + b₁ = (i.set s c).endPos.1 + b₂ := by - simp [Pos.Raw.next, Pos.Raw.get, Pos.Raw.set, endPos, ← utf8ByteSize'_eq, utf8ByteSize'] at h ⊢ + (h : (i.next s).1 + b₁ = s.rawEndPos.1 + b₂) : + (i.next (i.set s c)).1 + b₁ = (i.set s c).rawEndPos.1 + b₂ := by + simp [Pos.Raw.next, Pos.Raw.get, Pos.Raw.set, rawEndPos, ← utf8ByteSize'_eq, utf8ByteSize'] at h ⊢ rw [Nat.add_comm i.1, Nat.add_assoc] at h ⊢ let rec foo : ∀ cs a b₁ b₂, (Pos.Raw.utf8GetAux cs a i).utf8Size + b₁ = utf8ByteSize'.go cs + b₂ → @@ -3473,12 +3506,12 @@ theorem set_next_add (s : String) (i : Pos.Raw) (c : Char) (b₁ b₂) exact foo s.data 0 _ _ h theorem mapAux_lemma (s : String) (i : Pos.Raw) (c : Char) (h : ¬i.atEnd s) : - (i.set s c).endPos.1 - (i.next (i.set s c)).1 < s.endPos.1 - i.1 := by - suffices (i.set s c).endPos.1 - (i.next (i.set s c)).1 = s.endPos.1 - (i.next s).1 by + (i.set s c).rawEndPos.1 - (i.next (i.set s c)).1 < s.rawEndPos.1 - i.1 := by + suffices (i.set s c).rawEndPos.1 - (i.next (i.set s c)).1 = s.rawEndPos.1 - (i.next s).1 by rw [this] apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (Pos.Raw.lt_next ..) - have := set_next_add s i c (s.endPos.byteIdx - (i.next s).byteIdx) 0 - have := set_next_add s i c 0 ((i.next s).byteIdx - s.endPos.byteIdx) + have := set_next_add s i c (s.rawEndPos.byteIdx - (i.next s).byteIdx) 0 + have := set_next_add s i c 0 ((i.next s).byteIdx - s.rawEndPos.byteIdx) omega @[specialize] def mapAux (f : Char → Char) (i : Pos.Raw) (s : String) : String := @@ -3488,7 +3521,7 @@ theorem mapAux_lemma (s : String) (i : Pos.Raw) (c : Char) (h : ¬i.atEnd s) : have := mapAux_lemma s i c h let s := i.set s c mapAux f (i.next s) s -termination_by s.endPos.1 - i.1 +termination_by s.rawEndPos.1 - i.1 /-- Applies the function `f` to every character in a string, returning a string that contains the @@ -3558,7 +3591,7 @@ This is a legacy function. The recommended alternative is to construct slices re strings to be compared and use the `BEq` instance of `String.Slice`. -/ def Pos.Raw.substrEq (s1 : String) (pos1 : String.Pos.Raw) (s2 : String) (pos2 : String.Pos.Raw) (sz : Nat) : Bool := - pos1.byteIdx + sz ≤ s1.endPos.byteIdx && pos2.byteIdx + sz ≤ s2.endPos.byteIdx && loop pos1 pos2 { byteIdx := pos1.byteIdx + sz } + pos1.byteIdx + sz ≤ s1.rawEndPos.byteIdx && pos2.byteIdx + sz ≤ s2.rawEndPos.byteIdx && loop pos1 pos2 { byteIdx := pos1.byteIdx + sz } where loop (off1 off2 stop1 : Pos.Raw) := if _h : off1.byteIdx < stop1.byteIdx then @@ -3586,7 +3619,7 @@ Examples: * `"".isPrefixOf "red green blue" = true` -/ def isPrefixOf (p : String) (s : String) : Bool := - Pos.Raw.substrEq p 0 s 0 p.endPos.byteIdx + Pos.Raw.substrEq p 0 s 0 p.rawEndPos.byteIdx @[export lean_string_isprefixof] def Internal.isPrefixOfImpl (p : String) (s : String) : Bool := @@ -3601,21 +3634,21 @@ Examples: * `"red green blue".replace "e" "E" = "rEd grEEn bluE"` -/ def replace (s pattern replacement : String) : String := - if h : pattern.endPos.1 = 0 then s + if h : pattern.rawEndPos.1 = 0 then s else have hPatt := Nat.zero_lt_of_ne_zero h let rec loop (acc : String) (accStop pos : String.Pos.Raw) := - if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then - acc ++ accStop.extract s s.endPos + if h : pos.byteIdx + pattern.rawEndPos.byteIdx > s.rawEndPos.byteIdx then + acc ++ accStop.extract s s.rawEndPos else have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h) - if Pos.Raw.substrEq s pos pattern 0 pattern.endPos.byteIdx then + if Pos.Raw.substrEq s pos pattern 0 pattern.rawEndPos.byteIdx then have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _) loop (acc ++ accStop.extract s pos ++ replacement) (pos + pattern) (pos + pattern) else have := Nat.sub_lt_sub_left this (Pos.Raw.lt_next s pos) loop acc accStop (pos.next s) - termination_by s.endPos.1 - pos.1 + termination_by s.rawEndPos.1 - pos.1 loop "" 0 0 /-- @@ -4037,7 +4070,7 @@ and represents the same substring according to `Substring.toString`. (Note, the substring may still be inverted, i.e. beginning greater than end.) -/ def repair : Substring → Substring - | ⟨s, b, e⟩ => ⟨s, if b.isValid s then b else s.endPos, if e.isValid s then e else s.endPos⟩ + | ⟨s, b, e⟩ => ⟨s, if b.isValid s then b else s.rawEndPos, if e.isValid s then e else s.rawEndPos⟩ /-- Checks whether two substrings represent equal strings. Usually accessed via the `==` operator. @@ -4338,7 +4371,7 @@ Examples: * `let s := "ba "; s.get (s.nextWhile Char.isWhitespace 0) = 'b'` -/ @[inline] def Pos.Raw.nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw := - Substring.takeWhileAux s s.endPos p i + Substring.takeWhileAux s s.rawEndPos p i @[deprecated Pos.Raw.nextWhile (since := "2025-10-10")] abbrev nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw := diff --git a/src/Init/Meta/Defs.lean b/src/Init/Meta/Defs.lean index 380cf36275..cbd6d3b6a7 100644 --- a/src/Init/Meta/Defs.lean +++ b/src/Init/Meta/Defs.lean @@ -1550,7 +1550,7 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String := match stx.raw[1] with - | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.endPos ⟨2⟩) + | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.rawEndPos ⟨2⟩) | _ => "" end TSyntax diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 951ab37a10..7f6d4a760f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3441,7 +3441,7 @@ Character positions (counting the Unicode code points rather than bytes) are rep `Nat`s. Indexing a `String` by a `String.Pos.Raw` takes constant time, while character positions need to be translated internally to byte positions, which takes linear time. -A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p` lies on a UTF-8 +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` @@ -3501,10 +3501,10 @@ def String.utf8ByteSize (s : @& String) : Nat := /-- A UTF-8 byte position that points at the end of a string, just after the last character. -* `"abc".endPos = ⟨3⟩` -* `"L∃∀N".endPos = ⟨8⟩` +* `"abc".rawEndPos = ⟨3⟩` +* `"L∃∀N".rawEndPos = ⟨8⟩` -/ -@[inline] def String.endPos (s : String) : String.Pos.Raw where +@[inline] def String.rawEndPos (s : String) : String.Pos.Raw where byteIdx := utf8ByteSize s /-- @@ -3513,7 +3513,7 @@ Converts a `String` into a `Substring` that denotes the entire string. @[inline] def String.toSubstring (s : String) : Substring where str := s startPos := {} - stopPos := s.endPos + stopPos := s.rawEndPos /-- Converts a `String` into a `Substring` that denotes the entire string. diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 57f9b8b096..4f0cd16b95 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -153,7 +153,7 @@ directory. -/ def fileName (p : FilePath) : Option String := let lastPart := match posOfLastSep p with - | some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.endPos + | some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.rawEndPos | none => p.toString if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart @@ -192,7 +192,7 @@ def extension (p : FilePath) : Option String := p.fileName.bind fun fname => match fname.revPosOf '.' with | some 0 => none - | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.endPos + | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.rawEndPos | none => none /-- diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 83f7e155b4..b2b6f9d8ca 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -111,10 +111,10 @@ instance : FromJson CompletionIdentifier where | .str s => let c := s.front if c == 'c' then - let declName := String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName + let declName := String.Pos.Raw.extract s ⟨1⟩ s.rawEndPos |>.toName .ok <| .const declName else if c == 'f' then - let id := ⟨String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName⟩ + let id := ⟨String.Pos.Raw.extract s ⟨1⟩ s.rawEndPos |>.toName⟩ .ok <| .fvar id else .error "Expected string with prefix `c` or `f` in `FromJson` instance of `CompletionIdentifier`." diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean index abad55af60..8e90af5338 100644 --- a/src/Lean/DocString/Add.lean +++ b/src/Lean/DocString/Add.lean @@ -66,8 +66,8 @@ def parseVersoDocString -- Skip trailing `-/` let endPos := String.Pos.Raw.prev text.source <| endPos.prev text.source - let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos - have endPos_valid : endPos ≤ text.source.endPos := by + let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos + have endPos_valid : endPos ≤ text.source.rawEndPos := by unfold endPos split <;> simp [*] diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean index 9d8e47c35e..d783166c07 100644 --- a/src/Lean/DocString/Extension.lean +++ b/src/Lean/DocString/Extension.lean @@ -210,11 +210,11 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String := match stx.raw[1] with | Syntax.atom _ val => - return String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩) + return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩) | Syntax.node _ `Lean.Parser.Command.versoCommentBody _ => match stx.raw[1][0] with | Syntax.atom _ val => - return String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩) + return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩) | _ => throwErrorAt stx "unexpected doc string{indentD stx}" | _ => diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean index 8c2430899e..8f3086f82b 100644 --- a/src/Lean/DocString/Links.lean +++ b/src/Lean/DocString/Links.lean @@ -152,7 +152,7 @@ where Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`. -/ lookingAt (goal : String) (iter : String.Iterator) : Bool := - String.Pos.Raw.substrEq iter.s iter.i goal 0 goal.endPos.byteIdx + String.Pos.Raw.substrEq iter.s iter.i goal 0 goal.rawEndPos.byteIdx /-- Rewrites Lean reference manual links in `docstring` to point at the reference manual. diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 4561fdd816..c05a9deb0e 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -22,7 +22,7 @@ namespace Lean.Elab.Command match stx[1] with | Syntax.atom _ val => if getVersoModuleDocs (← getEnv) |>.isEmpty then - let doc := String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩) + let doc := String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩) modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩ else throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present." diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index f82738c3a9..5b442fdfb1 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -159,7 +159,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m ( match optDocComment.getOptional? with | none => return none | some s => match s[1] with - | .atom _ val => return some (String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩)) + | .atom _ val => return some (String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩)) | _ => throwErrorAt s "unexpected doc string{indentD s[1]}" section Methods diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean index 30bf373ccb..fba7da5239 100644 --- a/src/Lean/Elab/DocString.lean +++ b/src/Lean/Elab/DocString.lean @@ -1205,7 +1205,7 @@ private def mkSuggestion | pure m!"" let text ← getFileMap let pre := String.Pos.Raw.extract text.source 0 b - let post := String.Pos.Raw.extract text.source e text.source.endPos + let post := String.Pos.Raw.extract text.source e text.source.rawEndPos let edits := newStrings.map fun (s, _, _) => let lines := text.source.splitToList (· == '\n') |>.toArray let s' := pre ++ s ++ post diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean index 0a297587f4..28d2de69c5 100644 --- a/src/Lean/Elab/DocString/Builtin.lean +++ b/src/Lean/Elab/DocString/Builtin.lean @@ -647,7 +647,7 @@ def lean (name : Option Ident := none) (error warning «show» : flag false) (co -- TODO fallback for non-original syntax let pos := code.raw.getPos? true |>.get! let endPos := code.raw.getTailPos? true |>.get! - let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos + let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos let ictx := mkInputContext text.source (← getFileName) (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*]) diff --git a/src/Lean/Elab/DocString/Builtin/Parsing.lean b/src/Lean/Elab/DocString/Builtin/Parsing.lean index 797ab8a6cb..65e47eea77 100644 --- a/src/Lean/Elab/DocString/Builtin/Parsing.lean +++ b/src/Lean/Elab/DocString/Builtin/Parsing.lean @@ -25,7 +25,7 @@ def parseStrLit (p : ParserFn) (s : StrLit) : m Syntax := do let text ← getFileMap let env ← getEnv let ⟨pos, endPos⟩ ← strLitRange s - let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos + let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos let ictx := mkInputContext text.source (← getFileName) (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*]) @@ -101,7 +101,7 @@ def parseStrLit' (p : ParserFn) (s : StrLit) : m (Syntax × Bool) := do let text ← getFileMap let env ← getEnv let endPos := s.raw.getTailPos? true |>.get! - let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos + let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos let ictx := mkInputContext text.source (← getFileName) (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*]) diff --git a/src/Lean/Elab/StructInstHint.lean b/src/Lean/Elab/StructInstHint.lean index bc98c8211c..d6fc605659 100644 --- a/src/Lean/Elab/StructInstHint.lean +++ b/src/Lean/Elab/StructInstHint.lean @@ -148,7 +148,7 @@ where Counterpart of `String.findLineStart`. -/ findLineEnd (s : String) (p : String.Pos.Raw) : String.Pos.Raw := - s.findAux (· == '\n') s.endPos p + s.findAux (· == '\n') s.rawEndPos p /-- Is the structure instance notation `stx` described by `view` using single-line styling? diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index bb1028af85..36e2a1e85a 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -249,7 +249,7 @@ where (s.front != '\'' || "''".isPrefixOf s) && s.front != '\"' && !(isIdBeginEscape s.front) && - !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (String.Pos.Raw.get s ⟨1⟩) || isIdBeginEscape (String.Pos.Raw.get s ⟨1⟩))) && + !(s.front == '`' && (s.rawEndPos == ⟨1⟩ || isIdFirst (String.Pos.Raw.get s ⟨1⟩) || isIdBeginEscape (String.Pos.Raw.get s ⟨1⟩))) && !s.front.isDigit && !(s.any Char.isWhitespace) diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index e756d5af0b..17fd3ec3f6 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -302,7 +302,7 @@ where guard (octsEndPos.byteIdx == level) guard (octsEndPos.get line == ' ') let titleStartPos := octsEndPos.next line - let title := Substring.mk line titleStartPos line.endPos |>.toString + let title := Substring.mk line titleStartPos line.rawEndPos |>.toString let titleMatches : Bool := match title? with | some expectedTitle => title == expectedTitle | none => true diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 1381cf1cbc..08f9b688fc 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -380,7 +380,7 @@ def diagnosticsOfHeaderError (msg : String) : ProcessingM Snapshot.Diagnostics : let msgLog := MessageLog.empty.add { fileName := "" pos := ⟨1, 0⟩ - endPos := (← read).fileMap.toPosition (← read).fileMap.source.endPos + endPos := (← read).fileMap.toPosition (← read).fileMap.source.rawEndPos data := msg } Snapshot.Diagnostics.ofMessageLog msgLog diff --git a/src/Lean/Meta/Hint.lean b/src/Lean/Meta/Hint.lean index d163155469..f08fedfb59 100644 --- a/src/Lean/Meta/Hint.lean +++ b/src/Lean/Meta/Hint.lean @@ -398,7 +398,7 @@ where else have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (String.Pos.Raw.lt_next s _) if (i.get s).isWhitespace then - let skipped := (Substring.mk s i s.endPos).takeWhile (·.isWhitespace) + let skipped := (Substring.mk s i s.rawEndPos).takeWhile (·.isWhitespace) let i' := skipped.stopPos splitWordsAux s i' i' (r.push (String.Pos.Raw.extract s b i)) (ws.push (String.Pos.Raw.extract s i i')) else diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean index 545c614a6e..07d657fc96 100644 --- a/src/Lean/Meta/Tactic/Grind/Intro.lean +++ b/src/Lean/Meta/Tactic/Grind/Intro.lean @@ -55,9 +55,9 @@ It ensures base name is a simple `Name` and does not have a `_` suffix private def mkBaseName (name : Name) (type : Expr) : MetaM Name := do if let .str _ s := name then let pos := s.find (· == '_') - unless pos < s.endPos do + unless pos < s.rawEndPos do return Name.mkSimple s - let suffix := String.Pos.Raw.extract s (pos+'_') s.endPos + let suffix := String.Pos.Raw.extract s (pos+'_') s.rawEndPos unless suffix.isNat do return Name.mkSimple s let s := String.Pos.Raw.extract s ⟨0⟩ pos diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 207d5490fa..5c140e6729 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1040,7 +1040,7 @@ private def tokenFnAux : ParserFn := fun c s => else let tk := c.tokens.matchPrefix c.inputString i c.endPos.byteIdx <| by have := c.endPos_valid - rw [String.endPos] at this + rw [String.rawEndPos] at this omega identFnAux i tk .anonymous (includeWhitespace := true) c s diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index c18bfb549d..fa33446692 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -451,8 +451,8 @@ set_option linter.unusedVariables.funArgs false in -- Note: `crlfToLf` preserves logical line and column numbers for each character. def mkInputContext (input : String) (fileName : String) (normalizeLineEndings := true) - (endPos := input.endPos) - (endPos_valid : endPos ≤ input.endPos := by simp) : + (endPos := input.rawEndPos) + (endPos_valid : endPos ≤ input.rawEndPos := by simp) : InputContext := let text := FileMap.ofString input let next := if normalizeLineEndings then @@ -464,7 +464,7 @@ def mkInputContext (input : String) (fileName : String) (text, endPos) let text := next.1 let endPos' := next.2 - if h : endPos' ≤ text.source.endPos then + if h : endPos' ≤ text.source.rawEndPos then .mk text.source fileName (fileMap := text) (endPos := endPos') (endPos_valid := h) else .mk text.source fileName (fileMap := text) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index b794cd5eaf..5c3d8e1b70 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -27,7 +27,7 @@ def versoCommentBodyFn : ParserFn := fun c s => let iniSz := s.stackSize let commentEndPos := s.pos let endPos := c.prev (c.prev commentEndPos) - let endPos := if endPos ≤ c.inputString.endPos then endPos else c.inputString.endPos + let endPos := if endPos ≤ c.inputString.rawEndPos then endPos else c.inputString.rawEndPos let c' := c.setEndPos endPos (by unfold endPos; split <;> simp [*]) let s := Doc.Parser.document {} c' (s.setPos startPos) let s := diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean index 3bd907bc9d..196a7af80a 100644 --- a/src/Lean/Parser/Types.lean +++ b/src/Lean/Parser/Types.lean @@ -50,18 +50,18 @@ structure InputContext where inputString : String fileName : String fileMap : FileMap - endPos : String.Pos.Raw := inputString.endPos - endPos_valid : endPos ≤ inputString.endPos := by simp + endPos : String.Pos.Raw := inputString.rawEndPos + endPos_valid : endPos ≤ inputString.rawEndPos := by simp instance : Inhabited InputContext where - default := ⟨"", default, default, "".endPos, String.Pos.Raw.mk_le_mk.mpr (Nat.le_refl _)⟩ + default := ⟨"", default, default, "".rawEndPos, String.Pos.Raw.mk_le_mk.mpr (Nat.le_refl _)⟩ namespace InputContext def mk (input fileName : String) - (endPos : String.Pos.Raw := input.endPos) - (endPos_valid : endPos ≤ input.endPos := by simp) + (endPos : String.Pos.Raw := input.rawEndPos) + (endPos_valid : endPos ≤ input.rawEndPos := by simp) (fileMap : FileMap := FileMap.ofString input) : InputContext where inputString := input @@ -91,7 +91,7 @@ theorem not_atEnd_inputString {c : InputContext} {p : String.Pos.Raw} : intro h let {inputString, endPos := ⟨e⟩, endPos_valid, ..} := c cases p - simp only [String.endPos, String.Pos.Raw.mk_le_mk] at endPos_valid + simp only [String.rawEndPos, String.Pos.Raw.mk_le_mk] at endPos_valid simp_all [String.Pos.Raw.atEnd, InputContext.atEnd, String.Pos.Raw.mk_le_mk] exact Nat.lt_of_lt_of_le h endPos_valid @@ -198,7 +198,7 @@ instance : Coe ParserContext InputContext := ⟨(·.toInputContext)⟩ Modifies the ending position of a parser context. -/ def ParserContext.setEndPos (c : ParserContext) - (endPos : String.Pos.Raw) (endPos_valid : endPos ≤ c.inputString.endPos) : + (endPos : String.Pos.Raw) (endPos_valid : endPos ≤ c.inputString.rawEndPos) : ParserContext := { c with endPos, endPos_valid } @@ -263,7 +263,7 @@ structure ParserCache where parserCache : Std.HashMap ParserCacheKey ParserCacheEntry def initCacheForInput (input : String) : ParserCache where - tokenCache := { startPos := input.endPos + ' ' /- make sure it is not a valid position -/ } + tokenCache := { startPos := input.rawEndPos + ' ' /- make sure it is not a valid position -/ } parserCache := {} /-- A syntax array with an inaccessible prefix, used for sound caching. -/ diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 0eff8e9ad2..301fe53fa9 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -389,7 +389,7 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit -- Check if we would parse more than `tk` as a single token let tk' := tk.trimLeft let t ← parseToken $ tk' ++ st.leadWord - if t.pos ≤ tk'.endPos then + if t.pos ≤ tk'.rawEndPos then -- stopped within `tk` => use it as is pure false else @@ -612,7 +612,7 @@ def continuation : String := " [...]" instance : Std.Format.MonadPrettyFormat M where pushOutput s := do let lineEnd := s.find (· == '\n') - if lineEnd < s.endPos then + if lineEnd < s.rawEndPos then let s := (String.Pos.Raw.extract s 0 lineEnd).trimRight ++ continuation modify fun st => { st with line := st.line.append s } throw () diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 885aee3e2f..a67d767449 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -402,7 +402,7 @@ def setupImports let progressDiagnostic := { range := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩ -- make progress visible anywhere in the file - fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.endPos⟩ + fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.rawEndPos⟩ severity? := DiagnosticSeverity.information message := stderrLine } @@ -630,7 +630,7 @@ section NotificationHandling use the \"Restart File\" command in your editor." let diagnostic := { range := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩ - fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.endPos⟩ + fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.rawEndPos⟩ severity? := DiagnosticSeverity.information message := importOutOfDataMessage } @@ -1076,7 +1076,7 @@ where writeErrorDiag (doc : DocumentMeta) (err : Error) : IO Unit := do o.writeLspMessage <| mkPublishDiagnosticsNotification doc #[{ range := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩, - fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.endPos⟩ + fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.rawEndPos⟩ severity? := DiagnosticSeverity.error message := err.toString }] diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 920adcbb71..6ffe818149 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -300,7 +300,7 @@ def NamespaceEntry.finish (text : FileMap) (syms : Array DocumentSymbol) (endStx -- we can assume that commands always have at least one position (see `parseCommand`) let range := match endStx with | some endStx => (mkNullNode #[stx, endStx]).getRange?.get! - | none => { stx.getRange?.get! with stop := text.source.endPos } + | none => { stx.getRange?.get! with stop := text.source.rawEndPos } let name := name.foldr (fun x y => y ++ x) Name.anonymous prevSiblings.push <| DocumentSymbol.mk { -- anonymous sections are represented by `«»` name components @@ -386,7 +386,7 @@ partial def handleFoldingRange (_ : FoldingRangeParams) addRanges (text : FileMap) sections | [] => do if let (_, start)::rest := sections then - addRange text FoldingRangeKind.region start text.source.endPos + addRange text FoldingRangeKind.region start text.source.rawEndPos addRanges text rest [] | stx::stxs => do RequestM.checkCancelled diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index 32af70eee6..f68bdcf867 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -200,12 +200,12 @@ private def hightlightStringMatches? (query text : String) (matchPositions : Arr let mut r : Array (TaggedText α) := #[] let mut p : String.Pos.Raw := ⟨0⟩ for i in 0...matchPositions.size do - if p >= text.endPos then + if p >= text.rawEndPos then break let i := mapIdx i let globalMatchPos := matchPositions[i]! let matchPos := globalMatchPos.unoffsetBy offset - if matchPos >= text.endPos then + if matchPos >= text.rawEndPos then break if let some nonMatch := nonMatch? p matchPos then r := r.push nonMatch @@ -215,7 +215,7 @@ private def hightlightStringMatches? (query text : String) (matchPositions : Arr r := r.push <| .tag highlight (.text «match») p := matchEndPos anyMatch := true - if let some nonMatch := nonMatch? p text.endPos then + if let some nonMatch := nonMatch? p text.rawEndPos then r := r.push nonMatch if ! anyMatch then return none diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 4802b0965a..4764406c88 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -453,7 +453,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String | return gs let trailSize := i.stx.getTrailingSize -- show info at EOF even if strictly outside token + trail - let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx + let atEOF := tailPos.byteIdx + trailSize == text.source.rawEndPos.byteIdx -- include at least one trailing character (see also `priority` below) if pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + max 1 trailSize || atEOF) then -- overwrite bottom-up results according to "innermost" heuristics documented above diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 895a8025ab..923bae4874 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -27,7 +27,7 @@ def Lean.FileMap.rangeContainsHoverPos (text : Lean.FileMap) (r : Lean.Syntax.Ra -- which always excludes a `hoverPos` at the very end of the file. -- For the purposes of the language server, we generally assume that ranges that extend to -- the end of the file also include a `hoverPos` at the very end of the file. - let isRangeAtEOF := r.stop == text.source.endPos + let isRangeAtEOF := r.stop == text.source.rawEndPos r.contains hoverPos (includeStop := includeStop || isRangeAtEOF) def Lean.FileMap.rangeOverlapsRequestedRange @@ -37,7 +37,7 @@ def Lean.FileMap.rangeOverlapsRequestedRange (includeDocumentRangeStop := false) (includeRequestedRangeStop := false) : Bool := - let isDocumentRangeAtEOF := documentRange.stop == text.source.endPos + let isDocumentRangeAtEOF := documentRange.stop == text.source.rawEndPos documentRange.overlaps requestedRange (includeFirstStop := includeDocumentRangeStop || isDocumentRangeAtEOF) (includeSecondStop := includeRequestedRangeStop) @@ -49,7 +49,7 @@ def Lean.FileMap.rangeIncludesRequestedRange (includeDocumentRangeStop := false) (includeRequestedRangeStop := false) : Bool := - let isDocumentRangeAtEOF := documentRange.stop == text.source.endPos + let isDocumentRangeAtEOF := documentRange.stop == text.source.rawEndPos documentRange.includes requestedRange (includeSuperStop := includeDocumentRangeStop || isDocumentRangeAtEOF) (includeSubStop := includeRequestedRangeStop) diff --git a/src/Lean/Server/Test/Runner.lean b/src/Lean/Server/Test/Runner.lean index 8b8b4eaa38..46abc5be75 100644 --- a/src/Lean/Server/Test/Runner.lean +++ b/src/Lean/Server/Test/Runner.lean @@ -640,9 +640,9 @@ def processDirective (ws directive : String) (directiveTargetLineNo : Nat) : Run let colon := directive.posOf ':' let method := String.Pos.Raw.extract directive 0 colon |>.trim -- TODO: correctly compute in presence of Unicode - let directiveTargetColumn := ws.endPos + "--" + let directiveTargetColumn := ws.rawEndPos + "--" let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn.byteIdx } - let params := if colon < directive.endPos then String.Pos.Raw.extract directive (colon + ':') directive.endPos |>.trim else "{}" + let params := if colon < directive.rawEndPos then String.Pos.Raw.extract directive (colon + ':') directive.rawEndPos |>.trim else "{}" modify fun s => { s with pos, method, params } match method with -- `delete: "foo"` deletes the given string's number of characters at the given position. diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 7eb05aa3f6..74fdcc15e6 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -110,7 +110,7 @@ def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMa let start := text.lspPosToUtf8Pos r.start let «end» := text.lspPosToUtf8Pos r.«end» let pre := String.Pos.Raw.extract text.source 0 start - let post := String.Pos.Raw.extract text.source «end» text.source.endPos + let post := String.Pos.Raw.extract text.source «end» text.source.rawEndPos -- `pre` and `post` already have normalized line endings, so only `newText` needs its endings normalized. -- Note: this assumes that editing never separates a `\r\n`. -- If `pre` ends with `\r` and `newText` begins with `\n`, the result is potentially inaccurate. @@ -171,7 +171,7 @@ def mkFileProgressNotification (m : DocumentMeta) (processing : Array LeanFilePr def mkFileProgressAtPosNotification (m : DocumentMeta) (pos : String.Pos.Raw) (kind : LeanFileProgressKind := LeanFileProgressKind.processing) : JsonRpc.Notification Lsp.LeanFileProgressParams := - mkFileProgressNotification m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.endPos⟩, kind := kind }] + mkFileProgressNotification m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.rawEndPos⟩, kind := kind }] /-- Constructs a `$/lean/fileProgress` notification marking processing as done. -/ def mkFileProgressDoneNotification (m : DocumentMeta) : JsonRpc.Notification Lsp.LeanFileProgressParams := diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index 49b9a0e31e..a7081adf28 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -261,7 +261,7 @@ def shellMain IO.eprintln s!"unknown language '{langId}'\n"; return 1 -- Remove up to `\n` - pure <| String.Pos.Raw.extract contents endLinePos contents.endPos + pure <| String.Pos.Raw.extract contents endLinePos contents.rawEndPos else pure contents let setup? ← setupFileName?.mapM ModuleSetup.load diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 98abcd8e75..741ac8f329 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -192,10 +192,10 @@ def getWantsHelp : CliStateM Bool := def setConfigOpt (kvPair : String) : CliM PUnit := let pos := kvPair.posOf '=' let (key, val) := - if pos = kvPair.endPos then + if pos = kvPair.rawEndPos then (kvPair.toName, "") else - (String.Pos.Raw.extract kvPair 0 pos |>.toName, String.Pos.Raw.extract kvPair (pos.next kvPair) kvPair.endPos) + (String.Pos.Raw.extract kvPair 0 pos |>.toName, String.Pos.Raw.extract kvPair (pos.next kvPair) kvPair.rawEndPos) modifyThe LakeOptions fun opts => {opts with configOpts := opts.configOpts.insert key val} diff --git a/src/lake/Lake/Config/Artifact.lean b/src/lake/Lake/Config/Artifact.lean index fa6eed6b88..330706d4d0 100644 --- a/src/lake/Lake/Config/Artifact.lean +++ b/src/lake/Lake/Config/Artifact.lean @@ -57,7 +57,7 @@ public def ofFilePath? (path : FilePath) : Except String ArtifactDescr := do else let some hash := Hash.ofString? <| String.Pos.Raw.extract s 0 pos | throw "expected artifact file name to be a content hash" - let ext := String.Pos.Raw.extract s (pos.next' s h) s.endPos + let ext := String.Pos.Raw.extract s (pos.next' s h) s.rawEndPos return {hash, ext} public protected def fromJson? (data : Json) : Except String ArtifactDescr := do diff --git a/src/lake/Lake/Config/Cache.lean b/src/lake/Lake/Config/Cache.lean index 8e1109ef4a..7b57113866 100644 --- a/src/lake/Lake/Config/Cache.lean +++ b/src/lake/Lake/Config/Cache.lean @@ -61,13 +61,13 @@ public partial def parse (inputName : String) (contents : String) : LoggerIO Cac return cache else loop (i+1) cache stopPos (lfPos.next' contents h) - let lfPos := contents.posOfAux '\n' contents.endPos 0 + let lfPos := contents.posOfAux '\n' contents.rawEndPos 0 let line := String.Pos.Raw.extract contents 0 lfPos checkSchemaVersion inputName line.trim if h : lfPos.atEnd contents then return {} else - loop 2 {} contents.endPos (lfPos.next' contents h) + loop 2 {} contents.rawEndPos (lfPos.next' contents h) @[inline] private partial def loadCore (h : IO.FS.Handle) (fileName : String) diff --git a/src/lake/Lake/Toml/Elab/Value.lean b/src/lake/Lake/Toml/Elab/Value.lean index 607054a6e3..9814d0f548 100644 --- a/src/lake/Lake/Toml/Elab/Value.lean +++ b/src/lake/Lake/Toml/Elab/Value.lean @@ -154,10 +154,10 @@ partial def elabBasicStringCore (lit : String) (i : String.Pos.Raw := 0) (out := | 'r' => elabBasicStringCore lit next (out.push '\r') | '\"' => elabBasicStringCore lit next (out.push '"') | '\\' => elabBasicStringCore lit next (out.push '\\') - | 'u' => elabUnicodeEscape (Substring.mk lit next lit.endPos |>.take 4) - | 'U' => elabUnicodeEscape (Substring.mk lit next lit.endPos |>.take 8) + | 'u' => elabUnicodeEscape (Substring.mk lit next lit.rawEndPos |>.take 4) + | 'U' => elabUnicodeEscape (Substring.mk lit next lit.rawEndPos |>.take 8) | _ => - let i := Substring.mk lit i lit.endPos |>.trimLeft |>.startPos + let i := Substring.mk lit i lit.rawEndPos |>.trimLeft |>.startPos elabBasicStringCore lit i out else elabBasicStringCore lit i (out.push curr) diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean index 340611fb8e..23791f54f9 100644 --- a/src/lake/Lake/Util/Cli.lean +++ b/src/lake/Lake/Util/Cli.lean @@ -97,19 +97,19 @@ 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.posOf ' ' - if pos = opt.endPos then + if pos = opt.rawEndPos then handle opt else do - consArg <| (pos.next opt).extract opt opt.endPos + consArg <| (pos.next opt).extract opt opt.rawEndPos handle <| String.Pos.Raw.extract opt 0 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.posOf '=' - if pos = opt.endPos then + if pos = opt.rawEndPos then handle opt else do - consArg <| (pos.next opt).extract opt opt.endPos + consArg <| (pos.next opt).extract opt opt.rawEndPos handle <| String.Pos.Raw.extract opt 0 pos /-- Process a long option of the form `--long`, `--long=arg`, `"--long arg"`. -/ diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean index 1c5450cbff..a86e831cbe 100644 --- a/src/lake/Lake/Util/FilePath.lean +++ b/src/lake/Lake/Util/FilePath.lean @@ -65,7 +65,7 @@ public def modOfFilePath (path : FilePath) : Name := let path := path.stripSuffix FilePath.pathSeparator.toString FilePath.components path |>.foldl .str .anonymous where - removeExts (s : String) (i := s.endPos) (e := s.endPos) := + removeExts (s : String) (i := s.rawEndPos) (e := s.rawEndPos) := if h : i = 0 then String.Pos.Raw.extract s 0 e else diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index 1061c3328a..f278d4f054 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -95,7 +95,7 @@ public def StdVer.parse (ver : String) : Except String StdVer := do SemVerCore.parse ver else let core ← SemVerCore.parse <| String.Pos.Raw.extract ver 0 sepPos - let specialDescr := String.Pos.Raw.extract ver (sepPos.next' ver h) ver.endPos + let specialDescr := String.Pos.Raw.extract ver (sepPos.next' ver h) ver.rawEndPos if specialDescr.isEmpty then throw "invalid version: '-' suffix cannot be empty" return {toSemVerCore := core, specialDescr} @@ -140,9 +140,9 @@ public instance : Coe LeanVer ToolchainVer := ⟨ToolchainVer.release⟩ public def ofString (ver : String) : ToolchainVer := Id.run do let colonPos := ver.posOf ':' let (origin, tag) := - if h : colonPos < ver.endPos then - let pos := colonPos.next' ver (by simp_all [String.endPos, String.Pos.Raw.atEnd, String.Pos.Raw.lt_iff]) - (String.Pos.Raw.extract ver 0 colonPos, String.Pos.Raw.extract ver pos ver.endPos) + if h : colonPos < ver.rawEndPos then + let pos := colonPos.next' ver (by simp_all [String.rawEndPos, String.Pos.Raw.atEnd, String.Pos.Raw.lt_iff]) + (String.Pos.Raw.extract ver 0 colonPos, String.Pos.Raw.extract ver pos ver.rawEndPos) else ("", ver) let noOrigin := origin.isEmpty diff --git a/tests/bench/workspaceSymbolsNewRanges.lean b/tests/bench/workspaceSymbolsNewRanges.lean index 7ea832bec4..1e56fa2db7 100644 --- a/tests/bench/workspaceSymbolsNewRanges.lean +++ b/tests/bench/workspaceSymbolsNewRanges.lean @@ -37,7 +37,7 @@ private def containsInOrderLower (a b : String) : Bool := Id.run do return true let mut aIt := a.mkIterator -- TODO: the following code is assuming all characters are ASCII - for i in *...b.endPos.byteIdx do + for i in *...b.rawEndPos.byteIdx do if aIt.curr.toLower == (b.get ⟨i⟩).toLower then aIt := aIt.next if !aIt.hasNext then diff --git a/tests/compiler/str.lean b/tests/compiler/str.lean index a4318e9c30..b44cedc88c 100644 --- a/tests/compiler/str.lean +++ b/tests/compiler/str.lean @@ -8,7 +8,7 @@ def showChars : Nat → String → String.Pos.Raw → IO Unit def main : IO UInt32 := let s₁ := "hello α_world_β"; let b : String.Pos.Raw := 0; -let e := s₁.endPos; +let e := s₁.rawEndPos; IO.println (s₁.extract b e) *> IO.println (s₁.extract (b+ " ") e) *> IO.println (s₁.extract (b+ " ") (e.unoffsetBy ⟨1⟩)) *> diff --git a/tests/lean/docparse/run.lean b/tests/lean/docparse/run.lean index 8dd7cc974e..40c948769a 100644 --- a/tests/lean/docparse/run.lean +++ b/tests/lean/docparse/run.lean @@ -38,8 +38,8 @@ def test (p : ParserFn) (input : String) : IO String := do let stk := ppStack <| s'.stxStack.extract 0 s'.stxStack.size let remaining : String := - if s'.pos ≥ input.endPos then "All input consumed." - else s!"Remaining:\n{repr (input.extract s'.pos input.endPos)}" + if s'.pos ≥ input.rawEndPos then "All input consumed." + else s!"Remaining:\n{repr (input.extract s'.pos input.rawEndPos)}" if s'.allErrors.isEmpty then return s!"Success! Final stack:\n{stk.pretty 50}\n{remaining}" @@ -47,14 +47,14 @@ def test (p : ParserFn) (input : String) : IO String := do return s!"Failure @{p} ({ictx.fileMap.toPosition p}): {toString err}\n\ Final stack:\n\ {stk.pretty 50}\n\ - Remaining: {repr $ input.extract p input.endPos}" + Remaining: {repr $ input.extract p input.rawEndPos}" else let mut errors := "" for (p, _, e) in s'.allErrors.qsort errLt do errors := errors ++ s!" @{p} ({ictx.fileMap.toPosition p}): {toString e}\n" ++ - s!" {repr <| input.extract p input.endPos}\n" + 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 := diff --git a/tests/lean/run/frontend_meeting_2022_09_13.lean b/tests/lean/run/frontend_meeting_2022_09_13.lean index 76e8f09589..c30a9462b2 100644 --- a/tests/lean/run/frontend_meeting_2022_09_13.lean +++ b/tests/lean/run/frontend_meeting_2022_09_13.lean @@ -60,7 +60,7 @@ end open Lean Elab Command in @[command_elab commandComment] def elabCommandComment : CommandElab := fun stx => do let .atom _ val := stx[1] | return () - let str := val.extract 0 (val.endPos.unoffsetBy ⟨3⟩) + let str := val.extract 0 (val.rawEndPos.unoffsetBy ⟨3⟩) IO.println s!"str := {repr str}" //- My command comment hello world -// diff --git a/tests/lean/run/parseEnd.lean b/tests/lean/run/parseEnd.lean index 946770d828..55d0df922b 100644 --- a/tests/lean/run/parseEnd.lean +++ b/tests/lean/run/parseEnd.lean @@ -17,7 +17,7 @@ elab d:docComment "test" : command => do let endPos := input.prev <| input.prev endPos - if h : endPos ≤ input.endPos then + if h : endPos ≤ input.rawEndPos then let ictx := mkInputContext input (← getFileName) (endPos := endPos) (endPos_valid := h) let env ← getEnv let s := { mkParserState input with pos } diff --git a/tests/lean/run/string.lean b/tests/lean/run/string.lean index 94193f0e7f..dce330f9fc 100644 --- a/tests/lean/run/string.lean +++ b/tests/lean/run/string.lean @@ -80,8 +80,8 @@ Examples from documentation (added in https://github.com/leanprover/lean4/pull/4 #test lean.get (0 |> lean.next |> lean.next) = '∀' -- prev -#test abc.get (abc.endPos |> abc.prev) = 'c' -#test lean.get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃' +#test abc.get (abc.rawEndPos |> abc.prev) = 'c' +#test lean.get (lean.rawEndPos |> lean.prev |> lean.prev |> lean.prev) = '∃' -- front #test "abc".front = 'a' @@ -143,7 +143,7 @@ Behavior of `String.prev` (`lean_string_utf8_prev`) in special cases (see issue #test "L∃∀N".prev ⟨5⟩ = ⟨4⟩ #test "L∃∀N".prev ⟨6⟩ = ⟨4⟩ #test "L∃∀N".prev ⟨7⟩ = ⟨4⟩ -#test "L∃∀N".prev ⟨8⟩ = ⟨7⟩ -- endPos +#test "L∃∀N".prev ⟨8⟩ = ⟨7⟩ -- rawEndPos #test "L∃∀N".prev ⟨9⟩ = ⟨8⟩ #test "L∃∀N".prev ⟨100⟩ = ⟨99⟩ -- small value out of bounds #test "L∃∀N".prev ⟨2 ^ 128⟩ = ⟨2 ^ 128 - 1⟩ -- large non-scalar