From 467ac9d98a3d04c5e2e2edcd863deb984026c36b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jun 2022 16:31:59 -0700
Subject: [PATCH] feat: add support for `CommandElabM` at `#eval`

Note that it does not use `MetaEval` to execute the term of type
`CommandEval`. Thus, we can now use `#eval` to execute simple commands.

see #1256
---
 RELEASES.md                          | 13 ++++++++
 src/Lean/Elab/BuiltinCommand.lean    | 45 +++++++++++++++++++---------
 tests/lean/evalCmd.lean              | 16 ++++++++++
 tests/lean/evalCmd.lean.expected.out |  1 +
 4 files changed, 61 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/evalCmd.lean
 create mode 100644 tests/lean/evalCmd.lean.expected.out

diff --git a/RELEASES.md b/RELEASES.md
index 9bdb0443bb..fb5e11873e 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,19 @@
 Unreleased
 ---------
 
+* Add support for `CommandElabM` monad at `#eval`. Example:
+  ```lean
+  import Lean
+
+  open Lean Elab Command
+
+  #eval do
+    let id := mkIdent `foo
+    elabCommand (← `(def $id := 10))
+
+  #eval foo -- 10
+  ```
+
 * Try to elaborate `do` notation even if the expected type is not available. We still delay elaboration when the expected type
   is not available. This change is particularly useful when writing examples such as
   ```lean
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 63474f773e..07fe39a61b 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Elab.DeclarationRange
 import Lean.DocString
 import Lean.Util.CollectLevelParams
+import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 
@@ -305,14 +306,14 @@ private def mkRunEval (e : Expr) : MetaM Expr := do
 
 unsafe def elabEvalUnsafe : CommandElab
   | `(#eval%$tk $term) => do
-    let n := `_eval
+    let declName := `_eval
     let addAndCompile (value : Expr) : TermElabM Unit := do
       let (value, _) ← Term.levelMVarToParam (← instantiateMVars value)
       let type ← inferType value
       let us := collectLevelParams {} value |>.params
       let value ← instantiateMVars value
       let decl := Declaration.defnDecl {
-        name        := n
+        name        := declName
         levelParams := us.toList
         type        := type
         value       := value
@@ -321,6 +322,7 @@ unsafe def elabEvalUnsafe : CommandElab
       }
       Term.ensureNoUnassignedMVars decl
       addAndCompile decl
+    -- Elaborate `term`
     let elabEvalTerm : TermElabM Expr := do
       let e ← Term.elabTerm term none
       Term.synthesizeSyntheticMVarsNoPostponing
@@ -329,22 +331,37 @@ unsafe def elabEvalUnsafe : CommandElab
         mkDecide e
       else
         return e
-    let elabMetaEval : CommandElabM Unit := runTermElabM (some n) fun _ => do
-      let e ← mkRunMetaEval (← elabEvalTerm)
-      let env ← getEnv
-      let opts ← getOptions
-      let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) n finally setEnv env
-      let (out, res) ← act env opts -- we execute `act` using the environment
-      logInfoAt tk out
-      match res with
-      | Except.error e => throwError e.toString
-      | Except.ok env  => do setEnv env; pure ()
-    let elabEval : CommandElabM Unit := runTermElabM (some n) fun _ => do
+    -- Evaluate using term using `MetaEval` class.
+    let elabMetaEval : CommandElabM Unit := do
+      -- act? is `some act` if elaborated `term` has type `CommandElabM α`
+      let act? ← runTermElabM (some declName) fun _ => do
+        let e ← elabEvalTerm
+        let eType ← instantiateMVars (← inferType e)
+        if eType.isAppOfArity ``CommandElabM 1 then
+          let mut stx ← Term.exprToSyntax e
+          unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
+            stx ← `($stx >>= fun v => IO.println (repr v))
+          let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
+          pure <| some act
+        else
+          let e ← mkRunMetaEval e
+          let env ← getEnv
+          let opts ← getOptions
+          let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
+          let (out, res) ← act env opts -- we execute `act` using the environment
+          logInfoAt tk out
+          match res with
+          | Except.error e => throwError e.toString
+          | Except.ok env  => do setEnv env; pure none
+      let some act := act? | return ()
+      act
+    -- Evaluate using term using `Eval` class.
+    let elabEval : CommandElabM Unit := runTermElabM (some declName) fun _ => do
       -- fall back to non-meta eval if MetaEval hasn't been defined yet
       -- modify e to `runEval e`
       let e ← mkRunEval (← elabEvalTerm)
       let env ← getEnv
-      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) n finally setEnv env
+      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
       let (out, res) ← liftM (m := IO) act
       logInfoAt tk out
       match res with
diff --git a/tests/lean/evalCmd.lean b/tests/lean/evalCmd.lean
new file mode 100644
index 0000000000..84d87aed29
--- /dev/null
+++ b/tests/lean/evalCmd.lean
@@ -0,0 +1,16 @@
+import Lean
+
+open Lean Elab Command
+
+#eval do
+  let id := mkIdent `foo
+  elabCommand (← `(def $id := 10))
+
+example : foo = 10 := rfl
+
+#eval do
+  let id := mkIdent `boo
+  elabCommand (← `(def $id := false))
+  return 5
+
+example : boo = false := rfl
diff --git a/tests/lean/evalCmd.lean.expected.out b/tests/lean/evalCmd.lean.expected.out
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/tests/lean/evalCmd.lean.expected.out
@@ -0,0 +1 @@
+5