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

src/frontends/lean/builtin_tactics.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/tactic/apply_tactic.h"
 #include "library/tactic/rename_tactic.h"
-#include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/intros_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parse_table.h"
 

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/intros_tactic.h"
 
 namespace lean {
 static expr * g_exact_tac_fn      = nullptr;
@@ -143,16 +142,6 @@ bool is_tactic_macro(expr const & e) {
     return is_macro(e) && macro_def(e).get_name() == get_tactic_name();
 }
 
-static name * g_intros_tactic_name = nullptr;
-
-expr mk_intros_tactic_macro(buffer<name> const & ns) {
-    buffer<expr> args;
-    for (name const & n : ns) {
-        args.push_back(Const(n));
-    }
-    return mk_tactic_macro(*g_intros_tactic_name, args.size(), args.data());
-}
-
 expr_to_tactic_fn const & get_tactic_macro_fn(expr const & e) {
     lean_assert(is_tactic_macro(e));
     return static_cast<tactic_macro_definition_cell const*>(macro_def(e).raw())->get_fn();
@@ -317,8 +306,6 @@ void initialize_expr_to_tactic() {
                                     return mk_tactic_macro(kind, num, args);
                                 });
 
-    g_intros_tactic_name = new name(*g_tactic_name, "intros");
-
     name builtin_tac_name(*g_tactic_name, "builtin");
     name exact_tac_name(*g_tactic_name, "exact");
     name and_then_tac_name(*g_tactic_name, "and_then");
@@ -379,17 +366,6 @@ void initialize_expr_to_tactic() {
                      else
                          throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
                  });
-    register_tacm(*g_intros_tactic_name,
-                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                      buffer<name> ns;
-                      for (unsigned i = 0; i < macro_num_args(e); i++) {
-                          expr const & arg = macro_arg(e, i);
-                          if (!is_constant(arg))
-                              throw expr_to_tactic_exception(e, "invalid 'intros' tactic, arguments must be identifiers");
-                          ns.push_back(const_name(arg));
-                      }
-                      return intros_tactic(to_list(ns.begin(), ns.end()));
-                  });
     register_tac(exact_tac_name,
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      // TODO(Leo): use elaborate_fn
@@ -430,7 +406,6 @@ void finalize_expr_to_tactic() {
     delete g_and_then_tac_fn;
     delete g_id_tac_fn;
     delete g_exact_tac_fn;
-    delete g_intros_tactic_name;
     delete g_tactic_macros;
     delete g_map;
     delete g_tactic_name;

src/library/tactic/expr_to_tactic.h

@@ -52,8 +52,6 @@ expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args);
 expr mk_tactic_macro(name const & kind, expr const & e);
 bool is_tactic_macro(expr const & e);
 
-expr mk_intros_tactic_macro(buffer<name> const & ns);
-
 /** \brief Exception used to report a problem when an expression is being converted into a tactic. */
 class expr_to_tactic_exception : public tactic_exception {
 public:

src/library/tactic/init_module.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/apply_tactic.h"
 #include "library/tactic/rename_tactic.h"
+#include "library/tactic/intros_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -15,9 +16,11 @@ void initialize_tactic_module() {
     initialize_expr_to_tactic();
     initialize_apply_tactic();
     initialize_rename_tactic();
+    initialize_intros_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_intros_tactic();
     finalize_rename_tactic();
     finalize_apply_tactic();
     finalize_expr_to_tactic();

src/library/tactic/intros_tactic.cpp

@@ -6,7 +6,8 @@ Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
 #include "library/reducible.h"
-#include "library/tactic/tactic.h"
+#include "library/tactic/intros_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
 /** \brief Return a "user" name that is not used by any local constant in the given goal */
@@ -73,4 +74,33 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
     };
     return tactic01(fn);
 }
+
+static name * g_intros_tactic_name = nullptr;
+
+expr mk_intros_tactic_macro(buffer<name> const & ns) {
+    buffer<expr> args;
+    for (name const & n : ns) {
+        args.push_back(Const(n));
+    }
+    return mk_tactic_macro(*g_intros_tactic_name, args.size(), args.data());
+}
+
+void initialize_intros_tactic() {
+    g_intros_tactic_name = new name({"tactic", "intros"});
+    auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+        buffer<name> ns;
+        for (unsigned i = 0; i < macro_num_args(e); i++) {
+            expr const & arg = macro_arg(e, i);
+            if (!is_constant(arg))
+                throw expr_to_tactic_exception(e, "invalid 'intros' tactic, arguments must be identifiers");
+            ns.push_back(const_name(arg));
+        }
+        return intros_tactic(to_list(ns.begin(), ns.end()));
+    };
+    register_tactic_macro(*g_intros_tactic_name, fn);
+}
+
+void finalize_intros_tactic() {
+    delete g_intros_tactic_name;
+}
 }

src/library/tactic/intros_tactic.h

@@ -8,4 +8,7 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 namespace lean {
 tactic intros_tactic(list<name> ns, bool relax_main_opaque = true);
+expr mk_intros_tactic_macro(buffer<name> const & ns);
+void initialize_intros_tactic();
+void finalize_intros_tactic();
 }