refactor(library/tactic): move apply_tactic initialization to apply_tactic module

src/library/tactic/apply_tactic.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/metavar_closure.h"
 #include "library/type_util.h"
 #include "library/tactic/apply_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
@@ -129,4 +130,26 @@ int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tac
 void open_apply_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac");
 }
+
+static name * g_apply_tactic_name = nullptr;
+
+expr mk_apply_tactic_macro(expr const & e) {
+    return mk_tactic_macro(*g_apply_tactic_name, e);
+}
+
+void initialize_apply_tactic() {
+    g_apply_tactic_name = new name({"tactic", "apply"});
+    auto fn = [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+        check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument");
+        return apply_tactic(fn, macro_arg(e, 0));
+    };
+    register_tactic_macro(*g_apply_tactic_name, fn);
+
+    register_simple_tac(name({"tactic", "eassumption"}),
+                        []() { return eassumption_tactic(); });
+}
+
+void finalize_apply_tactic() {
+    delete g_apply_tactic_name;
+}
 }

src/library/tactic/apply_tactic.h

@@ -11,4 +11,7 @@ namespace lean {
 tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool relax_main_opaque = true);
 tactic eassumption_tactic(bool relax_main_opaque = true);
 void open_apply_tactic(lua_State * L);
+
+void initialize_apply_tactic();
+void finalize_apply_tactic();
 }

src/library/tactic/expr_to_tactic.cpp

@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/kernel_serializer.h"
 #include "library/tactic/expr_to_tactic.h"
-#include "library/tactic/apply_tactic.h"
 #include "library/tactic/intros_tactic.h"
 
 namespace lean {
@@ -144,14 +143,9 @@ bool is_tactic_macro(expr const & e) {
     return is_macro(e) && macro_def(e).get_name() == get_tactic_name();
 }
 
-static name * g_apply_tactic_name = nullptr;
 static name * g_rename_tactic_name = nullptr;
 static name * g_intros_tactic_name = nullptr;
 
-expr mk_apply_tactic_macro(expr const & e) {
-    return mk_tactic_macro(*g_apply_tactic_name, e);
-}
-
 expr mk_rename_tactic_macro(name const & from, name const & to) {
     expr args[2] = { Const(from), Const(to) };
     return mk_tactic_macro(*g_rename_tactic_name, 2, args);
@@ -304,8 +298,8 @@ 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); }
 
-static void check_macro_args(expr const & e, unsigned num_args, char const * msg) {
+void check_macro_args(expr const & e, unsigned num_args, char const * msg) {
-    if (macro_num_args(e) != num_args)
+    if (!is_macro(e) || macro_num_args(e) != num_args)
         throw expr_to_tactic_exception(e, msg);
 }
 
@@ -329,7 +323,6 @@ void initialize_expr_to_tactic() {
                                     return mk_tactic_macro(kind, num, args);
                                 });
 
-    g_apply_tactic_name = new name(*g_tactic_name, "apply");
     g_rename_tactic_name = new name(*g_tactic_name, "rename");
     g_intros_tactic_name = new name(*g_tactic_name, "intros");
 
@@ -357,8 +350,6 @@ void initialize_expr_to_tactic() {
                         []() { return now_tactic(); });
     register_simple_tac(name(*g_tactic_name, "assumption"),
                         []() { return assumption_tactic(); });
-    register_simple_tac(name(*g_tactic_name, "eassumption"),
-                        []() { return eassumption_tactic(); });
     register_simple_tac(name(*g_tactic_name, "fail"),
                         []() { return fail_tactic(); });
     register_simple_tac(name(*g_tactic_name, "beta"),
@@ -395,11 +386,6 @@ void initialize_expr_to_tactic() {
                      else
                          throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
                  });
-    register_tacm(*g_apply_tactic_name,
-                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
-                      check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument");
-                      return apply_tactic(fn, macro_arg(e, 0));
-                  });
     register_tacm(*g_rename_tactic_name,
                   [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                       check_macro_args(e, 2, "invalid 'rename' tactic, it must have two arguments");
@@ -458,7 +444,6 @@ void finalize_expr_to_tactic() {
     delete g_and_then_tac_fn;
     delete g_id_tac_fn;
     delete g_exact_tac_fn;
-    delete g_apply_tactic_name;
     delete g_rename_tactic_name;
     delete g_intros_tactic_name;
     delete g_tactic_macros;

src/library/tactic/expr_to_tactic.h

@@ -66,9 +66,14 @@ public:
 typedef std::function<tactic(type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
 expr_to_tactic_fn;
 
+/** \brief Throw an error if the given expression is not a macro with \c num_args arguments */
+void check_macro_args(expr const & e, unsigned num_args, char const * msg);
+
+void register_tactic_macro(name const & n, expr_to_tactic_fn const & fn);
+
 /** \brief Register a new "procedural attachment" for expr_to_tactic. */
 void register_tac(name const & n, expr_to_tactic_fn const & fn);
-// remark: we can use "const &" in the following procedures, for some obscure reason it produces
+// remark: we cannot use "std::function <...> const &" in the following procedures, for some obscure reason it produces
 // memory leaks when we compile using clang 3.3
 void register_simple_tac(name const & n, std::function<tactic()> f);
 void register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f);

src/library/tactic/init_module.cpp

@@ -6,14 +6,17 @@ Author: Leonardo de Moura
 */
 #include "library/tactic/proof_state.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/apply_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
     initialize_proof_state();
     initialize_expr_to_tactic();
+    initialize_apply_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_apply_tactic();
     finalize_expr_to_tactic();
     finalize_proof_state();
 }