From 53a64ac7673a677aa718ace3d5bee1a83780e2f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 17:47:52 -0700 Subject: [PATCH] refactor(library/tactic): move intros_tactic initialization to intros_tactic module --- src/frontends/lean/builtin_tactics.cpp | 2 +- src/library/tactic/expr_to_tactic.cpp | 25 -------------------- src/library/tactic/expr_to_tactic.h | 2 -- src/library/tactic/init_module.cpp | 3 +++ src/library/tactic/intros_tactic.cpp | 32 +++++++++++++++++++++++++- src/library/tactic/intros_tactic.h | 3 +++ 6 files changed, 38 insertions(+), 29 deletions(-) diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index c29cedfbf..dc6179381 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/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" diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index da60354af..d84b357e0 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/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 const & ns) { - buffer 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(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 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; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 9bdf62975..2a8ab340f 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/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 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: diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index a11174719..dec2b2814 100644 --- a/src/library/tactic/init_module.cpp +++ b/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(); diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index bd0aa1f2f..2ad234e7f 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/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 _ns, bool relax_main_opaque) { }; return tactic01(fn); } + +static name * g_intros_tactic_name = nullptr; + +expr mk_intros_tactic_macro(buffer const & ns) { + buffer 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 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; +} } diff --git a/src/library/tactic/intros_tactic.h b/src/library/tactic/intros_tactic.h index 8e549a2af..713ec166e 100644 --- a/src/library/tactic/intros_tactic.h +++ b/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 ns, bool relax_main_opaque = true); +expr mk_intros_tactic_macro(buffer const & ns); +void initialize_intros_tactic(); +void finalize_intros_tactic(); }