more code for evaluating tactics

Auto/EvaluateAuto/CommandAnalysis.lean

@@ -57,77 +57,16 @@ def runWithEffectOfCommandsCore
   the procedure is terminated.
 -/
 def runWithEffectOfCommands
-  (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat)
+  (input : String) (fileName : String) (cnt? : Option Nat)
   (action : Context → State → State → ConstantInfo → IO (Option α)) : CoreM (Array α) := do
   let inputCtx := Parser.mkInputContext input fileName
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let mut ensuring := #[]
   if auto.evalAuto.ensureAesop.get (← getOptions) then
     ensuring := ensuring.push { module := `Aesop }
-  let (env, messages) ← processHeaderEnsuring header opts messages inputCtx (ensuring := ensuring)
-  let commandState := Command.mkState env messages opts
+  let (env, messages) ← processHeaderEnsuring header {} messages inputCtx (ensuring := ensuring)
+  let commandState := Command.mkState env messages {}
   (runWithEffectOfCommandsCore cnt? action { inputCtx }).run'
     { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
 
-open Tactic in
-/--
-  Use `runWithEffectOfCommands` to run tactics at the place just before
-  the command that created the constant `name`\
-  Note: Use `initSrcSearchPath` to get SearchPath of source files
--/
-def runTacticsAtConstantDeclaration
-  (name : Name) (searchPath : SearchPath)
-  (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do
-  if ← isInitializerExecutionEnabled then
-    throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe"
-  let .some modName ← Lean.findModuleOf? name
-    | throwError "{decl_name%} :: Cannot find constant {name}"
-  let .some uri ← Server.documentUriFromModule searchPath modName
-    | throwError "{decl_name%} :: Cannot find module {modName}"
-  let .some path := System.Uri.fileUriToPath? uri
-    | throwError "{decl_name%} :: URI {uri} of {modName} is not a file"
-  let path := path.normalize
-  let inputHandle ← IO.FS.Handle.mk path .read
-  let input ← inputHandle.readToEnd
-  let results : Array (Array Result) ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci => do
-    if name != ci.name then
-      return .none
-    let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result :=
-      Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci)
-    let coreAction tactic : CoreM Result := (metaAction tactic).run'
-    let ioAction tactic : IO (Result × _) :=
-      (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
-    let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic)
-    return .some (resultsWithState.map Prod.fst))
-  let #[result] := results
-    | throwError "{decl_name%} :: Unexpected error"
-  return result
-
-open Tactic in
-/--
-  Effectively, `runTacticsAtConstantDeclaration` at each constant of the module `modName`\
-  Note: Use `initSrcSearchPath` to get SearchPath of source files
--/
-def runTacticsAtModule
-  (modName : Name) (searchPath : SearchPath)
-  (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do
-  let .some uri ← Server.documentUriFromModule searchPath modName
-    | throwError "{decl_name%} :: Cannot find module {modName}"
-  let .some path := System.Uri.fileUriToPath? uri
-    | throwError "{decl_name%} :: URI {uri} of {modName} is not a file"
-  let path := path.normalize
-  let inputHandle ← IO.FS.Handle.mk path .read
-  let input ← inputHandle.readToEnd
-  let results : Array (Array Result) ← runWithEffectOfCommands input path.toString {} .none (fun ctx st₁ st₂ ci => do
-    let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result :=
-      Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci)
-    let coreAction tactic : CoreM Result := (metaAction tactic).run'
-    let ioAction tactic : IO (Result × _) :=
-      (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
-    let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic)
-    return .some (resultsWithState.map Prod.fst))
-  let #[result] := results
-    | throwError "{decl_name%} :: Unexpected error"
-  return result
-
 end EvalAuto

Auto/EvaluateAuto/Result.lean

@@ -1,6 +1,11 @@
 import Lean
 open Lean
 
+initialize
+  registerTraceClass `auto.eval.printConfig
+  registerTraceClass `auto.eval.printProblem
+  registerTraceClass `auto.eval.printResult
+
 namespace EvalAuto
 
 inductive Result

Auto/EvaluateAuto/TestAuto.lean

@@ -7,11 +7,6 @@ import Auto.Tactic
 
 open Lean Auto
 
-initialize
-  registerTraceClass `auto.eval.printConfig
-  registerTraceClass `auto.eval.printProblem
-  registerTraceClass `auto.eval.printResult
-
 namespace EvalAuto
 
 inductive SolverConfig where
@@ -27,7 +22,7 @@ instance : ToString SolverConfig where
   | .smt sn       => s!"smt {sn}"
   | .tptp sn path => s!"tptp {sn} {path}"
 
-structure EvalConfig where
+structure EvalAutoConfig where
   /-- Timeout for Lean code (Lean-auto + native provers) -/
   maxHeartbeats : Nat           := 65536
   /-- Timeout for external provers, i.e. TPTP solvers and SMT solvers -/
@@ -37,15 +32,15 @@ structure EvalConfig where
   /-- Optional logfile for saving the result of the evaluation -/
   logFile       : Option String := .none
 
-instance : ToString EvalConfig where
-  toString : EvalConfig → String
+instance : ToString EvalAutoConfig where
+  toString : EvalAutoConfig → String
   | ⟨maxHeartbeats, timeout, solverConfig, logFile⟩ =>
     let logFileStr :=
       match logFile with
       | .some logFile => s!", logFile := {logFile}"
       | .none => ""
     s!"\{maxHeartbeats := {maxHeartbeats}, timeout := {timeout}, " ++
-    s!"solverConfig = {solverConfig}{logFileStr}}"
+    s!"solverConfig := {solverConfig}{logFileStr}}"
 
 /--
   Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof`
@@ -105,17 +100,17 @@ def disableAllSolvers (o : Options) : Options :=
   let o := auto.tptp.set o false
   o
 
-def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := do
-  let logFileHandle : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
+def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit := do
+  let logFileHandle? : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
   trace[auto.eval.printConfig] m!"Config = {config}"
-  if let .some fhandle := logFileHandle then
+  if let .some fhandle := logFileHandle? then
     fhandle.putStrLn s!"Config = {config}"
   let startTime ← IO.monoMsNow
   let mut results := #[]
   for name in names do
     let ci ← Name.getCi name decl_name%
     trace[auto.eval.printProblem] m!"Testing || {name} : {ci.type}"
-    if let .some fhandle := logFileHandle then
+    if let .some fhandle := logFileHandle? then
       fhandle.putStrLn ""
       fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}"
     let result : Result ← withCurrHeartbeats <|
@@ -154,16 +149,16 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d
               runAutoOnConst name
     trace[auto.eval.printResult] m!"{result}"
     results := results.push result
-    if let .some fhandle := logFileHandle then
+    if let .some fhandle := logFileHandle? then
       fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
-  if let .some fhandle := logFileHandle then
+  if let .some fhandle := logFileHandle? then
     fhandle.putStrLn ""
     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}"
 
-def runAutoOnNamesFile (cfg : EvalConfig) (fname : String) : CoreM Unit := do
+def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do
   let names ← NameArray.load fname
   runAutoOnConsts cfg names
 

Auto/EvaluateAuto/TestTactics.lean

@@ -8,9 +8,9 @@ open Lean
 
 namespace EvalAuto
 
-section Tactics
+open Elab Tactic
 
-  open Elab Tactic
+section Tactics
 
   def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl))
 
@@ -74,6 +74,136 @@ section Tactics
             Syntax.atom synth ")"
         ]
 
+  inductive RegisteredTactic where
+    | useRfl
+    | useSimp
+    | useSimpAll
+    | useSimpAllWithPremises
+    | useAesop
+    | useAesopWithPremises
+
+  instance : ToString RegisteredTactic where
+    toString : RegisteredTactic → String
+    | .useRfl                 => "useRfl"
+    | .useSimp                => "useSimp"
+    | .useSimpAll             => "useSimpAll"
+    | .useSimpAllWithPremises => "useSimpAllWithPremises"
+    | .useAesop               => "useAesop"
+    | .useAesopWithPremises   => "useAesopWithPremises"
+
+  def RegisteredTactic.toCiTactic : RegisteredTactic → ConstantInfo → TacticM Unit
+    | .useRfl                 => fun _ => EvalAuto.useRfl
+    | .useSimp                => fun _ => EvalAuto.useSimp
+    | .useSimpAll             => fun _ => EvalAuto.useSimpAll
+    | .useSimpAllWithPremises => EvalAuto.useSimpAllWithPremises
+    | .useAesop               => fun _ => EvalAuto.useAesop
+    | .useAesopWithPremises   => EvalAuto.useAesopWithPremises
+
 end Tactics
 
+/--
+  Use `runWithEffectOfCommands` to run tactics at the place just before
+  the command that created the constant `name`\
+  Note: Use `initSrcSearchPath` to get SearchPath of source files
+-/
+def runTacticsAtConstantDeclaration
+  (name : Name) (searchPath : SearchPath)
+  (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do
+  if ← isInitializerExecutionEnabled then
+    throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe"
+  let .some modName ← Lean.findModuleOf? name
+    | throwError "{decl_name%} :: Cannot find constant {name}"
+  let .some uri ← Server.documentUriFromModule searchPath modName
+    | throwError "{decl_name%} :: Cannot find module {modName}"
+  let .some path := System.Uri.fileUriToPath? uri
+    | throwError "{decl_name%} :: URI {uri} of {modName} is not a file"
+  let path := path.normalize
+  let inputHandle ← IO.FS.Handle.mk path .read
+  let input ← inputHandle.readToEnd
+  let results : Array (Array Result) ← runWithEffectOfCommands input path.toString (.some 1) (fun ctx st₁ st₂ ci => do
+    if name != ci.name then
+      return .none
+    let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result :=
+      Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci)
+    let coreAction tactic : CoreM Result := (metaAction tactic).run'
+    let ioAction tactic : IO (Result × _) :=
+      (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
+    let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic)
+    return .some (resultsWithState.map Prod.fst))
+  let #[result] := results
+    | throwError "{decl_name%} :: Unexpected error"
+  return result
+
+structure EvalTacticConfig where
+  /-- Timeout for each tactic -/
+  maxHeartbeats : Nat           := 65536
+  /-- Tactics to run at each constant declaration -/
+  tactics       : Array RegisteredTactic
+  /-- Optional logfile for saving the result of the evaluation -/
+  logFile       : Option String := .none
+
+instance : ToString EvalTacticConfig where
+  toString : EvalTacticConfig → String
+  | ⟨maxHeartbeats, tactics, logFile⟩ =>
+    let logFileStr :=
+      match logFile with
+      | .some logFile => s!", logFile := {logFile}"
+      | .none => ""
+    s!"\{maxHeartbeats := {maxHeartbeats}, tactics := {tactics}{logFileStr}}"
+
+/--
+  Effectively `runTacticsAtConstantDeclaration` at each constant in `modName` which satisfies `filter`\
+  Note: Use `initSrcSearchPath` to get SearchPath of source files
+-/
+def evalAtModule
+  (modName : Name) (searchPath : SearchPath) (filter : ConstantInfo → Bool)
+  (config : EvalTacticConfig) : CoreM Unit:= do
+  let logFileHandle? : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
+  trace[auto.eval.printConfig] m!"Config = {config}"
+  if let .some fhandle := logFileHandle? then
+    fhandle.putStrLn s!"Config = {config}"
+  let .some uri ← Server.documentUriFromModule searchPath modName
+    | throwError "{decl_name%} :: Cannot find module {modName}"
+  let .some path := System.Uri.fileUriToPath? uri
+    | throwError "{decl_name%} :: URI {uri} of {modName} is not a file"
+  let path := path.normalize
+  let inputHandle ← IO.FS.Handle.mk path .read
+  let input ← inputHandle.readToEnd
+  let startTime ← IO.monoMsNow
+  let results ← runWithEffectOfCommands input path.toString .none (fun ctx st₁ st₂ ci => do
+    if filter ci then
+      let result ← evalAction
+        {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
+        ci logFileHandle? config
+      return .some (ci.name, result)
+    else
+      return .none)
+  if let .some fhandle := logFileHandle? then
+    fhandle.putStrLn ""
+    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}"
+where
+  evalAction
+    (context : Core.Context) (state : Core.State) (ci : ConstantInfo)
+    (logFileHandle? : Option IO.FS.Handle) (config : EvalTacticConfig) : IO (Array Result) := do
+  config.tactics.zipWithIndex.mapM (fun (tactic, idx) => do
+    let metaAction : MetaM Result :=
+      Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic.toCiTactic ci)
+    let coreAction : CoreM Result := (do
+      trace[auto.eval.printProblem] m!"Testing tactic {idx} || {ci.name} : {ci.type}"
+      if let .some fhandle := logFileHandle? then
+        fhandle.putStrLn ""
+        fhandle.putStrLn s!"Testing tactic {idx} || {ci.name} : {← (Lean.Meta.ppExpr ci.type).run'}"
+      let result ← withCurrHeartbeats <|
+        withReader (fun ctx => { ctx with maxHeartbeats := config.maxHeartbeats * 1000 }) <|
+          Meta.MetaM.run' metaAction
+      trace[auto.eval.printResult] m!"{result}"
+      if let .some fhandle := logFileHandle? then
+        fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
+      return result)
+    let (result, _) ← coreAction.toIO context state
+    return result)
+
 end EvalAuto