parsing evaluation result

Auto/EvaluateAuto/NameArr.lean

@@ -11,75 +11,71 @@ def Name.canBeFilename (n : Name) : Bool :=
     match n with
     | .str _ s =>
       match s.get? 0 with
-      | .some c => s.all (fun c => c.isAlphanum || c == '_' || c == '\'')
+      | .some _ => s.all (fun c => c.isAlphanum || c == '_' || c == '\'')
       | .none => false
     | _ => false)
 
 /--
-  Unique string representation of array of names
-  We use `.` to separate fields of a name, and `\n` to separate names.
-  A `.` is appended to the end of each name.
-  A `\n` is further appended to the end of the last name.
-  We use `\` to escape `.` and `\n` occurring in the fields of names, i.e.,
-    `\.` represents literal `.`, `\\n` represents literal `\n`, and
-    `\\` represents literal `\`.
+  Unique string representation of names, where it is ensured that `\n` does not occur
+  A `.` is appended to the end of the name
+  We use "\\d" to represent ".", "\\n" to represent "\n", "\\\\" to represent "\\"
   To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields
 -/
-def NameArray.repr (ns : Array Name) : String :=
+def Name.uniqRepr (n : Name) : String :=
   let strRepr (s : String) : String :=
-    ((s.replace "\\" "\\\\").replace "." "\\.").replace "\n" "\\\n"
+    ((s.replace "\\" "\\\\").replace "." "\\d").replace "\n" "\\n"
   let compRepr (c : Name) : String :=
     match c with
     | .anonymous => ""
     | .mkNum _ n => s!"\\{n}"
     | .mkStr _ s => strRepr s
-  let nameRepr (n : Name) : String :=
-    String.join (n.components.map (fun c => compRepr c ++ "."))
-  String.join (ns.map (fun n => nameRepr n ++ "\n")).toList
+  String.join (n.components.map (fun c => compRepr c ++ "."))
 
-/-
-  Parse string representation of array of names
-  We use `.` to separate fields of a name, and `\n` to separate names
-  We use `\` to escape `.` and `\n` occurring in the fields of names, i.e.,
-    `\.` represents literal `.`, `\\n` represents literal `\n`, and
-    `\\` represents literal `\`.
-  To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields
+/--
+  Parsing unique representation of names, see `Name.uniqRepr`
 -/
-def NameArray.parse (repr : String) : Array Name := Id.run <| do
-  let mut curField := ""
-  let mut curFields : Array (String ⊕ Nat) := #[]
-  let mut allNames : Array Name := #[]
-  let mut escape := false
-  let mut num := false
-  for c in repr.data do
-    if !escape && c == '.' then
-      if num then
-        curFields := curFields.push (.inr ((String.toNat? curField).getD 0))
+def Name.parseUniqRepr (n : String) : Name :=
+  let compParse (s : String) : String ⊕ Nat := Id.run <| do
+    let s := s.data
+    if s[0]? == '\\' then
+      if let .some c := s[1]? then
+        if c.isDigit then
+          return .inr ((String.toNat? (String.mk (s.drop 1))).getD 0)
+    let mut ret := ""
+    let mut escape := false
+    for c in s do
+      if !escape then
+        if c != '\\' then
+          ret := ret.push c
+        else
+          escape := true
       else
-        curFields := curFields.push (.inl curField)
-      curField := ""
-      num := false
-      continue
-    if !escape && c == '\n' then
-      let curName := curFields.foldl (fun prev sn =>
-        match sn with
-        | .inl s => Name.mkStr prev s
-        | .inr n => Name.mkNum prev n) .anonymous
-      allNames := allNames.push curName
-      curFields := #[]
-      continue
-    if escape && c.isDigit then
-      num := true
-    if c == '\\' then
-      if escape then
         escape := false
-        curField := curField.push c
-      else
-        escape := true
-    else
-      escape := false
-      curField := curField.push c
-  return allNames
+        match c with
+        | '\\' => ret := ret.push '\\'
+        | 'd' => ret := ret.push '.'
+        | 'n' => ret := ret.push '\n'
+        | _ => ret := ret.push c
+    return .inl ret
+  let components := ((n.splitOn ".").dropLast).map compParse
+  components.foldl (fun prev sn =>
+    match sn with
+    | .inl s => Name.mkStr prev s
+    | .inr n => Name.mkNum prev n) .anonymous
+
+/--
+  Each name in the array is represented using `Name.uniqRepr`
+  Names are separated using `\n`. A `\n` is further appended to the end of the last name.
+-/
+def NameArray.repr (ns : Array Name) : String :=
+  String.join (ns.map (fun n => Name.uniqRepr n ++ "\n")).toList
+
+/-
+  Each name in the array is represented using `Name.uniqRepr`
+  Names are separated using `\n`. A `\n` is further appended to the end of the last name.
+-/
+def NameArray.parse (repr : String) : Array Name :=
+  Array.mk ((repr.splitOn "\n").map Name.parseUniqRepr).dropLast
 
 def NameArray.save (ns : Array Name) (fname : String) : IO Unit := do
   let fd ← IO.FS.Handle.mk fname .write

Auto/EvaluateAuto/Result.lean

@@ -36,7 +36,16 @@ def Result.concise : Result → String
 | .nonterminate => "T"
 | .subGoals => "G"
 | .exception _ => "E"
-
+#check Exception
+def Result.ofConcise? : String → Option Result
+| "S" => .some .success
+| "N" => .some .nonProp
+| "F" => .some .typeCheckFail
+| "U" => .some .typeUnequal
+| "T" => .some .nonterminate
+| "G" => .some .subGoals
+| "E" => .some (.exception (.error Syntax.missing "Filled_in_by_Result.ofConcise?"))
+| _   => .none
 
 open Elab Tactic in
 /--

Auto/EvaluateAuto/TestAuto.lean

@@ -163,7 +163,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
     fhandle.putStrLn s!"Elapsed time: {(← IO.monoMsNow) - startTime} ms"
     fhandle.putStrLn s!"\nSummary:\n"
     for ((name, result), idx) in (names.zip results).zipWithIndex do
-      fhandle.putStrLn s!"{idx} {result.concise} {name}"
+      fhandle.putStrLn s!"{idx} {result.concise} {Name.uniqRepr name}"
 
 def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do
   let names ← NameArray.load fname

Auto/EvaluateAuto/TestTactics.lean

@@ -210,7 +210,7 @@ def evalAtModule
     fhandle.putStrLn s!"Elapsed time : {(← IO.monoMsNow) - startTime} ms"
     fhandle.putStrLn s!"\nSummary:\n"
     for ((name, result), idx) in results.zipWithIndex do
-      fhandle.putStrLn s!"{idx} {result.map Result.concise} {name}"
+      fhandle.putStrLn s!"{idx} {result.map Result.concise} {Name.uniqRepr name}"
 where
   evalAction
     (context : Core.Context) (state : Core.State) (ci : ConstantInfo)
@@ -269,7 +269,7 @@ def EvalProc.create (path : String) (args : Array String) : IO EvalProc :=
 def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : CoreM Unit := do
   let mms ← mathlibModules
   if !(← allMathlibModuleNamesCanBeFilename) then
-    throwError "{decl_name%} :: Some mathlib modules have extra-ordinary names. Evaluation code needs to be changed!"
+    throwError "{decl_name%} :: Some Mathlib modules have extra-ordinary names. Evaluation code needs to be changed!"
   if !(← System.FilePath.isDir config.resultFolder) then
     IO.FS.createDir config.resultFolder
   let evaluateFilesHandle ← IO.FS.Handle.mk (config.resultFolder ++ "/evaluateFiles.txt") .write
@@ -341,4 +341,35 @@ where
       ]
     String.intercalate "\n" lines
 
-end EvalAuto
+/--
+  Read results generated by `evalTacticsAtMathlibHumanTheorems`
+-/
+def readTacticEvalResult (config : EvalTacticOnMathlibConfig) :
+  CoreM (Array (Name × Array (Name × Array Result))) := do
+  let resultFolder := config.resultFolder
+  if !(← System.FilePath.isDir resultFolder) then
+    throwError "{decl_name%} :: {config.resultFolder} is not a directory"
+  let allPaths ← System.FilePath.walkDir resultFolder
+  let mut ret := #[]
+  for path in allPaths do
+    if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then
+      let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7
+      let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
+      let lines := (← IO.FS.readFile path).splitOn "\n"
+      if lines[3]? != .some "Summary:" || lines[4]? != .some "" then
+        throwError "{decl_name%} :: Format of result file changed, please change analysis code"
+      let lines := (lines.drop 4).filter (fun s => s != "")
+      let lineAnalysis ← (Array.mk lines).mapM analyzeLine
+      ret := ret.push (modName, lineAnalysis)
+  return ret
+where
+  analyzeLine (line : String) : CoreM (Name × Array Result) := do
+    let line := (line.dropWhile (fun c => c != ' ')).drop 3
+    let tr := (line.takeWhile (fun c => c != ']')).splitOn ", "
+    let tr : Array Result ← (Array.mk tr).mapM (fun s => do
+      match Result.ofConcise? s with
+      | .some r => return r
+      | .none => throwError s!"{decl_name%} :: {s} is not a concise representation of a `Result`")
+    let line := (line.dropWhile (fun c => c != ']')).drop 2
+    let name := Name.parseUniqRepr line
+    return (name, tr)