Fix

Author: TwoFX

src/Init/Data/String/Extra.lean

@@ -153,25 +153,25 @@ def crlfToLf (text : String) : String :=
   go "" 0 0
 where
   go (acc : String) (accStop pos : String.Pos.Raw) : String :=
-    if h : text.atEnd pos then
+    if h : pos.atEnd text then
       -- note: if accStop = 0 then acc is empty
-      if accStop = 0 then text else acc ++ text.extract accStop pos
+      if accStop = 0 then text else acc ++ accStop.extract text pos
     else
-      let c := text.get' pos h
-      let pos' := text.next' pos h
-      if h' : ¬ text.atEnd pos' ∧ c == '\r' ∧ text.get pos' == '\n' then
-        let acc := acc ++ text.extract accStop pos
-        go acc pos' (text.next' pos' h'.1)
+      let c := pos.get' text h
+      let pos' := pos.next' text h
+      if h' : ¬ pos'.atEnd text ∧ c == '\r' ∧ pos'.get text == '\n' then
+        let acc := acc ++ accStop.extract text pos
+        go acc pos' (pos'.next' text h'.1)
       else
         go acc accStop pos'
   termination_by text.utf8ByteSize - pos.byteIdx
   decreasing_by
     decreasing_with
-      change text.utf8ByteSize - (text.next (text.next pos)).byteIdx < text.utf8ByteSize - pos.byteIdx
+      change text.utf8ByteSize - ((pos.next text).next text).byteIdx < text.utf8ByteSize - pos.byteIdx
       have k := Nat.gt_of_not_le <| mt decide_eq_true h
       exact Nat.sub_lt_sub_left k (Nat.lt_trans (String.Pos.Raw.lt_next text pos) (String.Pos.Raw.lt_next _ _))
     decreasing_with
-      change text.utf8ByteSize - (text.next pos).byteIdx < text.utf8ByteSize - pos.byteIdx
+      change text.utf8ByteSize - (pos.next text).byteIdx < text.utf8ByteSize - pos.byteIdx
       have k := Nat.gt_of_not_le <| mt decide_eq_true h
       exact Nat.sub_lt_sub_left k (String.Pos.Raw.lt_next _ _)
 

src/Init/Data/ToString/Name.lean

@@ -37,7 +37,7 @@ private partial def needsNoEscapeAsciiRest (s : String) (i : Nat) : Bool :=
 
 -- If you change this, also change the corresponding function in `Init.Meta`.
 @[inline] private def needsNoEscape (s : String) (h : s.utf8ByteSize > 0) : Bool :=
-  needsNoEscapeAscii s h || isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest
+  needsNoEscapeAscii s h || isIdFirst s.front && (s.toSubstring.drop 1).all isIdRest
 
 -- If you change this, also change the corresponding function in `Init.Meta`.
 @[inline] private def escape (s : String) : String :=

src/Init/System/FilePath.lean

@@ -77,8 +77,8 @@ There is no guarantee that two equivalent paths normalize to the same path.
 def normalize (p : FilePath) : FilePath := Id.run do
   let mut p := p
   -- normalize drive letter
-  if isWindows && p.toString.length >= 2 && (p.toString.get 0).isLower && p.toString.get ⟨1⟩ == ':' then
-    p := ⟨p.toString.set 0 (p.toString.get 0).toUpper⟩
+  if isWindows && p.toString.length >= 2 && p.toString.front.isLower && String.Pos.Raw.get p.toString ⟨1⟩ == ':' then
+    p := ⟨p.toString.capitalize⟩
   -- normalize separator
   unless pathSeparators.length == 1 do
     p := ⟨p.toString.map fun c => if pathSeparators.contains c then pathSeparator else c⟩
@@ -129,15 +129,15 @@ If the path is that of the root directory or the root of a drive letter, `none`
 Otherwise, the path's parent directory is returned.
 -/
 def parent (p : FilePath) : Option FilePath :=
-  let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  let extractParentPath := FilePath.mk <$> String.Pos.Raw.extract p.toString {} <$> posOfLastSep p
   if p.isAbsolute then
     let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
     if p.toString.length == lengthOfRootDirectory then
       -- `p` is a root directory
       none
     else if posOfLastSep p == some (String.Pos.Raw.mk (lengthOfRootDirectory - 1)) then
       -- `p` is a direct child of the root
-      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
+      some ⟨String.Pos.Raw.extract p.toString 0 ⟨lengthOfRootDirectory⟩⟩
     else
       -- `p` is an absolute path with at least two subdirectories
       extractParentPath
@@ -153,7 +153,7 @@ directory.
 -/
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with
-    | some sepPos => p.toString.extract (sepPos + '/') p.toString.endPos
+    | some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.endPos
     | none        => p.toString
   if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart
 
@@ -173,7 +173,7 @@ def fileStem (p : FilePath) : Option String :=
   p.fileName.map fun fname =>
     match fname.revPosOf '.' with
     | some ⟨0⟩ => fname
-    | some pos => fname.extract 0 pos
+    | some pos => String.Pos.Raw.extract fname 0 pos
     | none     => fname
 
 /--
@@ -192,7 +192,7 @@ def extension (p : FilePath) : Option String :=
   p.fileName.bind fun fname =>
     match fname.revPosOf '.' with
     | some 0   => none
-    | some pos => some <| fname.extract (pos + '.') fname.endPos
+    | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.endPos
     | none     => none
 
 /--

src/Init/System/Uri.lean

@@ -93,8 +93,8 @@ def pathToUri (fname : System.FilePath) : String := Id.run do
   if System.Platform.isWindows then
     -- normalize drive letter
     -- lower-case drive letters seem to be preferred in URIs
-    if uri.length >= 2 && (uri.get 0).isUpper && uri.get ⟨1⟩ == ':' then
-      uri := uri.set 0 (uri.get 0).toLower
+    if uri.length >= 2 && uri.front.isUpper && String.Pos.Raw.get uri ⟨1⟩ == ':' then
+      uri := uri.decapitalize
     uri := uri.map (fun c => if c == '\\' then '/' else c)
   uri := uri.foldl (fun s c => s ++ UriEscape.uriEscapeAsciiChar c) ""
   let result := if uri.startsWith "/" then "file://" ++ uri else "file:///" ++ uri
@@ -110,7 +110,7 @@ def fileUriToPath? (uri : String) : Option System.FilePath := Id.run do
     p := p.dropWhile (λ c => c != '/') -- drop the hostname.
     -- On Windows, the path "/c:/temp" needs to become "C:/temp"
     if System.Platform.isWindows && p.length >= 2 &&
-        p.get 0 == '/' && (p.get ⟨1⟩).isAlpha && p.get ⟨2⟩ == ':' then
+        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
     some p

src/Lean/AddDecl.lean

@@ -35,7 +35,7 @@ private def isNamespaceName : Name → Bool
 private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
   match name with
     | .str _ s =>
-      if s.get 0 == '_' then
+      if s.front == '_' then
         -- Do not register namespaces that only contain internal declarations.
         env
       else

src/Lean/Compiler/ExportAttr.lean

@@ -13,7 +13,7 @@ public section
 namespace Lean
 
 private def isValidCppId (id : String) : Bool :=
-  let first := id.get 0;
+  let first := id.front;
   first.isAlpha  && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_')
 
 private def isValidCppName : Name → Bool

src/Lean/Data/FuzzyMatching.lean

@@ -30,29 +30,29 @@ section Utils
   if string.isEmpty then
     #[]
   else if string.length == 1 then
-    #[f none (string.get 0) none]
+    #[f none (String.Pos.Raw.get string 0) none]
   else Id.run do
     let mut result := Array.mkEmpty string.length
-    result := result.push <| f none (string.get 0) (string.get ⟨1⟩)
+    result := result.push <| f none (String.Pos.Raw.get string 0) (String.Pos.Raw.get string ⟨1⟩)
     -- TODO: the following code is assuming all characters are ASCII
     for i in [2:string.length] do
-      result := result.push <| f (string.get ⟨i - 2⟩) (string.get ⟨i - 1⟩) (string.get ⟨i⟩)
-    result.push <| f (string.get ⟨string.length - 2⟩) (string.get ⟨string.length - 1⟩) none
+      result := result.push <| f (String.Pos.Raw.get string ⟨i - 2⟩) (String.Pos.Raw.get string ⟨i - 1⟩) (String.Pos.Raw.get string ⟨i⟩)
+    result.push <| f (String.Pos.Raw.get string ⟨string.length - 2⟩) (String.Pos.Raw.get string ⟨string.length - 1⟩) none
 
 private partial def containsInOrderLower (a b : String) : Bool := Id.run do
   go ⟨0⟩ ⟨0⟩
 where
   go (aPos bPos : String.Pos.Raw) : Bool :=
-    if ha : a.atEnd aPos then
+    if ha : aPos.atEnd a then
       true
-    else if hb : b.atEnd bPos then
+    else if hb : bPos.atEnd b then
       false
     else
-      let ac := a.get' aPos ha
-      let bc := b.get' bPos hb
-      let bPos := b.next' bPos hb
+      let ac := aPos.get' a ha
+      let bc := bPos.get' b hb
+      let bPos := bPos.next' b hb
       if ac.toLower == bc.toLower then
-        let aPos := a.next' aPos ha
+        let aPos := aPos.next' a ha
         go aPos bPos
       else
         go aPos bPos
@@ -173,7 +173,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
 
       let mut matchScore := .awful
 
-      if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) patternRoles[patternIdx]! wordRoles[wordIdx]! then
+      if allowMatch (String.Pos.Raw.get pattern ⟨patternIdx⟩) (String.Pos.Raw.get word ⟨wordIdx⟩) patternRoles[patternIdx]! wordRoles[wordIdx]! then
         if patternIdx >= 1 then
           let runLength := runLengths[getIdx (patternIdx - 1) (wordIdx - 1)]! + 1
           runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength
@@ -248,7 +248,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
     matchResult (patternIdx wordIdx : Nat) (patternRole wordRole : CharRole) (consecutive : Score) : Int16 := Id.run do
       let mut score : Int16 := 1
       /- Case-sensitive equality or beginning of a segment in pattern and word. -/
-      if (pattern.get ⟨patternIdx⟩) == (word.get ⟨wordIdx⟩) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then
+      if (String.Pos.Raw.get pattern ⟨patternIdx⟩) == (String.Pos.Raw.get word ⟨wordIdx⟩) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then
         score := score + 1
       /- Matched end of word with end of pattern -/
       if wordIdx == word.length - 1 && patternIdx == pattern.length - 1 then

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -109,12 +109,12 @@ instance : ToJson CompletionIdentifier where
 instance : FromJson CompletionIdentifier where
   fromJson?
     | .str s =>
-      let c := s.get 0
+      let c := s.front
       if c == 'c' then
-        let declName := s.extract ⟨1⟩ s.endPos |>.toName
+        let declName := String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName
         .ok <| .const declName
       else if c == 'f' then
-        let id := ⟨s.extract ⟨1⟩ s.endPos |>.toName⟩
+        let id := ⟨String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName⟩
         .ok <| .fvar id
       else
         .error "Expected string with prefix `c` or `f` in `FromJson` instance of `CompletionIdentifier`."

src/Lean/Data/Lsp/Utf16.lean

@@ -34,7 +34,7 @@ def utf16Length (s : String) : Nat :=
 
 private def codepointPosToUtf16PosFromAux (s : String) : Nat → Pos.Raw → Nat → Nat
   | 0,    _,       utf16pos => utf16pos
-  | cp+1, utf8pos, utf16pos => codepointPosToUtf16PosFromAux s cp (s.next utf8pos) (utf16pos + csize16 (s.get utf8pos))
+  | cp+1, utf8pos, utf16pos => codepointPosToUtf16PosFromAux s cp (utf8pos.next s) (utf16pos + csize16 (utf8pos.get s))
 
 /-- Computes the UTF-16 offset of the `n`-th Unicode codepoint
 in the substring of `s` starting at UTF-8 offset `off`.
@@ -47,7 +47,7 @@ def codepointPosToUtf16Pos (s : String) (pos : Nat) : Nat :=
 
 private partial def utf16PosToCodepointPosFromAux (s : String) : Nat → Pos.Raw → Nat → Nat
   | 0,        _,       cp => cp
-  | utf16pos, utf8pos, cp => utf16PosToCodepointPosFromAux s (utf16pos - csize16 (s.get utf8pos)) (s.next utf8pos) (cp + 1)
+  | utf16pos, utf8pos, cp => utf16PosToCodepointPosFromAux s (utf16pos - csize16 (utf8pos.get s)) (utf8pos.next s) (cp + 1)
 
 /-- Computes the position of the Unicode codepoint at UTF-16 offset
 `utf16pos` in the substring of `s` starting at UTF-8 offset `off`. -/
@@ -60,7 +60,7 @@ def utf16PosToCodepointPos (s : String) (pos : Nat) : Nat :=
 /-- Starting at `utf8pos`, finds the UTF-8 offset of the `p`-th codepoint. -/
 def codepointPosToUtf8PosFrom (s : String) : String.Pos.Raw → Nat → String.Pos.Raw
   | utf8pos, 0 => utf8pos
-  | utf8pos, p+1 => codepointPosToUtf8PosFrom s (s.next utf8pos) p
+  | utf8pos, p+1 => codepointPosToUtf8PosFrom s (utf8pos.next s) p
 
 end String
 

src/Lean/Data/Name.lean

@@ -111,7 +111,7 @@ def hasNum : Name → Bool
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
-  | str p s => s.get 0 == '_' || isInternal p
+  | str p s => s.front == '_' || isInternal p
   | num p _ => isInternal p
   | _       => false
 
@@ -122,7 +122,7 @@ We use name parts starting with `_` internally to create auxiliary names (e.g.,
 This function checks if any component of the name starts with `_`, or is numeric.
 -/
 def isInternalOrNum : Name → Bool
-  | .str p s => s.get 0 == '_' || isInternalOrNum p
+  | .str p s => s.front == '_' || isInternalOrNum p
   | .num _ _ => true
   | _       => false