feat(library/tactic/eval): eval_expr for arbitrary expressions

src/library/tactic/eval.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/fresh_name.h"
 #include "kernel/type_checker.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
@@ -14,26 +15,23 @@ namespace lean {
 static vm_obj eval(expr const & A, expr const & a, tactic_state const & s) {
     LEAN_TACTIC_TRY;
     if (has_local(a) || !closed(a))
-        return mk_tactic_exception("invalid eval tactic, expression must be closed", s);
+        return mk_tactic_exception("invalid eval_expr, expression must be closed", s);
     if (is_constant(a)) {
         type_context ctx = mk_type_context_for(s);
         if (!ctx.is_def_eq(A, ctx.infer(a)))
-            return mk_tactic_exception("invalid eval tactic, type mismatch", s);
+            return mk_tactic_exception("invalid eval_expr, type mismatch", s);
         vm_obj r = get_vm_state().get_constant(const_name(a));
         return mk_tactic_success(r, s);
     } else {
-        #if 0
-        environment aux_env = s.env();
-        name eval_aux_name("_eval_aux_expr");
+        vm_state & S = get_vm_state();
+        environment aux_env = S.env();
+        name eval_aux_name = mk_tagged_fresh_name("_eval_expr");
         auto cd = check(aux_env, mk_definition(aux_env, eval_aux_name, {}, A, a, true, false));
         aux_env = aux_env.add(cd);
         aux_env = vm_compile(aux_env, aux_env.get(eval_aux_name));
-        vm_state S(aux_env);
-        vm_obj r = S.get(eval_aux_name);
+        S.update_env(aux_env);
+        vm_obj r = S.get_constant(eval_aux_name);
         return mk_tactic_success(r, s);
-        #else
-        throw exception("invalid eval tactic, only constants are supported at this point");
-        #endif
     }
     LEAN_TACTIC_CATCH(s);
 }

src/library/vm/vm.cpp

@@ -974,6 +974,17 @@ vm_state::vm_state(environment const & env):
     m_bp(0) {
 }
 
+void vm_state::update_env(environment const & env) {
+    lean_assert(env.is_descendant(env));
+    m_env         = env;
+    auto ext      = get_extension(env);
+    m_decl_map    = ext.m_decls;
+    lean_assert(ext.m_next_decl_idx >= m_decl_vector.size());
+    m_decl_vector.resize(ext.m_next_decl_idx);
+    m_fn_name2idx = ext.m_name2idx;
+    lean_assert(is_eqp(m_builtin_cases_map, ext.m_cases));
+}
+
 void vm_state::push_fields(vm_obj const & obj) {
     if (is_constructor(obj)) {
         unsigned nflds = csize(obj);

src/library/vm/vm.h

@@ -540,6 +540,8 @@ public:
 
     environment const & env() const { return m_env; }
 
+    void update_env(environment const & env);
+
     /** \brief Push object into the data stack */
     void push(vm_obj const & o) { m_stack.push_back(o); }
 

tests/lean/eval_expr_error.lean

@@ -1,6 +1,18 @@
 open tactic
 
-meta def tst (A : Type) : tactic unit :=
+meta def tst1 (A : Type) : tactic unit :=
 do  a ← to_expr `(0),
     v ← eval_expr A a,
     return ()
+
+run_command do
+  a ← to_expr `(nat.add),
+  v ← eval_expr nat a,
+  trace v,
+  return ()
+
+run_command do
+  a ← to_expr `(λ x : nat, x + 1),
+  v ← (eval_expr nat a <|> trace "tactic failed" >> return 1),
+  trace v,
+  return ()

tests/lean/eval_expr_error.lean.expected.out

@@ -1 +1,6 @@
 eval_expr_error.lean:5:8: error: invalid eval_expr, type must be a closed expression
+eval_expr_error.lean:8:0: error: invalid eval_expr, type mismatch
+state:
+⊢ true
+tactic failed
+1

tests/lean/run/eval_constant.lean

@@ -4,3 +4,8 @@ run_command do
    e  ← to_expr `(nat.add),
    fn ← eval_expr (nat → nat → nat) e,
    trace (fn 10 20)
+
+run_command do
+   e  ← to_expr `(λ x y : nat, x + x + y),
+   fn ← eval_expr (nat → nat → nat) e,
+   trace (fn 10 20)