From ac9397816f9f605db8f946e82d480b12e3e53460 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 17:32:32 -0700 Subject: [PATCH] refactor(library/tactic): move apply_tactic initialization to apply_tactic module --- src/library/tactic/apply_tactic.cpp | 23 +++++++++++++++++++++++ src/library/tactic/apply_tactic.h | 3 +++ src/library/tactic/expr_to_tactic.cpp | 19 ++----------------- src/library/tactic/expr_to_tactic.h | 7 ++++++- src/library/tactic/init_module.cpp | 3 +++ 5 files changed, 37 insertions(+), 18 deletions(-) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 28ae9f6fb..189f07335 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/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; +} } diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index e84e80acc..bc3b519ca 100644 --- a/src/library/tactic/apply_tactic.h +++ b/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(); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 4d50f3f88..dce489a24 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/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) { - if (macro_num_args(e) != num_args) +void check_macro_args(expr const & e, unsigned num_args, char const * msg) { + 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; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index f8bf97c2a..87163b74c 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -66,9 +66,14 @@ public: typedef std::function 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 f); void register_bin_tac(name const & n, std::function f); diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 60fb890fc..503eb21d8 100644 --- a/src/library/tactic/init_module.cpp +++ b/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(); }