test code for previous works

Auto/EvaluateAuto/CommandAnalysis.lean

@@ -0,0 +1,96 @@
+import Lean
+import Auto.EvaluateAuto.EnvAnalysis
+import Auto.EvaluateAuto.Result
+open Lean
+
+namespace EvalAuto
+
+open Elab Frontend
+def runWithEffectOfCommandsCore
+  (cnt? : Option Nat)
+  (action : Context → State → State → ConstantInfo → IO (Option α)) : FrontendM (Array α) := do
+  let mut done := false
+  let mut ret := #[]
+  let mut cnt := 0
+  while !done do
+    if cnt?.isSome && cnt >= cnt?.getD 0 then
+      break
+    let prev ← get
+    done ← Frontend.processCommand
+    let post ← get
+    let newConsts := Environment.newLocalConstants prev.commandState.env post.commandState.env
+    for newConst in newConsts do
+      if let .some result ← action (← read) prev post newConst then
+        cnt := cnt + 1
+        ret := ret.push result
+        if cnt?.isSome && cnt >= cnt?.getD 0 then
+          break
+  return ret
+
+/--
+  Given a Lean4 file `fileName` with content `input` consisting of
+  a header and a series of commands, first parse the header. Then,
+  for each command `cmd`, record the states `st₁, st₂` before and
+  after executing the command, and run `action` on the `ConstantInfo`s produced
+  by `cmd`, together with `st₁, st₂` and the `InputContext`.\
+  An additional `cnt?` can be supplied to control termination.
+  When the number of times `action` returns `.some _` reaches `cnt?`,
+  the procedure is terminated.
+-/
+def runWithEffectOfCommands
+  (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat)
+  (action : Context → State → State → ConstantInfo → IO (Option α)) : IO (Array α) := do
+  let inputCtx := Parser.mkInputContext input fileName
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, messages) ← processHeader header opts messages inputCtx
+  let commandState := Command.mkState env messages opts
+  (runWithEffectOfCommandsCore cnt? action { inputCtx }).run'
+    { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
+
+open Elab Tactic in
+/--
+  Note: Use `initSrcSearchPath` to get SearchPath of Lean4's builtin source files
+-/
+def runTacticAtConstantDeclaration
+  (name : Name) (searchPath : SearchPath)
+  (tactic : ConstantInfo → TacticM Unit) : CoreM Result := do
+  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 ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci =>
+    let metaAction : MetaM (Option Result) := do
+      if ci.name != name then
+        return .none
+      let .mvar mid ← Meta.mkFreshExprMVar ci.type
+        | throwError "{decl_name%} :: Unexpected error"
+      let result : List MVarId ⊕ Exception ←
+        tryCatchRuntimeEx
+          (do let goals ← Term.TermElabM.run' (Tactic.run mid (tactic ci)) {}; return .inl goals)
+          (fun e => return .inr e)
+      match result with
+      | .inl goals =>
+        if goals.length >= 1 then
+          return .some .subGoals
+        let proof ← instantiateMVars (.mvar mid)
+        match Kernel.check (← getEnv) {} proof with
+        | Except.ok autoProofType =>
+          match Kernel.isDefEq (← getEnv) {} autoProofType ci.type with
+          | Except.ok true => return .some .success
+          | _ => return .some .typeUnequal
+        | Except.error _ => return .some .typeCheckFail
+      | .inr e => return .some (.exception e)
+    let coreAction : CoreM (Option Result) := metaAction.run'
+    let ioAction : IO (Option Result × _) := coreAction.toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
+    do
+      return (← ioAction).fst)
+  let #[result] := results
+    | throwError "{decl_name%} :: Unexpected error"
+  return result
+
+end EvalAuto

Auto/EvaluateAuto/ConstAnalysis.lean

@@ -50,6 +50,17 @@ def allHumanTheorems : CoreM (Array Name) := do
   let allHumanTheorems ← allConsts.filterM Name.isHumanTheorem
   return Array.mk allHumanTheorems
 
+def Name.isFromPackage (name : Name) (pkgPrefix : String) : CoreM Bool := do
+  let .some mod ← Lean.findModuleOf? name
+    | throwError "{decl_name%} :: Cannot find {name}"
+  return mod.components[0]? == .some (.str .anonymous pkgPrefix)
+
+def allHumanTheoremsFromPackage (pkgPrefix : String) : CoreM (Array Name) := do
+  let allConsts := (← getEnv).constants.toList.map Prod.fst
+  let allHumanTheoremsFromPackage ← allConsts.filterM (fun n =>
+    return (← Name.isHumanTheorem n) && (← Name.isFromPackage n pkgPrefix))
+  return Array.mk allHumanTheoremsFromPackage
+
 /-- Return the theorems that occurs in an expression -/
 def Expr.getUsedTheorems (e : Expr) : CoreM (Array Name) :=
   e.getUsedConstants.filterM Name.isTheorem

Auto/EvaluateAuto/EnvAnalysis.lean

@@ -4,6 +4,15 @@ open Lean
 
 namespace EvalAuto
 
+/--
+  Suppose `env₂` is the environment after running several non-import
+  commands starting from `env₁`, then `Environment.newLocalConstants env₁ env₂`
+  returns the new `ConstantInfo`s added by these commands
+-/
+def Environment.newLocalConstants (env₁ env₂ : Environment) :=
+  env₂.constants.map₂.toArray.filterMap (fun (name, ci) =>
+    if !env₁.constants.map₂.contains name then .some ci else .none)
+
 def mathlibModules : CoreM (Array Name) := do
   let u := (← getEnv).header.moduleNames
   return u.filter (fun name => name.components[0]? == .some `Mathlib)

Auto/EvaluateAuto/Result.lean

@@ -0,0 +1,32 @@
+import Lean
+open Lean
+
+namespace EvalAuto
+
+inductive Result
+  | success
+  | nonProp
+  | typeCheckFail
+  | typeUnequal
+  -- `auto` does not produce subgoals, but other tactics we test might (such as `simp`)
+  | subGoals
+  | exception (e : Exception)
+
+instance : ToMessageData Result where
+  toMessageData : Result → MessageData
+  | .success         => "Result.success"
+  | .nonProp         => "Result.nonProp"
+  | .typeCheckFail   => "Result.typeCheckFail"
+  | .typeUnequal     => "Result.typeUnequal"
+  | .subGoals        => "Result.subGoals"
+  | .exception e     => m!"Result.exception ::\n{e.toMessageData}"
+
+def Result.concise : Result → String
+| .success => "S"
+| .nonProp => "N"
+| .typeCheckFail => "F"
+| .typeUnequal => "U"
+| .subGoals => "G"
+| .exception _ => "E"
+
+end EvalAuto

Auto/EvaluateAuto/TestCode.lean

@@ -1,7 +1,9 @@
 import Lean
+import Auto.EvaluateAuto.Result
 import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.EnvAnalysis
 import Auto.EvaluateAuto.NameArr
+import Auto.EvaluateAuto.CommandAnalysis
 import Auto.Tactic
 
 open Lean Auto
@@ -13,28 +15,6 @@ initialize
 
 namespace EvalAuto
 
-inductive Result
-  | success
-  | nonProp
-  | typeCheckFail
-  | typeUnequal
-  | autoException (e : Exception)
-
-instance : ToMessageData Result where
-  toMessageData : Result → MessageData
-  | .success         => "Result.success"
-  | .nonProp         => "Result.nonProp"
-  | .typeCheckFail   => "Result.typeCheckFail"
-  | .typeUnequal     => "Result.typeUnequal"
-  | .autoException e => m!"Result.autoException ::\n{e.toMessageData}"
-
-def Result.concise : Result → String
-| .success => "S"
-| .nonProp => "N"
-| .typeCheckFail => "F"
-| .typeUnequal => "U"
-| .autoException _ => "E"
-
 inductive SolverConfig where
   | native
   | leanSmt
@@ -102,7 +82,7 @@ private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : Co
       | Except.ok true => return .success
       | _ => return .typeUnequal
     | Except.error _ => return .typeCheckFail
-  | .inr e => return .autoException e
+  | .inr e => return .exception e
 
 /--
   Run `Lean-auto` on the type of ``name``, using premises collected