chore: clean up string processing (#13797)

This PR drops some more `String.length` from the codebase.

src/Lean/Compiler/ExternAttr.lean

@@ -8,6 +8,9 @@ module
 prelude
 public import Lean.ProjFns
 public import Lean.Attributes
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.OrderInstances
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -72,30 +75,30 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
 def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=
   externAttr.getParam? env n
 
-private def parseOptNum : Nat → (pattern : String) → (it : pattern.Pos) → Nat → pattern.Pos × Nat
-  | 0,   _      , it, r => (it, r)
-  | n+1, pattern, it, r =>
-    if h : it.IsAtEnd then (it, r)
-    else
-      let c := it.get h
-      if '0' <= c && c <= '9'
-      then parseOptNum n pattern (it.next h) (r*10 + (c.toNat - '0'.toNat))
-      else (it, r)
+private def parseOptNum (pattern : String.Slice) (it : pattern.Pos) (r : Nat) : pattern.Pos × Nat :=
+  if h : it.IsAtEnd then (it, r)
+  else
+    let c := it.get h
+    if '0' <= c && c <= '9'
+    then
+      parseOptNum pattern (it.next h) (r*10 + (c.toNat - '0'.toNat))
+    else (it, r)
+termination_by it
 
-def expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.Pos) → String → String
-  | 0,   _,       _,  r => r
-  | i+1, pattern, it, r =>
-    if h : it.IsAtEnd then r
-    else let c := it.get h
-      if c ≠ '#' then expandExternPatternAux args i pattern (it.next h) (r.push c)
-      else
-        let it      := it.next h
-        let (it, j) := parseOptNum it.remainingBytes pattern it 0
-        let j       := j-1
-        expandExternPatternAux args i pattern it (r ++ args.getD j "")
+def expandExternPatternAux (args : List String) (pattern : String) (it : pattern.Pos) (r : String) : String :=
+  if h : it.IsAtEnd then r
+  else let c := it.get h
+    if c ≠ '#' then expandExternPatternAux args pattern (it.next h) (r.push c)
+    else
+      let it₁      := it.next h
+      let (it₂, j) := parseOptNum (pattern.sliceFrom it₁) (String.Slice.startPos _) 0
+      let j       := j-1
+      have : it < String.Pos.ofSliceFrom it₂ := Std.lt_of_lt_of_le String.Pos.lt_next String.Pos.le_ofSliceFrom
+      expandExternPatternAux args pattern (String.Pos.ofSliceFrom it₂) (r ++ args.getD j "")
+termination_by it
 
 def expandExternPattern (pattern : String) (args : List String) : String :=
-  expandExternPatternAux args pattern.length pattern pattern.startPos ""
+  expandExternPatternAux args pattern pattern.startPos ""
 
 def mkSimpleFnCall (fn : String) (args : List String) : String :=
   fn ++ "(" ++ ((args.intersperse ", ").foldl (·++·) "") ++ ")"

src/Lean/DocString/Parser.lean

@@ -1277,7 +1277,7 @@ mutual
           s.mkError s!"Internal error - index {atDepth} wasn't the directive fence - it was {stx} in {s.stxStack.back}, {s.stxStack.pop.back}, {s.stxStack.pop.pop.back}, {s.stxStack.pop.pop.pop.back}"
 
     withFenceSize (atDepth : Nat) (p : Nat → ParserFn) : ParserFn :=
-      withFence atDepth fun _ str => p str.length
+      withFence atDepth fun _ str => p str.lengthAssumingAscii -- `str` is made up of all `':'`
 
     withFencePos (atDepth : Nat) (p : Position → ParserFn) : ParserFn :=
       withFence atDepth fun info _ c s => p (c.fileMap.toPosition info.getPos?.get!) c s

src/Lean/Elab/Deriving/Repr.lean

@@ -41,7 +41,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
       if (← isType x <||> isProof x) then
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ "_")
       else
-        let indent := Syntax.mkNumLit <| toString ((toString fieldName |>.length) + " := ".length)
+        let indent := Syntax.mkNumLit <| toString ((toString fieldName |>.chars.length) + " := ".lengthAssumingAscii)
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ (Format.group (Format.nest $indent (repr ($target.$(mkIdent fieldName):ident)))))
     `(Format.bracket "{ " $fields:term " }")