Merge main into hammer

Author: JOSHCLUNE

Auto/EvaluateAuto/TestAuto.lean

@@ -167,16 +167,16 @@ where
     let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some res := Result.ofConcise? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a concise representation of a `Result`"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
     let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some time := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
     let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some hb := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let name := Name.parseUniqRepr line.toString
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
+    let name := Name.parseUniqRepr line
     return (name, res, time, hb)
 
 def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do
@@ -332,7 +332,7 @@ def readEATAResult (config : EvalAutoAsyncConfig) :
   let allFiles := (← System.FilePath.readDir resultFolder).map IO.FS.DirEntry.path
   let mut ret := #[]
   for file in allFiles do
-    if !(← System.FilePath.isDir file) && (file.toString.takeEnd 7).toString == ".result" then
+    if !(← System.FilePath.isDir file) && file.toString.takeEnd 7 == ".result" then
       ret := ret.append (← readRunAutoOnConstsResult file.toString)
   return ret
 

Auto/EvaluateAuto/TestTactics.lean

@@ -335,15 +335,15 @@ def readEvalTacticsAtModuleResult (resultFile : String) : CoreM (Array (Name ×
 where
   analyzeLine (fileName line : String) : CoreM (Name × Array (Result × Nat × Nat)) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 3
-    let tr := ((line.takeWhile (fun c => c != ']')).toString.splitOn ", ")
-    let tr : Array (Result × Nat × Nat) ← (Array.mk tr).mapM (fun s => do
+    let tr := ((line.takeWhile (fun c => c != ']')).split ", ").toStringArray
+    let tr : Array (Result × Nat × Nat) ← tr.mapM (fun s => do
       let [sr, st, sh] := s.splitOn " "
         | throwError s!"{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`"
       match Result.ofConcise? sr, String.toNat? st, String.toNat? sh with
       | .some r, .some t, .some h => return (r, t, h)
       | _, _, _ => throwError s!"{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`")
-    let line := (line.dropWhile (fun c => c != ']')).drop 2
-    let name := Name.parseUniqRepr line.toString
+    let line := ((line.dropWhile (fun c => c != ']')).drop 2).toString
+    let name := Name.parseUniqRepr line
     return (name, tr)
 
 structure EvalTacticOnMathlibConfig where
@@ -495,8 +495,8 @@ def readETMHTResult (config : EvalTacticOnMathlibConfig) :
   for path in allPaths do
     if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := ((path.toString.drop (resultFolder.length + 1)).dropEnd 7).toString
-      let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
+      let suffix := (path.toString.drop (resultFolder.length + 1)).dropEnd 7
+      let modName := (suffix.split "/").toStringArray.foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return ret
 
@@ -516,11 +516,11 @@ def readETMHTResultAllowNonRet (config : EvalTacticOnMathlibConfig) :
     if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let raw ← IO.FS.readFile path
       if raw.length == 0 then
-        nonRet := nonRet.push ((path.toString.dropEnd 7).toString)
+        nonRet := nonRet.push (path.toString.dropEnd 7).toString
         continue
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := ((path.toString.drop (resultFolder.length + 1)).dropEnd 7).toString
-      let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
+      let suffix := (path.toString.drop (resultFolder.length + 1)).dropEnd 7
+      let modName := (suffix.split "/").toStringArray.foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return (nonRet, ret)
 
@@ -580,7 +580,7 @@ def readETMHTEvaluateFiles (config : EvalTacticOnMathlibConfig) : CoreM (Array N
       let [name, retCode] := line.splitOn ":"
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
       let name := (name.dropEnd 1).toString
-      let retCode := (retCode.drop 1).toString
+      let retCode := retCode.drop 1
       let some retCode := retCode.toNat?
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
       retEnd := retEnd.push (str2Name name, retCode)

Auto/EvaluateAuto/TestTranslation.lean

@@ -103,14 +103,14 @@ where analyzeLine (line : String) : CoreM (Name × Nat × Option Nat) := do
   let line := (line.dropWhile (fun c => c != ' ')).drop 1
   let .some rawSize := rawSizeStr.toNat?
     | throwError "{decl_name%} :: {rawSizeStr} is not a string representation of a Nat"
-  let monoSizeStr := (line.takeWhile (fun c => c != ' ')).toString
-  let line := (line.dropWhile (fun c => c != ' ')).drop 1
+  let monoSizeStr := line.takeWhile (fun c => c != ' ')
+  let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
   let mut monoSize? : Option Nat := .none
   if monoSizeStr != "N" then
     let .some monoSize := monoSizeStr.toNat?
       | throwError "{decl_name%} :: {monoSizeStr} is not a string representation of a Nat"
     monoSize? := .some monoSize
-  let name := Name.parseUniqRepr line.toString
+  let name := Name.parseUniqRepr line
   return (name, rawSize, monoSize?)
 
 /--

Auto/IR/SMT.lean

@@ -14,7 +14,7 @@ namespace IR.SMT
 def isSimpleSymbol (s : String) : Bool :=
   let symbSpecials := "~!@$%^&*_-+=<>.?/"
   let front := s.front.isAlpha || (symbSpecials.contains s.front)
-  let body := s.all (fun c => Char.isAlphanum c || symbSpecials.contains c)
+  let body := s.all (fun (c : Char) => c.isAlphanum || symbSpecials.contains c)
   s.length != 0 && front && body
 
 -- <index>      ::= <numeral> | <symbol>

Auto/Parser/TPTP.lean

@@ -400,7 +400,7 @@ def ident2StringConst (s : String) : Option StringConst :=
       match x, y.toNat? with
       | .some l, .some y' => .some (l.push (Char.ofNat y'))
       | _,       _        => .none
-    match s.take 9, (((s.drop 9).toString.splitOn "d").drop 1).foldl foldFn (.some "") with
+    match s.take 9, (((s.drop 9).split "d").drop 1).toStringArray.foldl foldFn (.some "") with
     | "t_strVal_", .some s => .some (.strVal s)
     | _,         _       => .none
 
@@ -428,7 +428,7 @@ open Embedding.Lam in
 def ident2BitVecConst (s : String) : Option BitVecConst :=
   match s.take 7 with
   | "t_bvVal" =>
-    match (s.drop 7).toString.splitOn "_" with
+    match ((s.drop 7).split "_").toList with
     | ["", ns, is] =>
       match ns.toNat?, is.toNat? with
       | .some n, .some i => .some (.bvVal n i)
@@ -550,35 +550,35 @@ def ident2BitVecConst (s : String) : Option BitVecConst :=
       | "ashr", .some n => .some (.bvsmtashr n)
       | _,      _       => .none
   | "t_bvapp" =>
-    match s.take 11, (s.drop 11).toString.splitOn "_" with
+    match s.take 11, ((s.drop 11).split "_").toList with
     | "t_bvappend_", [ns, ms] =>
       match ns.toNat?, ms.toNat? with
       | .some n, .some m => .some (.bvappend n m)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvext" =>
-    match s.take 12, (s.drop 12).toString.splitOn "_" with
+    match s.take 12, ((s.drop 12).split "_").toList with
     | "t_bvextract_", [ns, hs, ls] =>
       match ns.toNat?, hs.toNat?, ls.toNat? with
       | .some n, .some h, .some l => .some (.bvextract n h l)
       | _,       _,       _       => .none
     | _,              _            => .none
   | "t_bvrep" =>
-    match s.take 11, (s.drop 11).toString.splitOn "_" with
+    match s.take 11, ((s.drop 11).split "_").toList with
     | "t_bvrepeat_", [ws, is] =>
       match ws.toNat?, is.toNat? with
       | .some w, .some i => .some (.bvrepeat w i)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvzer" =>
-    match s.take 15, (s.drop 15).toString.splitOn "_" with
+    match s.take 15, ((s.drop 15).split "_").toList with
     | "t_bvzeroExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvzeroExtend w v)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvsig" =>
-    match s.take 15, (s.drop 15).toString.splitOn "_" with
+    match s.take 15, ((s.drop 15).split "_").toList with
     | "t_bvsignExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvsignExtend w v)