chore: clean up string processing (#13802)

This PR removes some uses of `String.length`.

src/LeanIR.lean

@@ -41,9 +41,8 @@ def mkIRData (env : Environment) : IO ModuleData := do
   }
 
 def setConfigOption (opts : Options) (arg : String) : IO Options := do
-  if !arg.startsWith "-D" then
+  let some arg := arg.dropPrefix? "-D" |
     throw <| .userError s!"invalid trailing argument `{arg}`, expected argument of the form `-Dopt=val`"
-  let arg := arg.drop "-D".length
   let pos := arg.find '='
   if h : pos.IsAtEnd then
     throw <| .userError "invalid -D parameter, argument must contain '='"

src/lake/Lake/Toml/Data/DateTime.lean

@@ -84,7 +84,7 @@ public protected def toString (t : Time) : String :=
   if t.fracMantissa = 0 then
     s
   else
-    s!"{s}.{rpad (zpad t.fracMantissa t.fracExponent) '0' 3}"
+    s!"{s}.{rpadAscii (zpad t.fracMantissa t.fracExponent) '0' 3}"
 
 public instance : ToString Time := ⟨Time.toString⟩
 

src/lake/Lake/Toml/Data/Value.lean

@@ -68,7 +68,7 @@ public def ppString (s : String) : String :=
     | '\\' => s ++ "\\\\"
     | _ =>
       if c.val < 0x20 || c.val == 0x7F then
-        s ++ "\\u" ++ lpad (String.ofList <| Nat.toDigits 16 c.val.toNat) '0' 4
+        s ++ "\\u" ++ lpadAscii (String.ofList <| Nat.toDigits 16 c.val.toNat) '0' 4
       else
         s.push c
   s.push '\"'

src/lake/Lake/Toml/Elab/Value.lean

@@ -58,7 +58,7 @@ def elabDecInt (x : TSyntax ``decInt) : CoreM Int := do
   return decodeDecInt <| ← elabLit x "decimal integer"
 
 def decodeMantissa (s : String) : Nat × Nat :=
-  let (m,e) := s.foldl (init := (0,s.length)) fun (m,e) c =>
+  let (m,e) := s.foldl (init := (0,s.lengthAssumingAscii)) fun (m,e) c =>
     match c with
     | '_' => (m,e)
     | '.' => (m,0)

src/lake/Lake/Util/Cli.lean

@@ -121,7 +121,7 @@ variable [Monad m] [MonadStateOf ArgList m]
   (shortHandle : Char → m α) (longHandle : String → m α)
   (opt : String)
 : m α :=
-  if opt.length == 2 then -- `-x`
+  if opt.chars.length == 2 then -- `-x`
     shortHandle (String.Pos.Raw.get opt ⟨1⟩)
   else -- `-c(.+)`
     match String.Pos.Raw.get opt ⟨2⟩ with
@@ -148,7 +148,7 @@ public def processLeadingOption (handle : String → m PUnit) : m PUnit := do
   match (← getArgs) with
   | [] => pure ()
   | arg :: args =>
-    if arg.length > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
+    if arg.chars.length > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       setArgs args
       handle arg
 
@@ -158,7 +158,7 @@ Consumes empty leading arguments in the argument list.
 -/
 public partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do
   if let arg :: args ← getArgs then
-    let len := arg.length
+    let len := arg.chars.length
     if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       setArgs args
       handle arg
@@ -172,7 +172,7 @@ public partial def collectArgs
   (option : String → m PUnit) (args : Array String := #[])
 : m (Array String) := do
   if let some arg ← takeArg? then
-    let len := arg.length
+    let len := arg.chars.length
     if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       option arg
       collectArgs option args

src/lake/Lake/Util/String.lean

@@ -14,14 +14,14 @@ import Init.Data.String.Length
 
 namespace Lake
 
-public def lpad (s : String) (c : Char) (len : Nat) : String :=
-  "".pushn c (len - s.length) ++ s
+public def lpadAscii (s : String) (c : Char) (len : Nat) : String :=
+  "".pushn c (len - s.lengthAssumingAscii) ++ s
 
-public def rpad (s : String) (c : Char) (len : Nat) : String :=
-  s.pushn c (len - s.length)
+public def rpadAscii (s : String) (c : Char) (len : Nat) : String :=
+  s.pushn c (len - s.lengthAssumingAscii)
 
 public def zpad (n : Nat) (len : Nat) : String :=
-  lpad (toString n) '0' len
+  lpadAscii (toString n) '0' len
 
 /-- Returns whether a string is composed of only hexadecimal digits. -/
 public def isHex (s : String) : Bool :=

src/lake/Lake/Util/Version.lean

@@ -275,7 +275,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do
         let suffix ← (rest.drop 10).dropPrefix? "-rev"
         suffix.toString.toNat?
       -- Accept if no suffix (plain nightly) or valid -revK suffix
-      if rest.length ≤ 10 || rev?.isSome then
+      if rest.chars.length ≤ 10 || rev?.isSome then
         if noOrigin then
           return .nightly date rev?
         else if let some suffix := origin.dropPrefix? defaultOrigin then