From fa5d08b7de0214eb65874be9be28c5e3901cd5d3 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 18 Nov 2025 17:13:48 +0100 Subject: [PATCH] refactor: use `String.Slice` in `String.take` and variants (#11180) This PR redefines `String.take` and variants to operate on `String.Slice`. While previously functions returning a substring of the input sometimes returned `String` and sometimes returned `Substring.Raw`, they now uniformly return `String.Slice`. This is a BREAKING change, because many functions now have a different return type. So for example, if `s` is a string and `f` is a function accepting a string, `f (s.drop 1)` will no longer compile because `s.drop 1` is a `String.Slice`. To fix this, insert a call to `copy` to restore the old behavior: `f (s.drop 1).copy`. Of course, in many cases, there will be more efficient options. For example, don't write `f <| s.drop 1 |>.copy |>.dropEnd 1 |>.copy`, write `f <| s.drop 1 |>.dropEnd 1 |>.copy` instead. Also, instead of `(s.drop 1).copy = "Hello"`, write `s.drop 1 == "Hello".toSlice` instead. --- src/Init/Data/String/Basic.lean | 17 - src/Init/Data/String/Slice.lean | 85 ++-- src/Init/Data/String/TakeDrop.lean | 437 +++++++++++------- src/Init/Data/ToString/Name.lean | 1 + src/Init/System/IO.lean | 8 +- src/Init/System/Uri.lean | 6 +- src/Lean/Compiler/Old.lean | 1 + src/Lean/Data/Lsp/Communication.lean | 8 +- src/Lean/DocString/Markdown.lean | 8 +- src/Lean/DocString/Parser.lean | 4 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Deriving/FromToJson.lean | 2 +- src/Lean/Elab/DocString/Builtin.lean | 8 +- src/Lean/Elab/DocString/Builtin/Keywords.lean | 18 +- src/Lean/Elab/GuardMsgs.lean | 4 +- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Elab/Syntax.lean | 4 +- src/Lean/Elab/Tactic/Do/VCGen.lean | 2 +- src/Lean/Elab/Tactic/Doc.lean | 4 +- src/Lean/Elab/Tactic/Try.lean | 2 +- src/Lean/ErrorExplanation.lean | 8 +- src/Lean/Linter/List.lean | 2 +- src/Lean/LoadDynlib.lean | 2 +- src/Lean/Parser/Basic.lean | 10 +- src/Lean/Parser/Tactic/Doc.lean | 2 +- src/Lean/Parser/Term/Doc.lean | 4 +- src/Lean/PrettyPrinter/Formatter.lean | 16 +- .../Server/Completion/ImportCompletion.lean | 2 +- src/Lean/Server/FileWorker/ExampleHover.lean | 6 +- src/Lean/Server/FileWorker/SetupFile.lean | 2 +- src/Lean/Server/Test/Runner.lean | 6 +- src/Lean/Shell.lean | 4 +- src/Lean/Util/Path.lean | 4 +- src/Std/Time/Format/Basic.lean | 4 +- src/Std/Time/Zoned/Database/TZdb.lean | 4 +- src/lake/Lake/Build/Actions.lean | 2 +- src/lake/Lake/Build/ExternLib.lean | 2 +- src/lake/Lake/Build/Key.lean | 8 +- src/lake/Lake/CLI/Build.lean | 4 +- src/lake/Lake/CLI/Init.lean | 4 +- src/lake/Lake/CLI/Translate.lean | 2 +- src/lake/Lake/CLI/Translate/Lean.lean | 2 +- src/lake/Lake/Config/Cache.lean | 4 +- src/lake/Lake/Config/Env.lean | 4 +- src/lake/Lake/Config/InstallPath.lean | 8 +- src/lake/Lake/Config/OutFormat.lean | 4 +- src/lake/Lake/Reservoir.lean | 8 +- src/lake/Lake/Toml/Data/DateTime.lean | 2 +- src/lake/Lake/Toml/Data/Value.lean | 2 +- src/lake/Lake/Toml/Elab/Value.lean | 16 +- src/lake/Lake/Toml/ParserUtil.lean | 2 +- src/lake/Lake/Util/Cli.lean | 7 +- src/lake/Lake/Util/FilePath.lean | 4 +- src/lake/Lake/Util/Git.lean | 2 +- src/lake/Lake/Util/Log.lean | 6 +- src/lake/Lake/Util/Proc.lean | 8 +- src/lake/Lake/Util/Url.lean | 2 +- src/lake/Lake/Util/Version.lean | 6 +- tests/compiler/trie.lean | 2 +- tests/lean/Uri.lean | 2 +- tests/lean/docparse/run.lean | 2 +- tests/lean/run/errorExplanationElab.lean | 2 +- tests/lean/run/levenshtein.lean | 4 +- tests/lean/run/string_gaps.lean | 2 +- tests/lean/string_imp2.lean | 2 +- 65 files changed, 482 insertions(+), 342 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 1f4754dcae..7130e9e7bd 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -2785,23 +2785,6 @@ where def substrEq (s1 : String) (pos1 : String.Pos.Raw) (s2 : String) (pos2 : String.Pos.Raw) (sz : Nat) : Bool := Pos.Raw.substrEq s1 pos1 s2 pos2 sz -/-- -Checks whether the first string (`p`) is a prefix of the second (`s`). - -`String.startsWith` is a version that takes the potential prefix after the string. - -Examples: - * `"red".isPrefixOf "red green blue" = true` - * `"green".isPrefixOf "red green blue" = false` - * `"".isPrefixOf "red green blue" = true` --/ -def isPrefixOf (p : String) (s : String) : Bool := - Pos.Raw.substrEq p 0 s 0 p.rawEndPos.byteIdx - -@[export lean_string_isprefixof] -def Internal.isPrefixOfImpl (p : String) (s : String) : Bool := - String.isPrefixOf p s - /-- Returns the position of the beginning of the line that contains the position `pos`. diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index ff969ad169..898535cf7b 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -10,6 +10,7 @@ public import Init.Data.String.Pattern public import Init.Data.Ord.Basic public import Init.Data.Iterators.Combinators.FilterMap public import Init.Data.String.ToSlice +public import Init.Data.String.Termination set_option doc.verso true @@ -403,19 +404,19 @@ Examples: * {lean}`"red green blue".toSlice.dropWhile (fun (_ : Char) => true) == "".toSlice` -/ @[inline] -partial def dropWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice := - go s +def dropWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice := + go s.startPos where @[specialize pat] - go (s : Slice) : Slice := - if let some nextS := dropPrefix? s pat then - -- TODO: need lawful patterns to show this terminates - if s.startInclusive.offset < nextS.startInclusive.offset then - go nextS + go (curr : s.Pos) : Slice := + if let some nextCurr := ForwardPattern.dropPrefix? (s.replaceStart curr) pat then + if curr < Pos.ofReplaceStart nextCurr then + go (Pos.ofReplaceStart nextCurr) else - s + s.replaceStart curr else - s + s.replaceStart curr + termination_by curr /-- Removes leading whitespace from a slice by moving its start position to the first non-whitespace @@ -463,19 +464,19 @@ Examples: * {lean}`"red green blue".toSlice.takeWhile (fun (_ : Char) => true) == "red green blue".toSlice` -/ @[inline] -partial def takeWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice := +def takeWhile [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice := go s.startPos where @[specialize pat] go (curr : s.Pos) : Slice := if let some nextCurr := ForwardPattern.dropPrefix? (s.replaceStart curr) pat then - if (s.replaceStart curr).startPos < nextCurr then - -- TODO: need lawful patterns to show this terminates + if curr < Pos.ofReplaceStart nextCurr then go (Pos.ofReplaceStart nextCurr) else s.replaceEnd curr else s.replaceEnd curr + termination_by curr /-- Finds the position of the first match of the pattern {name}`pat` in a slice {name}`s`. If there @@ -712,23 +713,23 @@ Examples: * {lean}`"red green blue".toSlice.dropEndWhile (fun (_ : Char) => true) == "".toSlice` -/ @[inline] -partial def dropEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice := - go s +def dropEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice := + go s.endPos where @[specialize pat] - go (s : Slice) : Slice := - if let some nextS := dropSuffix? s pat then - -- TODO: need lawful patterns to show this terminates - if nextS.endExclusive.offset < s.endExclusive.offset then - go nextS + go (curr : s.Pos) : Slice := + if let some nextCurr := BackwardPattern.dropSuffix? (s.replaceEnd curr) pat then + if Pos.ofReplaceEnd nextCurr < curr then + go (Pos.ofReplaceEnd nextCurr) else - s + s.replaceEnd curr else - s + s.replaceEnd curr + termination_by curr.down /-- -Removes trailing whitespace from a slice by moving its start position to the first non-whitespace -character, or to its end position if there is no non-whitespace character. +Removes trailing whitespace from a slice by moving its end position to the last non-whitespace +character, or to its start position if there is no non-whitespace character. “Whitespace” is defined as characters for which {name}`Char.isWhitespace` returns {name}`true`. @@ -771,19 +772,19 @@ Examples: * {lean}`"red green blue".toSlice.takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice` -/ @[inline] -partial def takeEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice := +def takeEndWhile [BackwardPattern ρ] (s : Slice) (pat : ρ) : Slice := go s.endPos where @[specialize pat] go (curr : s.Pos) : Slice := if let some nextCurr := BackwardPattern.dropSuffix? (s.replaceEnd curr) pat then - if nextCurr < (s.replaceEnd curr).endPos then - -- TODO: need lawful patterns to show this terminates + if Pos.ofReplaceEnd nextCurr < curr then go (Pos.ofReplaceEnd nextCurr) else s.replaceStart curr else s.replaceStart curr + termination_by curr.down /-- Finds the position of the first match of the pattern {name}`pat` in a slice {name}`true`, starting @@ -1338,4 +1339,36 @@ Examples: def back (s : Slice) : Char := s.back?.getD default +/-- +Appends the slices in a list of slices, placing the separator {name}`s` between each pair. + +Examples: + * {lean}`", ".toSlice.intercalate ["red".toSlice, "green".toSlice, "blue".toSlice] = "red, green, blue"` + * {lean}`" and ".toSlice.intercalate ["tea".toSlice, "coffee".toSlice] = "tea and coffee"` + * {lean}`" | ".toSlice.intercalate ["M".toSlice, "".toSlice, "N".toSlice] = "M | | N"` +-/ +def intercalate (s : Slice) : List Slice → String + | [] => "" + | a :: as => go a.copy s as +where go (acc : String) (s : Slice) : List Slice → String + | a :: as => go (acc ++ s ++ a) s as + | [] => acc + +@[inherit_doc Slice.copy] +def toString (s : Slice) : String := + s.copy + +instance : ToString String.Slice where + toString := toString + +/-- +Converts a string to the Lean compiler's representation of names. The resulting name is +hierarchical, and the string is split at the dots ({lean}`'.'`). + +{lean}`"a.b".toSlice.toName` is the name {lit}`a.b`, not {lit}`«a.b»`. For the latter, use +`Name.mkSimple`. +-/ +def toName (s : Slice) : Lean.Name := + s.toString.toName + end String.Slice diff --git a/src/Init/Data/String/TakeDrop.lean b/src/Init/Data/String/TakeDrop.lean index 135f0cb3cb..18dffe1844 100644 --- a/src/Init/Data/String/TakeDrop.lean +++ b/src/Init/Data/String/TakeDrop.lean @@ -1,223 +1,320 @@ /- Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura, Mario Carneiro +Author: Leonardo de Moura, Mario Carneiro, Markus Himmel -/ module prelude +public import Init.Data.String.Slice public import Init.Data.String.Substring +set_option doc.verso true + /-! # `String.take` and variants -This file contains the implementations of `String.take` and its variants. Currently, they are -implemented in terms of `Substring`; soon, they will be implemented in terms of `String.Slice` -instead. +This file contains the implementations of `String.take` and its variants. -/ public section namespace String -/-- -Removes the specified number of characters (Unicode code points) from the start of the string. +variable {ρ : Type} -If `n` is greater than `s.length`, returns `""`. +open Slice.Pattern + +/-- +Returns a {name}`String.Slice` obtained by removing the specified number of characters (Unicode code +points) from the start of the string. + +If {name}`n` is greater than {lean}`s.length`, returns an empty slice. + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. Examples: - * `"red green blue".drop 4 = "green blue"` - * `"red green blue".drop 10 = "blue"` - * `"red green blue".drop 50 = ""` + * {lean}`"red green blue".drop 4 == "green blue".toSlice` + * {lean}`"red green blue".drop 10 == "blue".toSlice` + * {lean}`"red green blue".drop 50 == "".toSlice` + * {lean}`"مرحبا بالعالم".drop 3 == "با بالعالم".toSlice` -/ -@[inline] def drop (s : String) (n : Nat) : String := - (s.toRawSubstring.drop n).toString +@[inline] def drop (s : String) (n : Nat) : Slice := + s.toSlice.drop n @[export lean_string_drop] def Internal.dropImpl (s : String) (n : Nat) : String := - String.drop s n + (String.drop s n).copy /-- -Removes the specified number of characters (Unicode code points) from the end of the string. +Returns a {name}`String.Slice` obtained by removing the specified number of characters (Unicode code +points) from the end of the string. -If `n` is greater than `s.length`, returns `""`. +If {name}`n` is greater than {lean}`s.length`, returns an empty slice. + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. Examples: - * `"red green blue".dropRight 5 = "red green"` - * `"red green blue".dropRight 11 = "red"` - * `"red green blue".dropRight 50 = ""` + * {lean}`"red green blue".dropEnd 5 == "red green".toSlice` + * {lean}`"red green blue".dropEnd 11 == "red".toSlice` + * {lean}`"red green blue".dropEnd 50 == "".toSlice` + * {lean}`"مرحبا بالعالم".dropEnd 3 == "مرحبا بالع".toSlice` -/ -@[inline] def dropRight (s : String) (n : Nat) : String := - (s.toRawSubstring.dropRight n).toString +@[inline] def dropEnd (s : String) (n : Nat) : Slice := + s.toSlice.dropEnd n + +@[deprecated String.dropEnd (since := "2025-11-14")] +def dropRight (s : String) (n : Nat) : String := + (s.dropEnd n).copy @[export lean_string_dropright] def Internal.dropRightImpl (s : String) (n : Nat) : String := - String.dropRight s n + (String.dropEnd s n).copy /-- -Creates a new string that contains the first `n` characters (Unicode code points) of `s`. +Returns a {name}`String.Slice` that contains the first {name}`n` characters (Unicode code points) of +{name}`s`. -If `n` is greater than `s.length`, returns `s`. +If {name}`n` is greater than {lean}`s.length`, returns {lean}`s.toSlice`. + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. Examples: -* `"red green blue".take 3 = "red"` -* `"red green blue".take 1 = "r"` -* `"red green blue".take 0 = ""` -* `"red green blue".take 100 = "red green blue"` +* {lean}`"red green blue".take 3 == "red".toSlice` +* {lean}`"red green blue".take 1 == "r".toSlice` +* {lean}`"red green blue".take 0 == "".toSlice` +* {lean}`"red green blue".take 100 == "red green blue".toSlice` +* {lean}`"مرحبا بالعالم".take 5 == "مرحبا".toSlice` -/ -@[inline] def take (s : String) (n : Nat) : String := - (s.toRawSubstring.take n).toString +@[inline] def take (s : String) (n : Nat) : String.Slice := + s.toSlice.take n /-- -Creates a new string that contains the last `n` characters (Unicode code points) of `s`. +Returns a {name}`String.Slice` that contains the last {name}`n` characters (Unicode code points) of +{name}`s`. -If `n` is greater than `s.length`, returns `s`. +If {name}`n` is greater than {lean}`s.length`, returns {lean}`s.toSlice`. + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. Examples: -* `"red green blue".takeRight 4 = "blue"` -* `"red green blue".takeRight 1 = "e"` -* `"red green blue".takeRight 0 = ""` -* `"red green blue".takeRight 100 = "red green blue"` +* {lean}`"red green blue".takeEnd 4 == "blue".toSlice` +* {lean}`"red green blue".takeEnd 1 == "e".toSlice` +* {lean}`"red green blue".takeEnd 0 == "".toSlice` +* {lean}`"red green blue".takeEnd 100 == "red green blue".toSlice` +* {lean}`"مرحبا بالعالم".takeEnd 5 == "لعالم".toSlice` -/ -@[inline] def takeRight (s : String) (n : Nat) : String := - (s.toRawSubstring.takeRight n).toString +@[inline] def takeEnd (s : String) (n : Nat) : String.Slice := + s.toSlice.takeEnd n + +@[deprecated String.takeEnd (since := "2025-11-14")] +def takeRight (s : String) (n : Nat) : String := + (s.takeEnd n).toString /-- -Creates a new string that contains the longest prefix of `s` in which `p` returns `true` for all -characters. +Creates a string slice that contains the longest prefix of {name}`s` in which {name}`pat` matched +(potentially repeatedly). + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: -* `"red green blue".takeWhile (·.isLetter) = "red"` -* `"red green blue".takeWhile (· == 'r') = "r"` -* `"red green blue".takeWhile (· != 'n') = "red gree"` -* `"red green blue".takeWhile (fun _ => true) = "red green blue"` + * {lean}`"red green blue".takeWhile Char.isLower == "red".toSlice` + * {lean}`"red green blue".takeWhile 'r' == "r".toSlice` + * {lean}`"red red green blue".takeWhile "red " == "red red ".toSlice` + * {lean}`"red green blue".takeWhile (fun (_ : Char) => true) == "red green blue".toSlice` -/ -@[inline] def takeWhile (s : String) (p : Char → Bool) : String := - (s.toRawSubstring.takeWhile p).toString +@[inline] def takeWhile [ForwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.takeWhile pat /-- -Creates a new string by removing the longest prefix from `s` in which `p` returns `true` for all -characters. +Creates a string slice by removing the longest prefix from {name}`s` in which {name}`pat` matched +(potentially repeatedly). + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: -* `"red green blue".dropWhile (·.isLetter) = " green blue"` -* `"red green blue".dropWhile (· == 'r') = "ed green blue"` -* `"red green blue".dropWhile (· != 'n') = "n blue"` -* `"red green blue".dropWhile (fun _ => true) = ""` + * {lean}`"red green blue".dropWhile Char.isLower == " green blue".toSlice` + * {lean}`"red green blue".dropWhile 'r' == "ed green blue".toSlice` + * {lean}`"red red green blue".dropWhile "red " == "green blue".toSlice` + * {lean}`"red green blue".dropWhile (fun (_ : Char) => true) == "".toSlice` -/ -@[inline] def dropWhile (s : String) (p : Char → Bool) : String := - (s.toRawSubstring.dropWhile p).toString +@[inline] def dropWhile [ForwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.dropWhile pat /-- -Creates a new string that contains the longest suffix of `s` in which `p` returns `true` for all -characters. +Creates a string slice that contains the longest suffix of {name}`s` in which {name}`pat` matched +(potentially repeatedly). + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: -* `"red green blue".takeRightWhile (·.isLetter) = "blue"` -* `"red green blue".takeRightWhile (· == 'e') = "e"` -* `"red green blue".takeRightWhile (· != 'n') = " blue"` -* `"red green blue".takeRightWhile (fun _ => true) = "red green blue"` + * {lean}`"red green blue".takeEndWhile Char.isLower == "blue".toSlice` + * {lean}`"red green blue".takeEndWhile 'e' == "e".toSlice` + * {lean}`"red green blue".takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice` -/ -@[inline] def takeRightWhile (s : String) (p : Char → Bool) : String := - (s.toRawSubstring.takeRightWhile p).toString +@[inline] def takeEndWhile [BackwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.takeEndWhile pat + +@[deprecated String.takeEndWhile (since := "2025-11-17")] +def takeRightWhile (s : String) (p : Char → Bool) : String := + (s.takeEndWhile p).toString /-- -Creates a new string by removing the longest suffix from `s` in which `p` returns `true` for all -characters. +Creates a new string by removing the longest suffix from {name}`s` in which {name}`pat` matches +(potentially repeatedly). + +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: -* `"red green blue".dropRightWhile (·.isLetter) = "red green "` -* `"red green blue".dropRightWhile (· == 'e') = "red green blu"` -* `"red green blue".dropRightWhile (· != 'n') = "red green"` -* `"red green blue".dropRightWhile (fun _ => true) = ""` + * {lean}`"red green blue".dropEndWhile Char.isLower == "red green ".toSlice` + * {lean}`"red green blue".dropEndWhile 'e' == "red green blu".toSlice` + * {lean}`"red green blue".dropEndWhile (fun (_ : Char) => true) == "".toSlice` -/ -@[inline] def dropRightWhile (s : String) (p : Char → Bool) : String := - (s.toRawSubstring.dropRightWhile p).toString +@[inline] def dropEndWhile [BackwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.dropEndWhile pat + +@[deprecated String.dropEndWhile (since := "2025-11-17")] +def dropRightWhile (s : String) (p : Char → Bool) : String := + (s.dropEndWhile p).toString /-- -Checks whether the first string (`s`) begins with the second (`pre`). +Checks whether the first string ({name}`s`) begins with the pattern ({name}`pat`). -`String.isPrefix` is a version that takes the potential prefix before the string. +{name (scope := "Init.Data.String.TakeDrop")}`String.isPrefixOf` is a version that takes the +potential prefix before the string. Examples: - * `"red green blue".startsWith "red" = true` - * `"red green blue".startsWith "green" = false` - * `"red green blue".startsWith "" = true` - * `"red".startsWith "red" = true` + * {lean}`"red green blue".startsWith "red" = true` + * {lean}`"red green blue".startsWith "green" = false` + * {lean}`"red green blue".startsWith "" = true` + * {lean}`"red green blue".startsWith 'r' = true` + * {lean}`"red green blue".startsWith Char.isLower = true` -/ -@[inline] def startsWith (s pre : String) : Bool := - s.toRawSubstring.take pre.length == pre.toRawSubstring +@[inline] def startsWith [ForwardPattern ρ] (s : String) (pat : ρ) : Bool := + s.toSlice.startsWith pat /-- -Checks whether the first string (`s`) ends with the second (`post`). +Checks whether the second string ({name}`s`) begins with a prefix ({name}`p`). + +This function is generic over all currently supported patterns. + +{name}`String.startsWith` is a version that takes the potential prefix after the string. Examples: - * `"red green blue".endsWith "blue" = true` - * `"red green blue".endsWith "green" = false` - * `"red green blue".endsWith "" = true` - * `"red".endsWith "red" = true` + * {lean}`"red".isPrefixOf "red green blue" = true` + * {lean}`"green".isPrefixOf "red green blue" = false` + * {lean}`"".isPrefixOf "red green blue" = true` -/ -@[inline] def endsWith (s post : String) : Bool := - s.toRawSubstring.takeRight post.length == post.toRawSubstring +@[inline] def isPrefixOf (p : String) (s : String) : Bool := + s.startsWith p + +@[export lean_string_isprefixof] +def Internal.isPrefixOfImpl (p : String) (s : String) : Bool := + String.isPrefixOf p s /-- -Removes trailing whitespace from a string. +Checks whether the string ({name}`s`) ends with the pattern ({name}`pat`). -“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`. +This function is generic over all currently supported patterns. Examples: -* `"abc".trimRight = "abc"` -* `" abc".trimRight = " abc"` -* `"abc \t ".trimRight = "abc"` -* `" abc ".trimRight = " abc"` -* `"abc\ndef\n".trimRight = "abc\ndef"` + * {lean}`"red green blue".endsWith "blue" = true` + * {lean}`"red green blue".endsWith "green" = false` + * {lean}`"red green blue".endsWith "" = true` + * {lean}`"red green blue".endsWith 'e' = true` + * {lean}`"red green blue".endsWith Char.isLower = true` -/ -@[inline] def trimRight (s : String) : String := - s.toRawSubstring.trimRight.toString +@[inline] def endsWith [BackwardPattern ρ] (s : String) (pat : ρ) : Bool := + s.toSlice.endsWith pat /-- -Removes leading whitespace from a string. +Removes trailing whitespace from a string by returning a slice whose end position is the last +non-whitespace character, or the start position if there is no non-whitespace character. -“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`. +“Whitespace” is defined as characters for which {name}`Char.isWhitespace` returns {name}`true`. Examples: -* `"abc".trimLeft = "abc"` -* `" abc".trimLeft = " abc"` -* `"abc \t ".trimLeft = "abc \t "` -* `" abc ".trimLeft = "abc "` -* `"abc\ndef\n".trimLeft = "abc\ndef\n"` + * {lean}`"abc".trimAsciiEnd == "abc".toSlice` + * {lean}`" abc".trimAsciiEnd == " abc".toSlice` + * {lean}`"abc \t ".trimAsciiEnd == "abc".toSlice` + * {lean}`" abc ".trimAsciiEnd == " abc".toSlice` + * {lean}`"abc\ndef\n".trimAsciiEnd == "abc\ndef".toSlice` -/ -@[inline] def trimLeft (s : String) : String := - s.toRawSubstring.trimLeft.toString +@[inline] def trimAsciiEnd (s : String) : String.Slice := + s.toSlice.trimAsciiEnd + +@[deprecated String.trimAsciiEnd (since := "2025-11-17")] +def trimRight (s : String) : String := + s.trimAsciiEnd.copy + +/-- +Removes leading whitespace from a string by returning a slice whose start position is the first +non-whitespace character, or the end position if there is no non-whitespace character. + +“Whitespace” is defined as characters for which {name}`Char.isWhitespace` returns {name}`true`. + +Examples: + * {lean}`"abc".trimAsciiStart == "abc".toSlice` + * {lean}`" abc".trimAsciiStart == "abc".toSlice` + * {lean}`"abc \t ".trimAsciiStart == "abc \t ".toSlice` + * {lean}`" abc ".trimAsciiStart == "abc ".toSlice` + * {lean}`"abc\ndef\n".trimAsciiStart == "abc\ndef\n".toSlice` +-/ +@[inline] def trimAsciiStart (s : String) : String.Slice := + s.toSlice.trimAsciiStart + +@[deprecated String.trimAsciiStart (since := "2025-11-17")] +def trimLeft (s : String) : String := + s.trimAsciiStart.copy /-- Removes leading and trailing whitespace from a string. -“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`. +“Whitespace” is defined as characters for which {name}`Char.isWhitespace` returns {name}`true`. Examples: -* `"abc".trim = "abc"` -* `" abc".trim = "abc"` -* `"abc \t ".trim = "abc"` -* `" abc ".trim = "abc"` -* `"abc\ndef\n".trim = "abc\ndef"` + * {lean}`"abc".trimAscii == "abc".toSlice` + * {lean}`" abc".trimAscii == "abc".toSlice` + * {lean}`"abc \t ".trimAscii == "abc".toSlice` + * {lean}`" abc ".trimAscii == "abc".toSlice` + * {lean}`"abc\ndef\n".trimAscii == "abc\ndef".toSlice` -/ -@[inline] def trim (s : String) : String := - s.toRawSubstring.trim.toString +@[inline] def trimAscii (s : String) : String.Slice := + s.toSlice.trimAscii + +@[deprecated String.trimAscii (since := "2025-11-17")] +def trim (s : String) : String := + s.trimAscii.copy @[export lean_string_trim] def Internal.trimImpl (s : String) : String := - String.trim s + (String.trimAscii s).copy /-- -Repeatedly increments a position in a string, as if by `String.next`, while the predicate `p` -returns `true` for the character at the position. Stops incrementing at the end of the string or -when `p` returns `false` for the current character. +Repeatedly increments a position in a string, as if by {name}`String.Pos.Raw.next`, while the +predicate {name}`p` returns {lean}`true` for the character at the position. Stops incrementing at +the end of the string or when {name}`p` returns {lean}`false` for the current character. Examples: -* `let s := " a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'` -* `let s := "a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'` -* `let s := "ba "; s.get (s.nextWhile Char.isWhitespace 0) = 'b'` +* {lean}`let s := " a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'` +* {lean}`let s := "a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'` +* {lean}`let s := "ba "; (Pos.Raw.nextWhile s Char.isWhitespace 0).get s = 'b'` -/ @[inline] def Pos.Raw.nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw := Substring.Raw.takeWhileAux s s.rawEndPos p i @@ -231,14 +328,14 @@ def Internal.nextWhileImpl (s : String) (p : Char → Bool) (i : String.Pos.Raw) i.nextWhile s p /-- -Repeatedly increments a position in a string, as if by `String.next`, while the predicate `p` -returns `false` for the character at the position. Stops incrementing at the end of the string or -when `p` returns `true` for the current character. +Repeatedly increments a position in a string, as if by {name}`String.Pos.Raw.next`, while the predicate +{name}`p` returns {lean}`false` for the character at the position. Stops incrementing at the end of +the string or when {name}`p` returns {lean}`true` for the current character. Examples: -* `let s := " a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '` -* `let s := " a "; s.get (s.nextUntil Char.isLetter 0) = 'a'` -* `let s := "a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '` +* {lean}`let s := " a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '` +* {lean}`let s := " a "; (Pos.Raw.nextUntil s Char.isAlpha 0).get s = 'a'` +* {lean}`let s := "a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '` -/ @[inline] def Pos.Raw.nextUntil (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw := nextWhile s (fun c => !p c) i @@ -248,67 +345,91 @@ def nextUntil (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos i.nextUntil s p /-- -If `pre` is a prefix of `s`, returns the remainder. Returns `none` otherwise. +If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise. -The string `pre` is a prefix of `s` if there exists a `t : String` such that `s = pre ++ t`. If so, -the result is `some t`. +Use {name (scope := "Init.Data.String.Slice")}`String.dropPrefix` to return the slice +unchanged when {name}`pat` does not match a prefix. -Use `String.stripPrefix` to return the string unchanged when `pre` is not a prefix. +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: - * `"red green blue".dropPrefix? "red " = some "green blue"` - * `"red green blue".dropPrefix? "reed " = none` - * `"red green blue".dropPrefix? "" = some "red green blue"` + * {lean}`"red green blue".dropPrefix? "red " == some "green blue".toSlice` + * {lean}`"red green blue".dropPrefix? "reed " == none` + * {lean}`"red green blue".dropPrefix? 'r' == some "ed green blue".toSlice` + * {lean}`"red green blue".dropPrefix? Char.isLower == some "ed green blue".toSlice` -/ -def dropPrefix? (s : String) (pre : String) : Option Substring.Raw := - s.toRawSubstring.dropPrefix? pre.toRawSubstring +def dropPrefix? [ForwardPattern ρ] (s : String) (pat : ρ) : Option String.Slice := + s.toSlice.dropPrefix? pat /-- -If `suff` is a suffix of `s`, returns the remainder. Returns `none` otherwise. +If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise. -The string `suff` is a suffix of `s` if there exists a `t : String` such that `s = t ++ suff`. If so, -the result is `some t`. +Use {name (scope := "Init.Data.String.TakeDrop")}`String.dropSuffix` to return the slice +unchanged when {name}`pat` does not match a prefix. -Use `String.stripSuffix` to return the string unchanged when `suff` is not a suffix. +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: - * `"red green blue".dropSuffix? " blue" = some "red green"` - * `"red green blue".dropSuffix? " blu " = none` - * `"red green blue".dropSuffix? "" = some "red green blue"` + * {lean}`"red green blue".dropSuffix? " blue" == some "red green".toSlice` + * {lean}`"red green blue".dropSuffix? "bluu " == none` + * {lean}`"red green blue".dropSuffix? 'e' == some "red green blu".toSlice` + * {lean}`"red green blue".dropSuffix? Char.isLower == some "red green blu".toSlice` -/ -def dropSuffix? (s : String) (suff : String) : Option Substring.Raw := - s.toRawSubstring.dropSuffix? suff.toRawSubstring +def dropSuffix? [BackwardPattern ρ] (s : String) (pat : ρ) : Option String.Slice := + s.toSlice.dropSuffix? pat /-- -If `pre` is a prefix of `s`, returns the remainder. Returns `s` unmodified otherwise. +If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified +otherwise. -The string `pre` is a prefix of `s` if there exists a `t : String` such that `s = pre ++ t`. If so, -the result is `t`. Otherwise, it is `s`. +Use {name}`String.dropPrefix?` to return {name}`none` when {name}`pat` does not match a prefix. -Use `String.dropPrefix?` to return `none` when `pre` is not a prefix. +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: - * `"red green blue".stripPrefix "red " = "green blue"` - * `"red green blue".stripPrefix "reed " = "red green blue"` - * `"red green blue".stripPrefix "" = "red green blue"` + * {lean}`"red green blue".dropPrefix "red " == "green blue".toSlice` + * {lean}`"red green blue".dropPrefix "reed " == "red green blue".toSlice` + * {lean}`"red green blue".dropPrefix 'r' == "ed green blue".toSlice` + * {lean}`"red green blue".dropPrefix Char.isLower == "ed green blue".toSlice` -/ -def stripPrefix (s : String) (pre : String) : String := - s.dropPrefix? pre |>.map Substring.Raw.toString |>.getD s +def dropPrefix [ForwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.dropPrefix pat + +@[deprecated String.dropPrefix (since := "2025-11-17")] +def stripPrefix (s pre : String) : String := + (s.dropPrefix pre).toString /-- -If `suff` is a suffix of `s`, returns the remainder. Returns `s` unmodified otherwise. +If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified +otherwise. -The string `suff` is a suffix of `s` if there exists a `t : String` such that `s = t ++ suff`. If so, -the result is `t`. Otherwise, it is `s`. +Use {name}`String.dropSuffix?` to return {name}`none` when {name}`pat` does not match a prefix. -Use `String.dropSuffix?` to return `none` when `suff` is not a suffix. +This is a cheap operation because it does not allocate a new string to hold the result. +To convert the result into a string, use {name}`String.Slice.copy`. + +This function is generic over all currently supported patterns. Examples: - * `"red green blue".stripSuffix " blue" = "red green"` - * `"red green blue".stripSuffix " blu " = "red green blue"` - * `"red green blue".stripSuffix "" = "red green blue"` + * {lean}`"red green blue".dropSuffix " blue" == "red green".toSlice` + * {lean}`"red green blue".dropSuffix "bluu " == "red green blue".toSlice` + * {lean}`"red green blue".dropSuffix 'e' == "red green blu".toSlice` + * {lean}`"red green blue".dropSuffix Char.isLower == "red green blu".toSlice` -/ +def dropSuffix [BackwardPattern ρ] (s : String) (pat : ρ) : String.Slice := + s.toSlice.dropSuffix pat + +@[deprecated String.dropSuffix (since := "2025-11-17")] def stripSuffix (s : String) (suff : String) : String := - s.dropSuffix? suff |>.map Substring.Raw.toString |>.getD s + (s.dropSuffix suff).toString end String diff --git a/src/Init/Data/ToString/Name.lean b/src/Init/Data/ToString/Name.lean index df09cfb61f..1c95c39766 100644 --- a/src/Init/Data/ToString/Name.lean +++ b/src/Init/Data/ToString/Name.lean @@ -7,6 +7,7 @@ module prelude public import Init.Data.String.Substring +import Init.Data.String.TakeDrop /-! Here we give the. implementation of `Name.toString`. There is also a private implementation in diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 8cb5641fca..03945e42db 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -1008,8 +1008,8 @@ partial def Handle.lines (h : Handle) : IO (Array String) := do if line.length == 0 then pure lines else if line.back == '\n' then - let line := line.dropRight 1 - let line := if line.back == '\r' then line.dropRight 1 else line + let line := line.dropEnd 1 |>.copy + let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line read <| lines.push line else pure <| lines.push line @@ -1791,8 +1791,8 @@ partial def lines (s : Stream) : IO (Array String) := do if line.length == 0 then pure lines else if line.back == '\n' then - let line := line.dropRight 1 - let line := if line.back == '\r' then line.dropRight 1 else line + let line := line.dropEnd 1 |>.copy + let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line read <| lines.push line else pure <| lines.push line diff --git a/src/Init/System/Uri.lean b/src/Init/System/Uri.lean index 4d6f79949d..8370ba690a 100644 --- a/src/Init/System/Uri.lean +++ b/src/Init/System/Uri.lean @@ -107,13 +107,13 @@ def fileUriToPath? (uri : String) : Option System.FilePath := Id.run do if !uri.startsWith "file://" then none else - let mut p := (unescapeUri uri).drop "file://".length - p := p.dropWhile (λ c => c != '/') -- drop the hostname. + let mut p := (unescapeUri uri).drop "file://".length |>.copy + p := p.dropWhile (λ c => c != '/') |>.copy -- drop the hostname. -- On Windows, the path "/c:/temp" needs to become "C:/temp" if System.Platform.isWindows && p.length >= 2 && p.front == '/' && (String.Pos.Raw.get p ⟨1⟩).isAlpha && String.Pos.Raw.get p ⟨2⟩ == ':' then -- see also `pathToUri` - p := String.Pos.Raw.modify (p.drop 1) 0 .toUpper + p := String.Pos.Raw.modify (p.drop 1).copy 0 .toUpper some p end Uri diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean index b1a15ba13e..6add97282f 100644 --- a/src/Lean/Compiler/Old.lean +++ b/src/Lean/Compiler/Old.lean @@ -7,6 +7,7 @@ module prelude public import Lean.Environment +import Init.Data.String.TakeDrop public section diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean index 374ad3f53b..6e461e1fc3 100644 --- a/src/Lean/Data/Lsp/Communication.lean +++ b/src/Lean/Data/Lsp/Communication.lean @@ -21,14 +21,14 @@ open Lean.JsonRpc section private def parseHeaderField (s : String) : Option (String × String) := do - guard $ s ≠ "" ∧ s.takeRight 2 = "\r\n" - let xs := (s.dropRight 2).splitOn ": " + guard $ s ≠ "" ∧ s.takeEnd 2 == "\r\n".toSlice + let xs := (s.dropEnd 2).split ": " |>.toList match xs with | [] => none | [_] => none | name :: value :: rest => - let value := ": ".intercalate (value :: rest) - some ⟨name, value⟩ + let value := ": ".toSlice.intercalate (value :: rest) + some ⟨name.copy, value⟩ /-- Returns true when the string is a Lean 3 request. This means that the user is running a Lean 3 language client that diff --git a/src/Lean/DocString/Markdown.lean b/src/Lean/DocString/Markdown.lean index e73fd40760..e8110e71ae 100644 --- a/src/Lean/DocString/Markdown.lean +++ b/src/Lean/DocString/Markdown.lean @@ -187,8 +187,8 @@ where let (pre, post) := go more (s ++ pre, post) else - let s1 := s.takeWhile (·.isWhitespace) - let s2 := s.drop s1.length + let s1 := s.takeWhile Char.isWhitespace |>.copy + let s2 := s.drop s1.length |>.copy (s1, .text s2 ++ .concat more.toArray) | .concat xs :: more => go (xs.toList ++ more) | here :: more => ("", here ++ .concat more.toArray) @@ -202,8 +202,8 @@ where let (pre, post) := go more (pre, post ++ s) else - let s1 := s.takeRightWhile (·.isWhitespace) - let s2 := s.dropRight s1.length + let s1 := s.takeEndWhile Char.isWhitespace |>.copy + let s2 := s.dropEnd s1.length |>.copy (.concat more.toArray.reverse ++ .text s2, s1) | .concat xs :: more => go (xs.reverse.toList ++ more) | here :: more => (.concat more.toArray.reverse ++ here, "") diff --git a/src/Lean/DocString/Parser.lean b/src/Lean/DocString/Parser.lean index 9728ac8fe8..707b510452 100644 --- a/src/Lean/DocString/Parser.lean +++ b/src/Lean/DocString/Parser.lean @@ -683,7 +683,7 @@ mutual let str := s.stxStack.back if let .atom info str := str then if str.startsWith "\" " && str.endsWith " \"" then - let core := str.drop 2 |>.dropRight 2 + let core := str.drop 2 |>.dropEnd 2 |>.copy if core.any (· != ' ') then let str := "\"" ++ core ++ "\"" let info : SourceInfo := @@ -1047,7 +1047,7 @@ mutual | other => s.mkError s!"Internal error - not a column node {other}" deIndent (n : Nat) (str : String) : String := Id.run do - let str := if str != "" && str.back == '\n' then str.dropRight 1 else str + let str := if str != "" && str.back == '\n' then str.dropEnd 1 |>.copy else str let mut out := "" for line in str.splitOn "\n" do out := out ++ line.drop n ++ "\n" diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index ff08a186d2..77bdae158b 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -597,7 +597,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro stx.hasMissing && !showPartialSyntaxErrors.get (← getOptions) }) do -- initialize quotation context using hash of input string let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false) - withInitQuotContext (ss?.map (hash ·.toString.trim)) do + withInitQuotContext (ss?.map (hash ·.toString.trimAscii.copy)) do -- Reset messages and info state, which are both per-command modify fun st => { st with messages := {}, infoState := { enabled := st.infoState.enabled } } try diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 62a72485b4..cb6b4b7899 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -29,7 +29,7 @@ def mkFromJsonHeader (indVal : InductiveVal) : TermElabM Header := do def mkJsonField (n : Name) : CoreM (Bool × Term) := do let .str .anonymous s := n | throwError "invalid json field name {n}" - let s₁ := s.dropRightWhile (· == '?') + let s₁ := s.dropEndWhile (· == '?') |>.copy return (s != s₁, Syntax.mkStrLit s₁) def mkToJsonBodyForStruct (header : Header) (indName : Name) : TermElabM Term := do diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean index ce34226a53..98f4a2a21e 100644 --- a/src/Lean/Elab/DocString/Builtin.lean +++ b/src/Lean/Elab/DocString/Builtin.lean @@ -156,7 +156,7 @@ def name (full : Option Ident := none) (scope : DocScope := .local) let x := s.getString.toName if x.isAnonymous then let h ← - if s.getString != s.getString.trim && !s.getString.trim.isEmpty then + if s.getString.toSlice != s.getString.trimAscii && !s.getString.trimAscii.isEmpty then -- Like Markdown, Verso code elements that start and end with a space will strip the space, -- to allow code with leading or trailing backticks. But our suggestions shouldn't prefer -- that form here. Thus, the suggestion uses the delimiter positions instead of the string @@ -170,7 +170,7 @@ def name (full : Option Ident := none) (scope : DocScope := .local) let ⟨tailPos, _⟩ ← tk2.getRange? pure <| Syntax.mkStrLit (String.Pos.Raw.extract text.source pos tailPos) (info := .synthetic pos tailPos) if let some ref := ref? then - m!"Remove surrounding whitespace:".hint #[s.getString.trim] (ref? := some ref) + m!"Remove surrounding whitespace:".hint #[s.getString.trimAscii.copy] (ref? := some ref) else pure m!"" else pure m!"" throwErrorAt s "Not a valid name.{h}" @@ -870,7 +870,7 @@ where | (output, .error e) => Lean.logError e.toMessageData; pure (output, cmdState) | (output, .ok ((), cmdState)) => pure (output, cmdState) - if output.trim.isEmpty then return cmdState + if output.trimAscii.isEmpty then return cmdState let log : MessageData → Command.CommandElabM Unit := if let some tok := firstToken? stx then logInfoAt tok @@ -910,7 +910,7 @@ def output (name : Ident) (severity : Option (WithSyntax MessageSeverity) := non return .code code.getString let codeStr := code.getString for (sev, out) in outs do - if out.trim == codeStr.trim then + if out.trimAscii == codeStr.trimAscii then if let some s := severity then if s.val != sev then let sevName := diff --git a/src/Lean/Elab/DocString/Builtin/Keywords.lean b/src/Lean/Elab/DocString/Builtin/Keywords.lean index 45973e6a6e..2f5ce5309a 100644 --- a/src/Lean/Elab/DocString/Builtin/Keywords.lean +++ b/src/Lean/Elab/DocString/Builtin/Keywords.lean @@ -54,14 +54,14 @@ private partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do | (``ParserDescr.trailingNode, #[_, _, _, p]) => containsAtom p atom | (``ParserDescr.unary, #[.app _ (.lit (.strVal _)), p]) => containsAtom p atom | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => containsAtom p atom - | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trim == atom) - | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (tk.trim == atom) + | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trimAscii == atom.toSlice) + | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (tk.trimAscii == atom.toSlice) | (``Parser.withAntiquot, #[_, p]) => containsAtom p atom | (``Parser.leadingNode, #[_, _, p]) => containsAtom p atom | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) => containsAtom p1 atom <||> containsAtom p2 atom - | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trim == atom) - | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (tk.trim == atom) + | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (tk.trimAscii == atom.toSlice) + | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (tk.trimAscii == atom.toSlice) | (``Parser.symbol, #[_nonlit]) => pure false | (``Parser.withCache, #[_, p]) => containsAtom p atom | _ => if tryWhnf then attempt (← Meta.whnf p) false else pure false @@ -81,7 +81,7 @@ private partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Exp | (``ParserDescr.symbol, #[.lit (.strVal tk)]) | (``Parser.symbol, #[.lit (.strVal tk)]) | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => - if tk.trim == atom then + if tk.trimAscii == atom.toSlice then pure (Expr.app (.const ``ParserDescr.const []) (toExpr ``Parser.skip)) else pure none | (``Parser.withAntiquot, #[_, p]) => containsAtom' p atom @@ -132,7 +132,7 @@ private partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option E | (``ParserDescr.symbol, #[.lit (.strVal tk)]) | (``Parser.symbol, #[.lit (.strVal tk)]) | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => - if tk.trim == atom then + if tk.trimAscii == atom.toSlice then pure (Expr.app (.const ``ParserDescr.const []) (toExpr ``Parser.skip)) else pure none | (``Parser.withAntiquot, #[_, p]) => startsWithAtom? p atom @@ -192,7 +192,7 @@ where | [] => return false | .ident .. :: _ => return false | .atom _ s :: ss => - if a.trim == s.trim then + if a.trimAscii == s.trimAscii then set as go ss else return false @@ -236,7 +236,7 @@ private def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Op | .node _ _ p | .trailingNode _ _ _ p | .unary _ p => parserDescrHasAtom atom p | .nonReservedSymbol tk _ | .symbol tk => - if tk.trim == atom then + if tk.trimAscii == atom.toSlice then pure (some (.const ``Parser.skip)) else pure none | .binary ``Parser.andthen p1 p2 => @@ -258,7 +258,7 @@ private def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermEl | .node _ _ p | .trailingNode _ _ _ p | .unary _ p => parserDescrStartsWithAtom atom p | .nonReservedSymbol tk _ | .symbol tk => - if tk.trim == atom then + if tk.trimAscii == atom.toSlice then pure (some (.const ``Parser.skip)) else pure none | .binary ``Parser.andthen p1 p2 => diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index 84217751fe..6da2a76396 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -179,7 +179,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" - |>.trim |> removeTrailingWhitespaceMarker + |>.trimAscii |>.copy |> removeTrailingWhitespaceMarker let { whitespace, ordering, filterFn, reportPositions } ← parseGuardMsgsSpec spec? -- do not forward snapshot as we don't want messages assigned to it to leak outside withReader ({ · with snap? := none }) do @@ -206,7 +206,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S else none let strings ← toCheck.toList.mapM (messageToString · reportPos?) let strings := ordering.apply strings - let res := "---\n".intercalate strings |>.trim + let res := "---\n".intercalate strings |>.trimAscii |>.copy if whitespace.apply expected == whitespace.apply res then -- Passed. Only put toPassthrough messages back on the message log modify fun st => { st with messages := toPassthrough } diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 1cb5d13d53..a6c817a4c6 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -45,7 +45,7 @@ private partial def floatOutAntiquotTerms (stx : Syntax) : StateT (Syntax → Te private def getSepFromSplice (splice : Syntax) : String := if let Syntax.atom _ sep := getAntiquotSpliceSuffix splice then - sep.dropRight 1 -- drop trailing * + sep.dropEnd 1 |>.copy -- drop trailing * else unreachable! diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 36e2a1e85a..cd03632325 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -244,7 +244,7 @@ where isValidAtom (s : String) : Bool := -- Pretty-printing instructions shouldn't affect validity - let s := s.trim + let s := s.trimAscii.copy !s.isEmpty && (s.front != '\'' || "''".isPrefixOf s) && s.front != '\"' && @@ -331,7 +331,7 @@ private partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : Mac where visit (stx : Syntax) (acc : String) : String := match stx.isStrLit? with - | some val => acc ++ (val.trim.map fun c => if c.isWhitespace then '_' else c).capitalize + | some val => acc ++ (val.trimAscii.copy.map fun c => if c.isWhitespace then '_' else c).capitalize | none => match stx with | Syntax.node _ k args => diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 28a18ce7f6..06bd6795b7 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -375,7 +375,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant let n? : Option Nat := do let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal let .str .anonymous s := tag.getId | none - s.dropPrefix? "inv" >>= Substring.Raw.toNat? + s.dropPrefix? "inv" >>= String.Slice.toNat? let some mv := do invariants[(← n?) - 1]? | do logErrorAt alt m!"No invariant with label {tag} {repr tag}." continue diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean index aa486e8f7d..af1da8708c 100644 --- a/src/Lean/Elab/Tactic/Doc.lean +++ b/src/Lean/Elab/Tactic/Doc.lean @@ -78,7 +78,7 @@ private def showParserName (n : Name) : MetaM MessageData := do let tok ← if let some descr := env.find? n |>.bind (·.value?) then if let some tk ← getFirstTk descr then - pure <| Std.Format.text tk.trim + pure <| Std.Format.text tk.trimAscii.copy else pure <| format n else pure <| format n pure <| .ofFormatWithInfos { @@ -166,7 +166,7 @@ def allTacticDocs : MetaM (Array TacticDoc) := do let userName : String ← if let some descr := env.find? tac |>.bind (·.value?) then if let some tk ← getFirstTk descr then - pure tk.trim + pure tk.trimAscii.copy else pure tac.toString else pure tac.toString diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index c3683192d8..e34bb8c194 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -342,7 +342,7 @@ private def expandUserTactic (tac : TSyntax `tactic) (goal : MVarId) : MetaM (Ar if line.startsWith " [apply] " then let tacticText := line.drop " [apply] ".length let env ← getEnv - if let .ok stx := Parser.runParserCategory env `tactic tacticText then + if let .ok stx := Parser.runParserCategory env `tactic tacticText.copy then suggestions := suggestions.push ⟨stx⟩ pure (some suggestions)) diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index dd38c7af32..afa15417d6 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -154,7 +154,7 @@ deriving Repr, Inhabited private def ValidationState.ofSource (input : String) : ValidationState where lines := input.splitOn "\n" |>.zipIdx - |>.filter (!·.1.trim.isEmpty) + |>.filter (!·.1.trimAscii.isEmpty) |>.toArray -- Workaround to account for the fact that `Input` expects "EOF" to be a valid position @@ -258,9 +258,9 @@ where let (_, closing) ← fence numTicks <|> fail s!"Missing closing code fence for block with header '{infoString}'" -- Validate code block: - unless closing.trim.isEmpty do + unless closing.trimAscii.isEmpty do fail s!"Expected a closing code fence, but found the nonempty info string `{closing}`" - let info ← match ErrorExplanation.CodeInfo.parse infoString with + let info ← match ErrorExplanation.CodeInfo.parse infoString.copy with | .ok i => pure i | .error s => fail s @@ -277,7 +277,7 @@ where fence (ticksToClose : Option Nat := none) := attempt do let line ← any if line.startsWith "```" then - let numTicks := line.takeWhile (· == '`') |>.length + let numTicks := line.takeWhile (· == '`') |>.copy |>.length match ticksToClose with | none => return (numTicks, line.drop numTicks) | some n => diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean index ca8e96a0e2..065d3aa7c3 100644 --- a/src/Lean/Linter/List.lean +++ b/src/Lean/Linter/List.lean @@ -157,7 +157,7 @@ def bitVecWidths (t : InfoTree) : List (Syntax × Name) := /-- Strip optional suffixes from a binder name. -/ def stripBinderName (s : String) : String := - s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂" |>.stripSuffix "₃" |>.stripSuffix "₄" + s.dropSuffix "'" |>.dropSuffix "₁" |>.dropSuffix "₂" |>.dropSuffix "₃" |>.dropSuffix "₄" |>.copy /-- Allowed names for index variables. -/ def allowedIndices : List String := ["i", "j", "k", "start", "stop", "step"] diff --git a/src/Lean/LoadDynlib.lean b/src/Lean/LoadDynlib.lean index aaecfafe0c..ee648f1fe7 100644 --- a/src/Lean/LoadDynlib.lean +++ b/src/Lean/LoadDynlib.lean @@ -97,7 +97,7 @@ def loadPlugin (path : System.FilePath) : IO Unit := do let dynlib ← Dynlib.load path -- Lean libraries can be prefixed with `lib` or suffixed with `_shared` -- under some configurations. We strip these from the initializer symbol. - let name := name.stripPrefix "lib" |>.stripSuffix "_shared" + let name := name.dropPrefix "lib" |>.dropSuffix "_shared" let name := s!"initialize_{name}" let some sym := dynlib.get? name | throw <| IO.userError s!"error loading plugin, initializer not found '{name}'" diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index f6a45773f2..ce8fed4544 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1111,7 +1111,7 @@ def symbolFn (sym : String) : ParserFn := symbolFnAux sym ("'" ++ sym ++ "'") def symbolNoAntiquot (sym : String) : Parser := - let sym := sym.trim + let sym := sym.trimAscii.copy { info := symbolInfo sym fn := symbolFn sym } @@ -1154,7 +1154,7 @@ def nonReservedSymbolInfo (sym : String) (includeIdent : Bool) : ParserInfo := { } def nonReservedSymbolNoAntiquot (sym : String) (includeIdent := false) : Parser := - let sym := sym.trim + let sym := sym.trimAscii.copy { info := nonReservedSymbolInfo sym includeIdent, fn := nonReservedSymbolFn sym } @@ -1236,8 +1236,8 @@ def unicodeSymbolFn (sym asciiSym : String) : ParserFn := set_option linter.unusedVariables false in def unicodeSymbolNoAntiquot (sym asciiSym : String) (preserveForPP : Bool) : Parser := - let sym := sym.trim - let asciiSym := asciiSym.trim + let sym := sym.trimAscii.copy + let asciiSym := asciiSym.trimAscii.copy { info := unicodeSymbolInfo sym asciiSym fn := unicodeSymbolFn sym asciiSym } @@ -1893,7 +1893,7 @@ def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anony -- ========================= def sepByElemParser (p : Parser) (sep : String) : Parser := - withAntiquotSpliceAndSuffix `sepBy p (symbol (sep.trim ++ "*")) + withAntiquotSpliceAndSuffix `sepBy p (symbol (sep.trimAscii.copy ++ "*")) def sepBy (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser := sepByNoAntiquot (sepByElemParser p sep) psep allowTrailingSep diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean index cf0a8691de..84ee968490 100644 --- a/src/Lean/Parser/Tactic/Doc.lean +++ b/src/Lean/Parser/Tactic/Doc.lean @@ -260,7 +260,7 @@ def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do let exts := getTacticExtensions env tactic if exts.size == 0 then "" - else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight + else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimAsciiEnd |>.copy where indentLine (str: String) : String := (if str.all (·.isWhitespace) then str else " " ++ str) ++ "\n" diff --git a/src/Lean/Parser/Term/Doc.lean b/src/Lean/Parser/Term/Doc.lean index a7d5be49df..4df8a3c059 100644 --- a/src/Lean/Parser/Term/Doc.lean +++ b/src/Lean/Parser/Term/Doc.lean @@ -72,7 +72,7 @@ the docstring. -/ def getRecommendedSpellingString (env : Environment) (declName : Name) : String := Id.run do let spellings := getRecommendedSpellingsForName env declName if spellings.size == 0 then "" - else "\n\nConventions for notations in identifiers:\n\n" ++ String.join (spellings.toList.map bullet) |>.trimRight + else "\n\nConventions for notations in identifiers:\n\n" ++ String.join (spellings.toList.map bullet) |>.trimAsciiEnd |>.copy where indentLine (str : String) : String := (if str.all (·.isWhitespace) then str else " " ++ str) ++ "\n" @@ -81,7 +81,7 @@ where let additionalInfoLines := spelling.additionalInformation?.map (·.splitOn "\n") match additionalInfoLines with | none | some [] => firstLine ++ ".\n\n" - | some [l] => firstLine ++ s!" ({l.trimRight}).\n\n" + | some [l] => firstLine ++ s!" ({l.trimAsciiEnd}).\n\n" | some ls => firstLine ++ ".\n\n" ++ String.join (ls.map indentLine) ++ "\n\n" end Lean.Parser.Term.Doc diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 66cd2b55c4..5a15b599f5 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -380,14 +380,14 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit let st ← get -- If there is no space between `tk` and the next word, see if we should insert a discretionary space. - if st.leadWord != "" && tk.trimRight == tk then + if st.leadWord != "" && tk.trimAsciiEnd == tk.toSlice then let insertSpace ← do if ident && st.leadWordIdent then -- Both idents => need space pure true else -- Check if we would parse more than `tk` as a single token - let tk' := tk.trimLeft + let tk' := tk.trimAsciiStart.copy let t ← parseToken $ tk' ++ st.leadWord if t.pos ≤ tk'.rawEndPos then -- stopped within `tk` => use it as is @@ -398,21 +398,21 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit if !insertSpace then -- extend `leadWord` if not prefixed by whitespace push tk - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "", leadWordIdent := ident } + modify fun st => { st with leadWord := if tk.trimAsciiStart == tk.toSlice then tk ++ st.leadWord else "", leadWordIdent := ident } else pushLine push tk - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident } + modify fun st => { st with leadWord := if tk.trimAsciiStart == tk.toSlice then tk else "", leadWordIdent := ident } else -- already separated => use `tk` as is if st.leadWord == "" then - push tk.trimRight + push tk.trimAsciiEnd.copy else if tk.endsWith " " then pushLine - push tk.trimRight + push tk.trimAsciiEnd.copy else push tk -- preserve special whitespace for tokens like ":=\n" - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident } + modify fun st => { st with leadWord := if tk.trimAsciiStart == tk.toSlice then tk else "", leadWordIdent := ident } if let SourceInfo.original ss _ _ _ := info then -- preserve non-whitespace content (comments) @@ -613,7 +613,7 @@ instance : Std.Format.MonadPrettyFormat M where pushOutput s := do let lineEnd := s.find (· == '\n') if lineEnd < s.rawEndPos then - let s := (String.Pos.Raw.extract s 0 lineEnd).trimRight ++ continuation + let s := (String.Pos.Raw.extract s 0 lineEnd).trimAsciiEnd.copy ++ continuation modify fun st => { st with line := st.line.append s } throw () else diff --git a/src/Lean/Server/Completion/ImportCompletion.lean b/src/Lean/Server/Completion/ImportCompletion.lean index d7bdd9a1fc..6165cca13e 100644 --- a/src/Lean/Server/Completion/ImportCompletion.lean +++ b/src/Lean/Server/Completion/ImportCompletion.lean @@ -96,7 +96,7 @@ def collectAvailableImportsFromLake : IO (Option AvailableImports) := do args := #["available-imports"] } let lakeProc ← IO.Process.spawn spawnArgs - let stdout := String.trim (← lakeProc.stdout.readToEnd) + let stdout := String.trimAscii (← lakeProc.stdout.readToEnd) |>.copy let exitCode ← lakeProc.wait match exitCode with | 0 => diff --git a/src/Lean/Server/FileWorker/ExampleHover.lean b/src/Lean/Server/FileWorker/ExampleHover.lean index bcd280a435..4456bc9edd 100644 --- a/src/Lean/Server/FileWorker/ExampleHover.lean +++ b/src/Lean/Server/FileWorker/ExampleHover.lean @@ -88,11 +88,11 @@ def rewriteExamples (docstring : String) : String := Id.run do -- The current state, which tracks the context of the line being processed let mut inOutput : RWState := .normal for l in lines do - let indent := l.takeWhile (· == ' ') |>.length - let mut l' := l.trimLeft + let indent := l.takeWhile (· == ' ') |>.copy |>.length + let mut l' := l.trimAsciiStart -- Is this a code block fence? if l'.startsWith "```" then - let count := l'.takeWhile (· == '`') |>.length + let count := l'.takeWhile (· == '`') |>.copy |>.length l' := l'.dropWhile (· == '`') l' := l'.dropWhile (· == ' ') match inOutput with diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean index f2d280d7c7..630fcc37b1 100644 --- a/src/Lean/Server/FileWorker/SetupFile.lean +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -51,7 +51,7 @@ partial def runLakeSetupFile processStderr (acc ++ line) let stderr ← ServerTask.IO.asTask (processStderr "") - let stdout := String.trim (← lakeProc.stdout.readToEnd) + let stdout := String.trimAscii (← lakeProc.stdout.readToEnd) |>.copy let stderr ← IO.ofExcept stderr.get let exitCode ← lakeProc.wait return ⟨spawnArgs, exitCode, stdout, stderr⟩ diff --git a/src/Lean/Server/Test/Runner.lean b/src/Lean/Server/Test/Runner.lean index 8cb924b41e..26b0af9f9c 100644 --- a/src/Lean/Server/Test/Runner.lean +++ b/src/Lean/Server/Test/Runner.lean @@ -636,13 +636,13 @@ def processGenericRequest : RunnerM Unit := do logResponse s.method params def processDirective (ws directive : String) (directiveTargetLineNo : Nat) : RunnerM Unit := do - let directive := directive.drop 1 + let directive := directive.drop 1 |>.copy let colon := directive.posOf ':' - let method := String.Pos.Raw.extract directive 0 colon |>.trim + let method := String.Pos.Raw.extract directive 0 colon |>.trimAscii |>.copy -- TODO: correctly compute in presence of Unicode let directiveTargetColumn := ws.rawEndPos + "--" let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn.byteIdx } - let params := if colon < directive.rawEndPos then String.Pos.Raw.extract directive (colon + ':') directive.rawEndPos |>.trim else "{}" + let params := if colon < directive.rawEndPos then String.Pos.Raw.extract directive (colon + ':') directive.rawEndPos |>.trimAscii |>.copy 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/Shell.lean b/src/Lean/Shell.lean index a7081adf28..19c43e65fd 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -254,8 +254,8 @@ def shellMain let contents ← if contents.startsWith "#lang" then let endLinePos := contents.posOf '\n' - let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos |>.trim - if langId == "lean4" then + let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos |>.trimAscii + if langId == "lean4".toSlice then pure () -- do nothing for now else IO.eprintln s!"unknown language '{langId}'\n"; diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index 46b28168a1..f4b17e8097 100644 --- a/src/Lean/Util/Path.lean +++ b/src/Lean/Util/Path.lean @@ -150,7 +150,7 @@ def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Nam throw $ IO.userError s!"input file '{fname}' must be contained in root directory ({rootDir})" -- NOTE: use `fname` instead of `fname.normalize` to preserve casing on all platforms let fnameSuffix := fname.toString.drop rootDir.toString.length - let modNameStr := FilePath.mk fnameSuffix |>.withExtension "" + let modNameStr := FilePath.mk fnameSuffix.copy |>.withExtension "" let modName := modNameStr.components.foldl Name.mkStr Name.anonymous pure modName @@ -179,6 +179,6 @@ def findSysroot (lean := "lean") : IO FilePath := do cmd := lean args := #["--print-prefix"] } - return out.trim + return out.trimAscii.copy end Lean diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index e6f3ddf01c..04fbe815c4 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -627,7 +627,7 @@ private def pad (size : Nat) (n : Int) (cut : Bool := false) : String := let numStr := toString n if numStr.length > size then - sign ++ if cut then numStr.drop (numStr.length - size) else numStr + sign ++ if cut then numStr.drop (numStr.length - size) |>.copy else numStr else sign ++ leftPad size '0' numStr @@ -636,7 +636,7 @@ private def rightTruncate (size : Nat) (n : Int) (cut : Bool := false) : String let numStr := toString n if numStr.length > size then - sign ++ if cut then numStr.take size else numStr + sign ++ if cut then numStr.take size |>.copy else numStr else sign ++ rightPad size '0' numStr diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index 8b03f27cd9..a523f3e0b2 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -66,8 +66,8 @@ def idFromPath (path : System.FilePath) : Option String := do let last₁ ← res[res.size - 2]? if last₁ = "zoneinfo" - then some <| last.trim - else some <| last₁.trim ++ "/" ++ last.trim + then some <| last.trimAscii.copy + else some <| last₁.trimAscii.copy ++ "/" ++ last.trimAscii /-- Retrieves the timezone rules from the local timezone data file. diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index d58fb2ff05..465cfb52c5 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/src/lake/Lake/Build/Actions.lean @@ -70,7 +70,7 @@ public def compileLeanModule unless txt.isEmpty do logInfo s!"stdout:\n{txt}" unless out.stderr.isEmpty do - logInfo s!"stderr:\n{out.stderr.trim}" + logInfo s!"stderr:\n{out.stderr.trimAscii}" if out.exitCode ≠ 0 then error s!"Lean exited with code {out.exitCode}" diff --git a/src/lake/Lake/Build/ExternLib.lean b/src/lake/Lake/Build/ExternLib.lean index 08ddffbca4..9ed94d229d 100644 --- a/src/lake/Lake/Build/ExternLib.lean +++ b/src/lake/Lake/Build/ExternLib.lean @@ -68,7 +68,7 @@ def computeDynlibOfShared (sharedLibTarget : Job FilePath) : SpawnM (Job Dynlib) if Platform.isWindows then return {path := sharedLib, name := stem} else if stem.startsWith "lib" then - return {path := sharedLib, name := stem.drop 3} + return {path := sharedLib, name := stem.drop 3 |>.copy} else error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix" else diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index 5e585b4353..0bfa1a02b8 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -74,13 +74,13 @@ where if pkg.isEmpty then return .package .anonymous else - return .package (stringToLegalOrSimpleName pkg) + return .package (stringToLegalOrSimpleName pkg.copy) else if target.startsWith "+" then - return .module (stringToLegalOrSimpleName (target.drop 1)) + return .module (stringToLegalOrSimpleName (target.drop 1).copy) else parsePackageTarget .anonymous target | [pkg, target] => - let pkg := if pkg.startsWith "@" then pkg.drop 1 else pkg + let pkg := if pkg.startsWith "@" then pkg.drop 1 |>.copy else pkg if pkg.isEmpty then parsePackageTarget .anonymous target else @@ -91,7 +91,7 @@ where if target.isEmpty then throw s!"ill-formed target: default package targets are not supported in partial build keys" else if target.startsWith "+" then - let target := target.drop 1 |> stringToLegalOrSimpleName + let target := target.drop 1 |>.copy |> stringToLegalOrSimpleName return .packageModule pkg target else let target := stringToLegalOrSimpleName target diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean index 0510e1d846..7251119554 100644 --- a/src/lake/Lake/CLI/Build.lean +++ b/src/lake/Lake/CLI/Build.lean @@ -210,7 +210,7 @@ private def resolveTargetBaseSpec : EIO CliError (Array BuildSpec) := do if spec.startsWith "@" then let spec := spec.drop 1 - resolveTargetLikeSpec ws spec facet (explicit := true) + resolveTargetLikeSpec ws spec.copy facet (explicit := true) else if spec.startsWith "+" then let mod := spec.drop 1 |>.toName if let some mod := ws.findTargetModule? mod then @@ -237,7 +237,7 @@ public def parseExeTargetSpec | some exe => return exe | none => throw <| CliError.unknownExe spec | [pkgSpec, targetSpec] => - let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec + let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 |>.copy else pkgSpec let pkg ← parsePackageSpec ws pkgSpec let targetName := stringToLegalOrSimpleName targetSpec match pkg.findLeanExe? targetName with diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 293f9d187f..f23fd69a1f 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -525,7 +525,7 @@ public def init | none => error s!"illegal package name: could not derive one from '{path}'" else return name - let name := name.trim + let name := name.trimAscii.copy validatePkgName name IO.FS.createDirAll cwd initPkg cwd (stringToLegalOrSimpleName name) tmp lang env offline @@ -534,7 +534,7 @@ public def new (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) (cwd : FilePath := ".") (offline := false) : LoggerIO PUnit := do - let name := name.trim + let name := name.trimAscii.copy validatePkgName name let name := stringToLegalOrSimpleName name let dirName := dotlessName name diff --git a/src/lake/Lake/CLI/Translate.lean b/src/lake/Lake/CLI/Translate.lean index 1bf4b967af..e519ee2755 100644 --- a/src/lake/Lake/CLI/Translate.lean +++ b/src/lake/Lake/CLI/Translate.lean @@ -32,6 +32,6 @@ public def Package.mkConfigString (pkg : Package) (lang : ConfigLang) : LogIO St let env ← importModulesUsingCache #[`Lake] {} 1024 let pp := ppModule <| descopeTSyntax <| pkg.mkLeanConfig match (← pp.toIO {fileName := "", fileMap := default} {env} |>.toBaseIO) with - | .ok (fmt, _) => pure <| (toString fmt).trim ++ "\n" + | .ok (fmt, _) => pure <| (toString fmt).trimAscii.copy ++ "\n" | .error ex => error s!"(internal) failed to pretty print Lean configuration: {ex.toString}" diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 651339e6c2..29b9b9768e 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -265,7 +265,7 @@ def Dependency.mkRequire (cfg : Dependency) : RequireDecl := Unhygienic.run do let ver? ← if let some ver := cfg.version? then if ver.startsWith "git#" then - some <$> `(verSpec|git $(toLean <| ver.drop 4)) + some <$> `(verSpec|git $(toLean <| ver.drop 4 |>.copy)) else some <$> `(verSpec|$(toLean ver):term) else diff --git a/src/lake/Lake/Config/Cache.lean b/src/lake/Lake/Config/Cache.lean index feacd66615..a33620b4a9 100644 --- a/src/lake/Lake/Config/Cache.lean +++ b/src/lake/Lake/Config/Cache.lean @@ -48,7 +48,7 @@ public partial def parse (inputName : String) (contents : String) : LoggerIO Cac let rec loop (i : Nat) (cache : CacheMap) (stopPos pos : String.Pos.Raw) := do let lfPos := contents.posOfAux '\n' stopPos pos let line := String.Pos.Raw.extract contents pos lfPos - if line.trim.isEmpty then + if line.trimAscii.isEmpty then return cache let cache ← id do match Json.parse line >>= fromJson? with @@ -63,7 +63,7 @@ public partial def parse (inputName : String) (contents : String) : LoggerIO Cac loop (i+1) cache stopPos (lfPos.next' contents h) let lfPos := contents.posOfAux '\n' contents.rawEndPos 0 let line := String.Pos.Raw.extract contents 0 lfPos - checkSchemaVersion inputName line.trim + checkSchemaVersion inputName line.trimAscii.copy if h : lfPos.atEnd contents then return {} else diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index e99a9133bc..62fe7d9100 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -159,7 +159,7 @@ public def compute reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1" noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false enableArtifactCache := (← IO.getEnv "LAKE_ARTIFACT_CACHE").bind envToBool? |>.getD false - cacheKey? := (← IO.getEnv "LAKE_CACHE_KEY").map (·.trim) + cacheKey? := (← IO.getEnv "LAKE_CACHE_KEY").map (·.trimAscii.copy) cacheArtifactEndpoint? := (← IO.getEnv "LAKE_CACHE_ARTIFACT_ENDPOINT").map normalizeUrl cacheRevisionEndpoint? := (← IO.getEnv "LAKE_CACHE_REVISION_ENDPOINT").map normalizeUrl githashOverride := (← IO.getEnv "LEAN_GITHASH").getD "" @@ -193,7 +193,7 @@ where else return default normalizeUrl url := - if url.back == '/' then url.dropRight 1 else url + if url.back == '/' then url.dropEnd 1 |>.copy else url /-- The string Lake uses to identify Lean in traces. diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index 36add2e04e..a486d98ab9 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/src/lake/Lake/Config/InstallPath.lean @@ -166,7 +166,7 @@ environment variables. If `ELAN` is set but empty, Elan is considered disabled. public def findElanInstall? : BaseIO (Option ElanInstall) := do if let some home ← IO.getEnv "ELAN_HOME" then let elan := (← IO.getEnv "ELAN").getD "elan" - if elan.trim.isEmpty then + if elan.trimAscii.isEmpty then return none else return some {elan, home} @@ -184,7 +184,7 @@ public def findLeanSysroot? (lean := "lean") : BaseIO (Option FilePath) := do args := #["--print-prefix"] } if out.exitCode == 0 then - pure <| some <| FilePath.mk <| out.stdout.trim + pure <| some <| FilePath.mk <| out.stdout.trimAscii.copy else pure <| none act.catchExceptions fun _ => pure none @@ -234,7 +234,7 @@ where cmd := leanExe sysroot |>.toString, args := #["--githash"] } - return out.stdout.trim + return out.stdout.trimAscii.copy findAr := do if let some ar ← IO.getEnv "LEAN_AR" then return FilePath.mk ar @@ -322,7 +322,7 @@ public def findLeanInstall? : BaseIO (Option LeanInstall) := do return some <| ← LeanInstall.get sysroot let lean ← do if let some lean ← IO.getEnv "LEAN" then - if lean.trim.isEmpty then + if lean.trimAscii.isEmpty then return none else pure lean diff --git a/src/lake/Lake/Config/OutFormat.lean b/src/lake/Lake/Config/OutFormat.lean index 7178cf9b9d..c98a882ae0 100644 --- a/src/lake/Lake/Config/OutFormat.lean +++ b/src/lake/Lake/Config/OutFormat.lean @@ -26,8 +26,8 @@ export ToText (toText) public instance (priority := 0) [ToString α] : ToText α := ⟨toString⟩ public instance : ToText Json := ⟨Json.compress⟩ -public instance [ToText α] : ToText (List α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropRight 1)⟩ -public instance [ToText α] : ToText (Array α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropRight 1)⟩ +public instance [ToText α] : ToText (List α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropEnd 1 |>.copy)⟩ +public instance [ToText α] : ToText (Array α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropEnd 1 |>.copy)⟩ /-- Class used to format target output as text for `lake query`. -/ public class QueryText (α : Type u) where diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean index 4f1f0c20dc..3ddcb7ab74 100644 --- a/src/lake/Lake/Reservoir.lean +++ b/src/lake/Lake/Reservoir.lean @@ -147,12 +147,12 @@ public def Reservoir.fetchPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO | .error e => errorWithLog do logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned unsupported JSON: {e}" - logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}" + logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trimAscii}" failure | .error e => errorWithLog do logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned invalid JSON: {e}" - logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}" + logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trimAscii}" failure /-- @@ -199,10 +199,10 @@ public def Reservoir.fetchPkgVersions | .error e => errorWithLog do logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned unsupported JSON: {e}" - logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}" + logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trimAscii}" failure | .error e => errorWithLog do logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned invalid JSON: {e}" - logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}" + logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trimAscii}" failure diff --git a/src/lake/Lake/Toml/Data/DateTime.lean b/src/lake/Lake/Toml/Data/DateTime.lean index f2648db54f..ba75890bb8 100644 --- a/src/lake/Lake/Toml/Data/DateTime.lean +++ b/src/lake/Lake/Toml/Data/DateTime.lean @@ -105,7 +105,7 @@ public def ofString? (dt : String) : Option DateTime := do | [d,t] => let d ← Date.ofString? d if t.back == 'Z' || t.back == 'z' then - return offsetDateTime d (← Time.ofString? <| t.dropRight 1) + return offsetDateTime d (← Time.ofString? <| t.dropEnd 1 |>.copy) else if let [t,o] := t.splitToList (· == '+') then return offsetDateTime d (← Time.ofString? t) <| some (false, ← Time.ofString? o) else if let [t,o] := t.splitToList (· == '-') then diff --git a/src/lake/Lake/Toml/Data/Value.lean b/src/lake/Lake/Toml/Data/Value.lean index 6dbfad25ec..15f19a1e7d 100644 --- a/src/lake/Lake/Toml/Data/Value.lean +++ b/src/lake/Lake/Toml/Data/Value.lean @@ -133,7 +133,7 @@ public def ppTable (t : Table) : String := | _ => (appendKeyval ts k v, fs) -- Ensures root table keys come before subtables -- See https://github.com/leanprover/lean4/issues/4099 - (ts.push '\n' ++ fs).trimRight.push '\n' + (ts.push '\n' ++ fs).trimAsciiEnd.copy.push '\n' where appendKeyval s k v := s.append s!"{ppKey k} = {v}\n" diff --git a/src/lake/Lake/Toml/Elab/Value.lean b/src/lake/Lake/Toml/Elab/Value.lean index 284b66c57a..246e371ac0 100644 --- a/src/lake/Lake/Toml/Elab/Value.lean +++ b/src/lake/Lake/Toml/Elab/Value.lean @@ -42,9 +42,9 @@ def decodeDecNum (s : String) : Nat := def decodeSign (s : String) : Bool × String := if s.front == '-' then - (true, s.drop 1) + (true, s.drop 1 |>.copy) else if s.front == '+' then - (false, s.drop 1) + (false, s.drop 1 |>.copy) else (false, s) @@ -122,7 +122,7 @@ def elabDateTime (x : TSyntax ``dateTime) : CoreM DateTime := do -------------------------------------------------------------------------------- def elabLiteralString (x : TSyntax ``literalString) : CoreM String := do - return (← elabLit x "literalString").drop 1 |>.dropRight 1 + return (← elabLit x "literalString").drop 1 |>.dropEnd 1 |>.copy def decodeHexDigits (s : Substring.Raw) : Nat := s.foldl (init := 0) fun n c => n*16 + decodeHexDigit c @@ -164,23 +164,23 @@ partial def elabBasicStringCore (lit : String) (i : String.Pos.Raw := 0) (out := def elabBasicString (x : TSyntax ``basicString) : CoreM String := do let spelling ← elabLit x "basic string" - withRef x <| elabBasicStringCore (spelling.drop 1 |>.dropRight 1) + withRef x <| elabBasicStringCore (spelling.drop 1 |>.dropEnd 1 |>.copy) def dropInitialNewline (s : String) : String := if s.front == '\r' then - s.drop 2 + s.drop 2 |>.copy else if s.front == '\n' then - s.drop 1 + s.drop 1 |>.copy else s def elabMlLiteralString (x : TSyntax ``mlLiteralString) : CoreM String := do let spelling ← elabLit x "multi-line literal string" - return dropInitialNewline (spelling.drop 3 |>.dropRight 3) + return dropInitialNewline (spelling.drop 3 |>.dropEnd 3 |>.copy) def elabMlBasicString (x : TSyntax ``mlBasicString) : CoreM String := do let spelling ← elabLit x "multi-line basic string" - withRef x <| elabBasicStringCore (dropInitialNewline (spelling.drop 3 |>.dropRight 3)) + withRef x <| elabBasicStringCore (dropInitialNewline (spelling.drop 3 |>.dropEnd 3 |>.copy)) def elabString (x : TSyntax ``string) : CoreM String := do match x with diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean index 6f32c54e94..90ae988081 100644 --- a/src/lake/Lake/Toml/ParserUtil.lean +++ b/src/lake/Lake/Toml/ParserUtil.lean @@ -173,7 +173,7 @@ public def chAtom.parenthesizer (_ : Char) (_ : List String) (_ : ParserFn) : P /-- Parse the trimmed string as an atom (but use the full string for formatting). -/ public def strAtom (s : String) (expected := [s!"'{s}'"]) (trailingFn := skipFn) : Parser := - atom (strFn s.trim expected) trailingFn + atom (strFn s.trimAscii.copy expected) trailingFn @[combinator_formatter strAtom] public def strAtom.formatter (s : String) (_ : List String) (_ : ParserFn) : Formatter := diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean index 21dc1ef5ef..412677f1d5 100644 --- a/src/lake/Lake/Util/Cli.lean +++ b/src/lake/Lake/Util/Cli.lean @@ -8,6 +8,7 @@ module prelude import Init.Data.Array.Basic public import Init.Data.String.TakeDrop +import Init.Data.String.Slice namespace Lake @@ -69,15 +70,15 @@ variable [Monad m] [MonadStateOf ArgList m] /-- Process a short option of the form `-x=arg`. -/ @[inline] public def shortOptionWithEq (handle : Char → m α) (opt : String) : m α := do - consArg (opt.drop 3); handle (String.Pos.Raw.get opt ⟨1⟩) + consArg (opt.drop 3).copy; handle (String.Pos.Raw.get opt ⟨1⟩) /-- Process a short option of the form `"-x arg"`. -/ @[inline] public def shortOptionWithSpace (handle : Char → m α) (opt : String) : m α := do - consArg <| opt.drop 2 |>.trimLeft; handle (String.Pos.Raw.get opt ⟨1⟩) + consArg <| opt.drop 2 |>.trimAsciiStart |>.copy; handle (String.Pos.Raw.get opt ⟨1⟩) /-- Process a short option of the form `-xarg`. -/ @[inline] public def shortOptionWithArg (handle : Char → m α) (opt : String) : m α := do - consArg (opt.drop 2); handle (String.Pos.Raw.get opt ⟨1⟩) + consArg (opt.drop 2).copy; handle (String.Pos.Raw.get opt ⟨1⟩) /-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/ @[inline] public def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean index 49e74a5dba..8e41e39f78 100644 --- a/src/lake/Lake/Util/FilePath.lean +++ b/src/lake/Lake/Util/FilePath.lean @@ -64,8 +64,8 @@ Examples: -/ public def modOfFilePath (path : FilePath) : Name := let path := removeExts path.normalize.toString - let path := path.stripSuffix FilePath.pathSeparator.toString - FilePath.components path |>.foldl .str .anonymous + let path := path.dropSuffix FilePath.pathSeparator.toString + FilePath.components path.copy |>.foldl .str .anonymous where removeExts (s : String) (i := s.rawEndPos) (e := s.rawEndPos) := if h : i = 0 then diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean index 1c7281be21..f6d985ca7a 100644 --- a/src/lake/Lake/Util/Git.lean +++ b/src/lake/Lake/Util/Git.lean @@ -30,7 +30,7 @@ public def filterUrl? (url : String) : Option String := if url.startsWith "git" then none else if url.endsWith ".git" then - some <| url.dropRight 4 + some <| url.dropEnd 4 |>.copy else some url diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index d0a635d70c..257b81dc72 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -155,8 +155,8 @@ public instance : ToString LogEntry := ⟨LogEntry.toString⟩ {level := .error, message} public def LogEntry.ofSerialMessage (msg : SerialMessage) : LogEntry := - let str := if msg.caption.trim.isEmpty then - msg.data.trim else s!"{msg.caption.trim}:\n{msg.data.trim}" + let str := if msg.caption.trimAscii.isEmpty then + msg.data.trimAscii.copy else s!"{msg.caption.trimAscii}:\n{msg.data.trimAscii}" { level := .ofMessageSeverity msg.severity message := mkErrorStringWithPos msg.fileName msg.pos str none @@ -446,7 +446,7 @@ from an `ELogT` (e.g., `LogIO`). let buf ← liftM (m := BaseIO) buf.get let out := String.fromUTF8! buf.data unless out.isEmpty do - logInfo s!"stdout/stderr:\n{out.trim}" + logInfo s!"stdout/stderr:\n{out.trimAscii}" return a /-- Throw with the logged error `message`. -/ diff --git a/src/lake/Lake/Util/Proc.lean b/src/lake/Lake/Util/Proc.lean index aa89942908..46025384cc 100644 --- a/src/lake/Lake/Util/Proc.lean +++ b/src/lake/Lake/Util/Proc.lean @@ -22,9 +22,9 @@ public def mkCmdLog (args : IO.Process.SpawnArgs) : String := [Monad m] (out : IO.Process.Output) (log : String → m PUnit) : m Unit := do unless out.stdout.isEmpty do - log s!"stdout:\n{out.stdout.trim}" + log s!"stdout:\n{out.stdout.trimAscii}" unless out.stderr.isEmpty do - log s!"stderr:\n{out.stderr.trim}" + log s!"stderr:\n{out.stderr.trimAscii}" @[inline] public def rawProc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO IO.Process.Output := do withLogErrorPos do @@ -50,13 +50,13 @@ public def captureProc' (args : IO.Process.SpawnArgs) : LogIO (IO.Process.Output logError s!"external command '{args.cmd}' exited with code {out.exitCode}" @[inline] public def captureProc (args : IO.Process.SpawnArgs) : LogIO String := do - return (← captureProc' args).stdout.trim -- remove, e.g., newline at end + return (← captureProc' args).stdout.trimAscii.copy -- remove, e.g., newline at end public def captureProc? (args : IO.Process.SpawnArgs) : BaseIO (Option String) := do EIO.catchExceptions (h := fun _ => pure none) do let out ← IO.Process.output args if out.exitCode = 0 then - return some out.stdout.trim -- remove, e.g., newline at end + return some out.stdout.trimAscii.copy -- remove, e.g., newline at end else return none diff --git a/src/lake/Lake/Util/Url.lean b/src/lake/Lake/Util/Url.lean index ee29e3a3d1..e41b5ec70d 100644 --- a/src/lake/Lake/Util/Url.lean +++ b/src/lake/Lake/Util/Url.lean @@ -120,7 +120,7 @@ public def getUrl? | .ok none => error s!"curl's JSON output did not contain a response code" | .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}" if code == 200 then - return some out.stdout.trim + return some out.stdout.trimAscii.copy else if code == 404 then return none else diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index 0d2f8f2d92..208a777fbc 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -260,7 +260,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do ("", ver) let noOrigin := origin.isEmpty if tag.startsWith "v" then - if let .ok ver := StdVer.parse (tag.drop 1) then + if let .ok ver := StdVer.parse (tag.drop 1).copy then if noOrigin|| origin == defaultOrigin then return .release ver else if let some date := tag.dropPrefix? "nightly-" then @@ -268,7 +268,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do if noOrigin then return .nightly date else if let some suffix := origin.dropPrefix? defaultOrigin then - if suffix.isEmpty || suffix == "-nightly".toRawSubstring then + if suffix.isEmpty || suffix == "-nightly".toSlice then return .nightly date else if let some n := tag.dropPrefix? "pr-release-" then if let some n := n.toNat? then @@ -283,7 +283,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do public def ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do try let toolchainString ← IO.FS.readFile toolchainFile - return some <| ToolchainVer.ofString toolchainString.trim + return some <| ToolchainVer.ofString toolchainString.trimAscii.copy catch | .noFileOrDirectory .. => return none diff --git a/tests/compiler/trie.lean b/tests/compiler/trie.lean index afb8c5c50b..5ed7a202d1 100644 --- a/tests/compiler/trie.lean +++ b/tests/compiler/trie.lean @@ -50,7 +50,7 @@ def Array.findPrefix : Array String → String → Array String := fun a s => /-- The intended semanics of `Trie.matchPrefix`: Longest prefix found in trie -/ def Array.matchPrefix : Array String → String → Option String := fun a s => Id.run do for i in List.reverse (List.range (s.length + 1)) do - let pfix := s.take i + let pfix := s.take i |>.copy if let some _ := a.find? (· == pfix) then return some pfix return none diff --git a/tests/lean/Uri.lean b/tests/lean/Uri.lean index c1ffed8905..969927e75a 100644 --- a/tests/lean/Uri.lean +++ b/tests/lean/Uri.lean @@ -27,7 +27,7 @@ def testShouldEscape := (Char.ofNat 127).toString] -- for 0x7F assert! should_quote.data.all (λ c => let x := (escapeUri c.toString) - x.length == 3 && x.take 1 == "%") + x.length == 3 && x.take 1 == "%".toSlice) true def testPartialEscape := diff --git a/tests/lean/docparse/run.lean b/tests/lean/docparse/run.lean index 40c948769a..28d7fb1cca 100644 --- a/tests/lean/docparse/run.lean +++ b/tests/lean/docparse/run.lean @@ -106,7 +106,7 @@ def main : List String → IO UInt32 | IO.eprintln "Expected file in current directory" return 4 let kind := file.takeWhile (· != '_') - let some p := testConfigs.lookup kind + let some p := testConfigs.lookup kind.copy | IO.eprintln s!"Not found in test configs: {kind}" return 5 IO.print <| ← test p (← IO.FS.readFile inputFile) diff --git a/tests/lean/run/errorExplanationElab.lean b/tests/lean/run/errorExplanationElab.lean index 9e3a487be0..70e8244f03 100644 --- a/tests/lean/run/errorExplanationElab.lean +++ b/tests/lean/run/errorExplanationElab.lean @@ -120,7 +120,7 @@ def withReportedOutput (x : MetaM α) : MetaM Unit := do -- We need to omit the path to the file, since that's host-dependent; also drop line -- number to avoid noise let dropped := res.splitOn fileName |>.map (fun (s : String) => s.dropWhile (· != ' ')) - logInfo ("".intercalate dropped) + logInfo ("".toSlice.intercalate dropped) /-- info: error(lean.bar): function is noncomputable diff --git a/tests/lean/run/levenshtein.lean b/tests/lean/run/levenshtein.lean index bda6806875..362261bd3c 100644 --- a/tests/lean/run/levenshtein.lean +++ b/tests/lean/run/levenshtein.lean @@ -39,7 +39,7 @@ def deletions (n : Nat) (s : String) : Array String := for s' in deletions n' s do if s'.isEmpty then break for i in [0:s'.length] do - let d := s'.take i ++ s'.drop (i + 1) + let d := (s'.take i).copy ++ s'.drop (i + 1) if !out.contains d then out := out.push d return out.reverse @@ -92,7 +92,7 @@ def insertions (toInsert : String) (s : String) : Array String := Id.run do let mut next := #[] for s' in out do for i in [0:s'.length + 1] do - next := next.push ((s'.take i).push c ++ s'.drop i) + next := next.push ((s'.take i |>.copy).push c ++ s'.drop i) out := next return out diff --git a/tests/lean/run/string_gaps.lean b/tests/lean/run/string_gaps.lean index c0af8cf144..780953c18d 100644 --- a/tests/lean/run/string_gaps.lean +++ b/tests/lean/run/string_gaps.lean @@ -151,7 +151,7 @@ def String.dedent (s : String) : Option String := if !parts.all (·.startsWith "|") then none else - p₀ ++ "\n" ++ String.intercalate "\n" (parts.map fun p => p.drop 1) + p₀ ++ "\n" ++ String.intercalate "\n" (parts.map fun p => p.drop 1 |>.copy) elab "d!" s:str : term => do let some s := s.raw.isStrLit? | Lean.Elab.throwIllFormedSyntax diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean index 1fea1a6df9..e3dab62a15 100644 --- a/tests/lean/string_imp2.lean +++ b/tests/lean/string_imp2.lean @@ -46,7 +46,7 @@ it₁.remainingToString ++ "-" ++ it₂.remainingToString #eval "αβ".mkIterator.next.prev.hasPrev #eval "abc" == "abc" #eval "abc" == "abd" -#eval "αβγ".drop 1 +#eval "αβγ".drop 1 |>.copy #eval "αβγ".takeRight 1 def ss : Substring.Raw := "0123abcdαβγδ".toRawSubstring