feat(library/tactic, frontends/lean/elaborator): add to_expr tactic

library/init/meta/tactic.lean

@@ -133,8 +133,10 @@ meta_constant mk_mapp_core  : transparency → name → list (option expr) → t
    The tactic fails if the given expression is not a local constant. -/
 meta_constant subst         : expr → tactic unit
 meta_constant exact         : expr → tactic unit
-/- Elaborate the given quoted expression with respect to the current main goal. -/
-meta_constant to_expr       : qexpr → tactic expr
+/- Elaborate the given quoted expression with respect to the current main goal.
+   If the boolean argument is tt, then metavariables are tolerated and
+   become new goals. -/
+meta_constant to_expr_core  : bool → qexpr → tactic expr
 /- Return true if the given expression is a type class. -/
 meta_constant is_class      : expr → tactic bool
 /- Try to create an instance of the given type class. -/
@@ -223,6 +225,9 @@ mk_app_core semireducible
 meta_definition mk_mapp : name → list (option expr) → tactic expr :=
 mk_mapp_core semireducible
 
+meta_definition to_expr : qexpr → tactic expr :=
+to_expr_core ff
+
 meta_definition revert (l : expr) : tactic nat :=
 revert_lst [l]
 

src/frontends/lean/elaborator.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/find_fn.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/replace_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
 #include "library/trace.h"
@@ -1343,6 +1344,50 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
     }
 }
 
+// Auxiliary procedure for #translate
+static expr translate_local_name(environment const & env, local_context const & lctx, name const & local_name, expr const & src) {
+    if (auto decl = lctx.get_local_decl_from_user_name(local_name)) {
+        return decl->mk_ref();
+    }
+    if (env.find(local_name)) {
+        if (is_local(src))
+            return mk_constant(local_name);
+        else
+            return src;
+    }
+    throw elaborator_exception(src, format("unknown identifier '") + format(local_name) + format("'"));
+}
+
+/** \brief Translated local constants (and undefined constants) occurring in \c e into
+    local constants provided by \c ctx.
+    Throw exception is \c ctx does not contain the local constant.
+*/
+static expr translate(environment const & env, local_context const & lctx, expr const & e) {
+    auto fn = [&](expr const & e) {
+        if (is_placeholder(e) || is_by(e)) {
+            return some_expr(e); // ignore placeholders
+        } else if (is_constant(e)) {
+            expr new_e = copy_tag(e, translate_local_name(env, lctx, const_name(e), e));
+            return some_expr(new_e);
+        } else if (is_local(e)) {
+            expr new_e = copy_tag(e, translate_local_name(env, lctx, local_pp_name(e), e));
+            return some_expr(new_e);
+        } else {
+            return none_expr();
+        }
+    };
+    return replace(e, fn);
+}
+
+expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+                      expr const & e, bool relaxed) {
+    std::tuple<expr, level_param_names> p = elaborate(env, opts, mctx, lctx, translate(env, lctx, e), !relaxed);
+    if (std::get<1>(p)) {
+        throw exception("nested elaboration failed, new universe parameters have been created");
+    }
+    return std::get<0>(p);
+}
+
 void elaborator::invoke_tactics(checkpoint const & C) {
     buffer<expr_pair> to_process;
     list<expr_pair> old_stack = C.m_saved_tactic_stack;
@@ -1353,6 +1398,8 @@ void elaborator::invoke_tactics(checkpoint const & C) {
     if (to_process.empty()) return;
     unassigned_uvars_to_params();
 
+    scope_elaborate_fn scope(nested_elaborate);
+
     unsigned i = to_process.size();
     while (i > 0) {
         --i;

src/frontends/lean/elaborator.h

@@ -212,6 +212,9 @@ public:
 std::tuple<expr, level_param_names> elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                                               expr const & e, bool check_unassigend);
 
+expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+                      expr const & e, bool relaxed);
+
 void initialize_elaborator();
 void finalize_elaborator();
 }

src/frontends/lean/old_elaborator.cpp

@@ -49,6 +49,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/tactic_state.h"
+#include "frontends/lean/elaborator.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/info_manager.h"
@@ -1682,6 +1683,8 @@ static tactic_state to_tactic_state(environment const & env, options const & opt
 }
 
 optional<tactic_state> old_elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar) {
+    scope_elaborate_fn scope(nested_elaborate);
+
     name tactic_name("_tactic");
     expr tactic_type = ::lean::mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit"));
     /* compile tactic */

src/library/tactic/elaborate.cpp

@@ -5,6 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/annotation.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/elaborate.h"
+#include "library/tactic/tactic_state.h"
 
 namespace lean {
 static name * g_by_name = nullptr;
@@ -13,10 +16,39 @@ expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
 bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
 expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
 
+LEAN_THREAD_PTR(elaborate_fn const, g_elaborate);
+
+scope_elaborate_fn::scope_elaborate_fn(elaborate_fn const & fn) {
+    m_old = g_elaborate;
+    g_elaborate = &fn;
+}
+
+scope_elaborate_fn::~scope_elaborate_fn() {
+    g_elaborate = m_old;
+}
+
+vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj const & _s) {
+    tactic_state const & s = to_tactic_state(_s);
+    optional<metavar_decl> g = s.get_main_goal_decl();
+    if (!g) return mk_no_goals_exception(s);
+    if (!g_elaborate) {
+        return mk_tactic_exception("elaborator is not available", s);
+    }
+    metavar_context mctx = s.mctx();
+    try {
+        expr r = (*g_elaborate)(s.env(), s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed));
+        return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 void initialize_elaborate() {
     g_by_name           = new name("by");
     register_annotation(*g_by_name);
+    DECLARE_VM_BUILTIN(name({"tactic", "to_expr_core"}), tactic_to_expr_core);
 }
+
 void finalize_elaborate() {
     delete g_by_name;
 }

src/library/tactic/elaborate.h

@@ -6,12 +6,27 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
+#include "library/metavar_context.h"
 
 namespace lean {
 expr mk_by(expr const & e);
 bool is_by(expr const & e);
 expr const & get_by_arg(expr const & e);
 
+/* Elaboration function.
+   \remark The boolean flag indicates whether metavariables should be tolerated in the result or not.
+   \remark The metavariable context is input/output. */
+typedef std::function<expr(environment const &, options const &, metavar_context &, local_context const &, expr const &, bool)> elaborate_fn;
+
+/** \brief Auxiliary function for setting the thread local elaboration
+    procedure used by the tactic framework. */
+class scope_elaborate_fn {
+    elaborate_fn const * m_old;
+public:
+    scope_elaborate_fn(elaborate_fn const &);
+    ~scope_elaborate_fn();
+};
+
 void initialize_elaborate();
 void finalize_elaborate();
 }

src/library/tactic/tactic_state.cpp

@@ -356,11 +356,6 @@ vm_obj tactic_local_context(vm_obj const & s0) {
     return mk_tactic_success(to_obj(to_list(r)), s);
 }
 
-vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & s) {
-    /* TODO(Leo): invoke elaborator */
-    return mk_tactic_success(qe, to_tactic_state(s));
-}
-
 vm_obj rotate_left(unsigned n, tactic_state const & s) {
     buffer<expr> gs;
     to_buffer(s.goals(), gs);
@@ -479,7 +474,6 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}),           tactic_unify_core);
     DECLARE_VM_BUILTIN(name({"tactic", "get_local"}),            tactic_get_local);
     DECLARE_VM_BUILTIN(name({"tactic", "local_context"}),        tactic_local_context);
-    DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}),              tactic_to_expr);
     DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}),          tactic_rotate_left);
     DECLARE_VM_BUILTIN(name({"tactic", "get_goals"}),            tactic_get_goals);
     DECLARE_VM_BUILTIN(name({"tactic", "set_goals"}),            tactic_set_goals);

tests/lean/qexpr1.lean

@@ -0,0 +1,17 @@
+open tactic
+
+set_option pp.all true
+
+example (a b c : nat) : true :=
+by do
+  x ← to_expr `(a + b),
+  trace x, infer_type x >>= trace,
+  constructor
+
+example (a b c : nat) : true :=
+by do
+  x ← get_local `a,
+  x ← mk_app `nat.succ [x],
+  r ← to_expr `(%%x + b),
+  trace r, infer_type r >>= trace,
+  constructor

tests/lean/qexpr1.lean.expected.out

@@ -0,0 +1,4 @@
+@add.{1} nat nat_has_add a b
+nat
+@add.{1} nat nat_has_add (nat.succ a) b
+nat