feat(frontends/lean): add run_tactic command

This commit also adds the tactic `add_decl`.

library/init/meta/tactic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.trace init.function init.option init.monad init.alternative init.meta.exceptional
-import init.meta.format init.meta.environment init.meta.pexpr
+import init.trace init.function init.option init.monad init.alternative init.nat_div
+import init.meta.exceptional init.meta.format init.meta.environment init.meta.pexpr
 meta_constant tactic_state : Type₁
 
 namespace tactic_state
@@ -315,6 +315,8 @@ meta_constant cases_core     : transparency → expr → list name → tactic un
 meta_constant generalize_core : transparency → expr → name → tactic unit
 /- instantiate assigned metavariables in the given expression -/
 meta_constant instantiate_mvars : expr → tactic expr
+/- Add the given declaration to the environment -/
+meta_constant add_decl : declaration → tactic unit
 open list nat
 
 /- Add (H : T := pr) to the current goal -/
@@ -608,4 +610,11 @@ meta_definition refine (e : pexpr) : tactic unit :=
 do tgt : expr ← target,
    to_expr_core tt `((%%e : %%tgt)) >>= exact
 
+meta_definition expr_of_nat (n : ℕ) : tactic expr :=
+if n = 0 then to_expr `(0)
+else if n = 1 then to_expr `(1)
+else do
+r : expr ← expr_of_nat (n / 2),
+if n % 2 = 0 then to_expr `(bit0 %%r)
+else to_expr `(bit1 %%r)
 end tactic

src/emacs/lean-syntax.el

@@ -21,7 +21,7 @@
     "instances" "coercions" "attributes" "raw" "migrate" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
     "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from" "aliases" "register_simp_ext"
-    "mutual_definition" "mutual_meta_definition" "mutual_inductive" "def" "mutual_def")
+    "mutual_definition" "mutual_meta_definition" "mutual_inductive" "def" "mutual_def" "run_tactic")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))

src/frontends/lean/builtin_cmds.cpp

@@ -30,10 +30,12 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/legacy_type_context.h"
 #include "library/reducible.h"
+#include "library/typed_expr.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/kabstract.h"
+#include "library/tactic/elaborate.h"
 #include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
 #include "library/tactic/defeq_simplifier/defeq_simplifier.h"
 #include "library/tactic/simplifier/simp_extensions.h"
@@ -42,6 +44,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/calc.h"
 #include "frontends/lean/notation_cmd.h"
+#include "frontends/lean/elaborator.h"
 #include "frontends/lean/inductive_cmds.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/print_cmd.h"
@@ -561,6 +564,20 @@ environment add_key_equivalence_cmd(parser & p) {
     return add_key_equivalence(p.env(), h1, h2);
 }
 
+static environment run_tactic_cmd(parser & p) {
+    /* initial state for executing the tactic */
+    environment env      = p.env();
+    options opts         = p.get_options();
+    metavar_context mctx;
+    expr tactic          = p.parse_expr();
+    expr try_constructor = mk_app(mk_constant(get_tactic_try_name()), mk_constant(get_tactic_constructor_name()));
+    tactic               = mk_app(mk_constant(get_monad_and_then_name()), tactic, try_constructor);
+    expr val             = mk_typed_expr(mk_true(), mk_by(tactic));
+    bool check_unassigned = false;
+    elaborate(env, opts, mctx, local_context(), val, check_unassigned);
+    return env;
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",              "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -582,6 +599,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("declare_trace",     "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd));
     add_cmd(r, cmd_info("register_simp_ext", "register simplifier extension", register_simp_ext_cmd));
     add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd));
+    add_cmd(r, cmd_info("run_tactic",        "execute a tactic at top-level", run_tactic_cmd));
     add_cmd(r, cmd_info("#erase_cache",      "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#unify",            "(for debugging purposes)", unify_cmd));
     add_cmd(r, cmd_info("#compile",          "(for debugging purposes)", compile_cmd));

src/frontends/lean/elaborator.cpp

@@ -36,6 +36,7 @@ Author: Leonardo de Moura
 #include "library/tactic/elaborate.h"
 #include "library/equations_compiler/compiler.h"
 #include "frontends/lean/builtin_exprs.h"
+#include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/info_annotation.h"
@@ -1115,10 +1116,6 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
         return visit_app_core(fn, args, expected_type, e);
 }
 
-static expr mk_tactic_unit() {
-    return mk_app(mk_constant(get_tactic_name(), {mk_level_one()}), mk_constant(get_unit_name()));
-}
-
 expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type) {
     lean_assert(is_by(e));
     expr tac;
@@ -1665,7 +1662,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
             throw_unsolved_tactic_state(*new_s, "tactic failed, result contains meta-variables", ref);
         }
         mctx.assign(mvar, val);
-        // TODO(Leo): should we update the environment?!?
+        m_env = new_s->env();
         m_ctx.set_mctx(mctx);
     } else if (optional<pair<format, tactic_state>> ex = is_tactic_exception(S, m_opts, r)) {
         throw_unsolved_tactic_state(ex->second, ex->first, ref);
@@ -1967,13 +1964,14 @@ pair<expr, level_param_names> elaborator::finalize(expr const & e, bool check_un
 }
 
 pair<expr, level_param_names>
-elaborate(environment const & env, options const & opts,
+elaborate(environment & env, options const & opts,
           metavar_context & mctx, local_context const & lctx, expr const & e,
           bool check_unassigned) {
     elaborator elab(env, opts, mctx, lctx);
     expr r = elab.elaborate(e);
     auto p = elab.finalize(r, check_unassigned, true);
     mctx = elab.mctx();
+    env  = elab.env();
     return p;
 }
 

src/frontends/lean/elaborator.h

@@ -239,7 +239,7 @@ public:
     };
 };
 
-pair<expr, level_param_names> elaborate(environment const & env, options const & opts,
+pair<expr, level_param_names> elaborate(environment & env, options const & opts,
                                         metavar_context & mctx, local_context const & lctx,
                                         expr const & e, bool check_unassigend);
 

src/frontends/lean/token_table.cpp

@@ -115,9 +115,9 @@ void init_token_table(token_table & t) {
          "exit", "set_option", "open", "export", "override", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic",
          "multiple_instances", "find_decl", "attribute", "persistent",
-         "mutual_inductive",
-         "include", "omit", "migrate", "init_quotient", "init_hits", "declare_trace", "register_simp_ext",
-         "add_key_equivalence", "#erase_cache",
+         "mutual_inductive", "include", "omit", "migrate",
+         "init_quotient", "init_hits", "declare_trace", "register_simp_ext",
+         "run_tactic", "add_key_equivalence", "#erase_cache",
          "#compile", "#unify", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/frontends/lean/util.cpp

@@ -414,4 +414,8 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg) {
     }
     return mk_pair(id, decl_it->second.kind());
 }
+
+expr mk_tactic_unit() {
+    return mk_app(mk_constant(get_tactic_name(), {mk_level_one()}), mk_constant(get_unit_name()));
+}
 }

src/frontends/lean/util.h

@@ -113,4 +113,7 @@ expr elim_choice_num(expr const & e);
 
 /** \brief Parse option name */
 pair<name, option_kind> parse_option_name(parser & p, char const * error_msg);
+
+/** Create (tactic unit) type */
+expr mk_tactic_unit();
 }

src/library/constants.cpp

@@ -153,6 +153,7 @@ name const * g_monad = nullptr;
 name const * g_monad_map = nullptr;
 name const * g_monad_bind = nullptr;
 name const * g_monad_ret = nullptr;
+name const * g_monad_and_then = nullptr;
 name const * g_monadIO = nullptr;
 name const * g_monoid = nullptr;
 name const * g_mul = nullptr;
@@ -307,6 +308,8 @@ name const * g_subtype_tag = nullptr;
 name const * g_subtype_elt_of = nullptr;
 name const * g_subtype_rec = nullptr;
 name const * g_tactic = nullptr;
+name const * g_tactic_try = nullptr;
+name const * g_tactic_constructor = nullptr;
 name const * g_to_string = nullptr;
 name const * g_to_int = nullptr;
 name const * g_to_real = nullptr;
@@ -478,6 +481,7 @@ void initialize_constants() {
     g_monad_map = new name{"monad", "map"};
     g_monad_bind = new name{"monad", "bind"};
     g_monad_ret = new name{"monad", "ret"};
+    g_monad_and_then = new name{"monad", "and_then"};
     g_monadIO = new name{"monadIO"};
     g_monoid = new name{"monoid"};
     g_mul = new name{"mul"};
@@ -632,6 +636,8 @@ void initialize_constants() {
     g_subtype_elt_of = new name{"subtype", "elt_of"};
     g_subtype_rec = new name{"subtype", "rec"};
     g_tactic = new name{"tactic"};
+    g_tactic_try = new name{"tactic", "try"};
+    g_tactic_constructor = new name{"tactic", "constructor"};
     g_to_string = new name{"to_string"};
     g_to_int = new name{"to_int"};
     g_to_real = new name{"to_real"};
@@ -804,6 +810,7 @@ void finalize_constants() {
     delete g_monad_map;
     delete g_monad_bind;
     delete g_monad_ret;
+    delete g_monad_and_then;
     delete g_monadIO;
     delete g_monoid;
     delete g_mul;
@@ -958,6 +965,8 @@ void finalize_constants() {
     delete g_subtype_elt_of;
     delete g_subtype_rec;
     delete g_tactic;
+    delete g_tactic_try;
+    delete g_tactic_constructor;
     delete g_to_string;
     delete g_to_int;
     delete g_to_real;
@@ -1129,6 +1138,7 @@ name const & get_monad_name() { return *g_monad; }
 name const & get_monad_map_name() { return *g_monad_map; }
 name const & get_monad_bind_name() { return *g_monad_bind; }
 name const & get_monad_ret_name() { return *g_monad_ret; }
+name const & get_monad_and_then_name() { return *g_monad_and_then; }
 name const & get_monadIO_name() { return *g_monadIO; }
 name const & get_monoid_name() { return *g_monoid; }
 name const & get_mul_name() { return *g_mul; }
@@ -1283,6 +1293,8 @@ name const & get_subtype_tag_name() { return *g_subtype_tag; }
 name const & get_subtype_elt_of_name() { return *g_subtype_elt_of; }
 name const & get_subtype_rec_name() { return *g_subtype_rec; }
 name const & get_tactic_name() { return *g_tactic; }
+name const & get_tactic_try_name() { return *g_tactic_try; }
+name const & get_tactic_constructor_name() { return *g_tactic_constructor; }
 name const & get_to_string_name() { return *g_to_string; }
 name const & get_to_int_name() { return *g_to_int; }
 name const & get_to_real_name() { return *g_to_real; }

src/library/constants.h

@@ -155,6 +155,7 @@ name const & get_monad_name();
 name const & get_monad_map_name();
 name const & get_monad_bind_name();
 name const & get_monad_ret_name();
+name const & get_monad_and_then_name();
 name const & get_monadIO_name();
 name const & get_monoid_name();
 name const & get_mul_name();
@@ -309,6 +310,8 @@ name const & get_subtype_tag_name();
 name const & get_subtype_elt_of_name();
 name const & get_subtype_rec_name();
 name const & get_tactic_name();
+name const & get_tactic_try_name();
+name const & get_tactic_constructor_name();
 name const & get_to_string_name();
 name const & get_to_int_name();
 name const & get_to_real_name();

src/library/constants.txt

@@ -148,6 +148,7 @@ monad
 monad.map
 monad.bind
 monad.ret
+monad.and_then
 monadIO
 monoid
 mul
@@ -302,6 +303,8 @@ subtype.tag
 subtype.elt_of
 subtype.rec
 tactic
+tactic.try
+tactic.constructor
 to_string
 to_int
 to_real

src/library/tactic/tactic_state.cpp

@@ -5,12 +5,14 @@ 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/constants.h"
 #include "library/type_context.h"
 #include "library/pp_options.h"
 #include "library/trace.h"
 #include "library/util.h"
 #include "library/cache_helper.h"
+#include "library/module.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
 #include "library/vm/vm_format.h"
@@ -18,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_level.h"
+#include "library/vm/vm_declaration.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/tactic/tactic_state.h"
@@ -506,6 +509,16 @@ vm_obj tactic_instantiate_mvars(vm_obj const & e, vm_obj const & _s) {
     return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
 }
 
+vm_obj tactic_add_decl(vm_obj const & d, vm_obj const & _s) {
+    tactic_state const & s  = to_tactic_state(_s);
+    try {
+        environment new_env = module::add(s.env(), check(s.env(), to_declaration(d)));
+        return mk_tactic_success(set_env(s, new_env));
+    } catch (throwable & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),            tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}),    tactic_state_format_expr);
@@ -534,6 +547,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "mk_fresh_name"}),        tactic_mk_fresh_name);
     DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for);
     DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}),    tactic_instantiate_mvars);
+    DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}),             tactic_add_decl);
 }
 
 void finalize_tactic_state() {

tests/lean/run/run_tactic1.lean

@@ -0,0 +1,32 @@
+open tactic
+
+run_tactic tactic.trace "hello world"
+
+run_tactic do
+ N ← to_expr `(nat),
+ v ← to_expr `(10),
+ add_decl (declaration.def `val10 [] N v tt)
+
+vm_eval val10
+
+example : val10 = 10 := rfl
+
+meta_definition mk_defs : nat → tactic unit
+| 0     := skip
+| (n+1) := do
+   N ← to_expr `(nat),
+   v ← expr_of_nat n,
+   add_decl (declaration.def (name.append_after `val n) [] N v tt),
+   mk_defs n
+
+run_tactic mk_defs 10
+
+example : val_1 = 1 := rfl
+example : val_2 = 2 := rfl
+example : val_3 = 3 := rfl
+example : val_4 = 4 := rfl
+example : val_5 = 5 := rfl
+example : val_6 = 6 := rfl
+example : val_7 = 7 := rfl
+example : val_8 = 8 := rfl
+example : val_9 = 9 := rfl