diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 2d6d83a59..12c558b32 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -608,8 +608,6 @@ expr elaborator::visit_sort(expr const & e) { expr elaborator::visit_macro(expr const & e, constraint_seq & cs) { if (is_as_is(e)) { return get_as_is_arg(e); - } else if (is_tactic_macro(e)) { - return e; } else { buffer args; for (unsigned i = 0; i < macro_num_args(e); i++) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 233ded8c7..c99b7a0ac 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -131,15 +131,8 @@ 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"}); - register_tac(*g_apply_tactic_name, + register_tac(name({"tactic", "apply"}), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument"); return apply_tactic(fn, get_tactic_expr_expr(app_arg(e))); @@ -150,6 +143,5 @@ void initialize_apply_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 8f16cc8c9..310169354 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -11,7 +11,6 @@ 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); -expr mk_apply_tactic_macro(expr const & e); 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 e171d0e51..be018ccb2 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -157,82 +157,6 @@ void get_tactic_id_list_elements(expr l, buffer & r, char const * error_ms } } -/** \brief We use macros to wrap some builtin tactics that would not type check otherwise. - Example: in the tactic `apply t`, `t` is a pre-term (i.e., a term before elaboration). - Moreover its context depends on the goal it is applied to. -*/ -class tactic_macro_definition_cell : public macro_definition_cell { - name m_name; - expr_to_tactic_fn m_fn; -public: - tactic_macro_definition_cell(name const & n, expr_to_tactic_fn const & fn): - m_name(n), m_fn(fn) {} - name const & get_tatic_kind() const { return m_name; } - expr_to_tactic_fn const & get_fn() const { return m_fn; } - virtual bool operator==(macro_definition_cell const & other) const { - if (tactic_macro_definition_cell const * other_ptr = dynamic_cast(&other)) { - return m_name == other_ptr->m_name; - } else { - return false; - } - } - virtual name get_name() const { return get_tactic_name(); } - virtual format pp(formatter const &) const { return format(m_name); } - virtual void display(std::ostream & out) const { out << m_name; } - virtual pair get_type(expr const &, extension_context &) const { - return mk_pair(get_tactic_type(), constraint_seq()); - } - virtual optional expand(expr const &, extension_context &) const { - // Remark: small hack for conditionally expanding tactic macros. - // When processing type checking a macro definition, we want to unfold it, - // otherwise the kernel will not accept it. - // When converting it to a tactic object, we don't want to unfold it. - // The procedure expr_to_tactic temporarily sets g_unfold_tactic_macros to false. - // This is a thread local storage. So, there is no danger. - if (g_unfold_tactic_macros) - return some_expr(get_builtin_tac()); - else - return none_expr(); - } - virtual void write(serializer & s) const { - s.write_string(get_tactic_opcode()); - s << m_name; - } -}; - -typedef std::unordered_map tactic_macros; -static tactic_macros * g_tactic_macros = nullptr; -tactic_macros & get_tactic_macros() { return *g_tactic_macros; } - -void register_tactic_macro(name const & n, expr_to_tactic_fn const & fn) { - tactic_macros & ms = get_tactic_macros(); - lean_assert(ms.find(n) == ms.end()); - ms.insert(mk_pair(n, macro_definition(new tactic_macro_definition_cell(n, fn)))); -} - -expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args) { - tactic_macros & ms = get_tactic_macros(); - auto it = ms.find(kind); - if (it != ms.end()) { - return mk_macro(it->second, num_args, args); - } else { - throw exception(sstream() << "unknown builtin tactic '" << kind << "'"); - } -} - -expr mk_tactic_macro(name const & kind, expr const & e) { - return mk_tactic_macro(kind, 1, &e); -} - -bool is_tactic_macro(expr const & e) { - return is_macro(e) && macro_def(e).get_name() == get_tactic_name(); -} - -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(); -} - static void throw_failed(expr const & e) { throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); } @@ -249,45 +173,41 @@ static bool is_builtin_tactic(expr const & v) { tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) { e = tc.whnf(e).first; - if (is_tactic_macro(e)) { - return get_tactic_macro_fn(e)(tc, fn, e, p); + expr f = get_app_fn(e); + if (!is_constant(f)) + throw_failed(e); + optional it = tc.env().find(const_name(f)); + if (!it || !it->is_definition()) + throw_failed(e); + expr v = it->get_value(); + if (is_builtin_tactic(v)) { + auto const & map = get_expr_to_tactic_map(); + auto it2 = map.find(const_name(f)); + if (it2 != map.end()) + return it2->second(tc, fn, e, p); + else + throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << + const_name(f) << "' was not found"); } else { - expr f = get_app_fn(e); - if (!is_constant(f)) - throw_failed(e); - optional it = tc.env().find(const_name(f)); - if (!it || !it->is_definition()) - throw_failed(e); - expr v = it->get_value(); - if (is_builtin_tactic(v)) { - auto const & map = get_expr_to_tactic_map(); - auto it2 = map.find(const_name(f)); - if (it2 != map.end()) - return it2->second(tc, fn, e, p); - else - throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << - const_name(f) << "' was not found"); - } else { - // unfold definition - buffer locals; - get_app_rev_args(e, locals); - level_param_names const & ps = it->get_univ_params(); - levels ls = const_levels(f); - unsigned num_ps = length(ps); - unsigned num_ls = length(ls); - if (num_ls > num_ps) - throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); - if (num_ls < num_ps) { - buffer extra_ls; - name_generator ngen = tc.mk_ngen(); - for (unsigned i = num_ls; i < num_ps; i++) - extra_ls.push_back(mk_meta_univ(ngen.next())); - ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); - } - v = instantiate_univ_params(v, ps, ls); - v = apply_beta(v, locals.size(), locals.data()); - return expr_to_tactic(tc, fn, v, p); + // unfold definition + buffer locals; + get_app_rev_args(e, locals); + level_param_names const & ps = it->get_univ_params(); + levels ls = const_levels(f); + unsigned num_ps = length(ps); + unsigned num_ls = length(ls); + if (num_ls > num_ps) + throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); + if (num_ls < num_ps) { + buffer extra_ls; + name_generator ngen = tc.mk_ngen(); + for (unsigned i = num_ls; i < num_ps; i++) + extra_ls.push_back(mk_meta_univ(ngen.next())); + ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); } + v = instantiate_univ_params(v, ps, ls); + v = apply_beta(v, locals.size(), locals.data()); + return expr_to_tactic(tc, fn, v, p); } } @@ -367,11 +287,6 @@ 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); } -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); -} - void initialize_expr_to_tactic() { g_tmp_prefix = new name(name::mk_internal_unique_name()); @@ -398,17 +313,6 @@ void initialize_expr_to_tactic() { g_expr_list_cons = new expr(mk_constant(name({"tactic", "expr_list", "cons"}))); g_expr_list_nil = new expr(mk_constant(name({"tactic", "expr_list", "nil"}))); - g_tactic_opcode = new std::string("TAC"); - - g_tactic_macros = new tactic_macros(); - - register_macro_deserializer(*g_tactic_opcode, - [](deserializer & d, unsigned num, expr const * args) { - name kind; - d >> kind; - return mk_tactic_macro(kind, num, args); - }); - name builtin_tac_name(*g_tactic_name, "builtin"); name and_then_tac_name(*g_tactic_name, "and_then"); name or_else_tac_name(*g_tactic_name, "or_else"); @@ -486,7 +390,6 @@ void finalize_expr_to_tactic() { delete g_or_else_tac_fn; delete g_and_then_tac_fn; delete g_id_tac_fn; - delete g_tactic_macros; delete g_map; delete g_tactic_name; delete g_tactic_opcode; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 9af9445e3..6faead15d 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -57,10 +57,6 @@ expr const & get_id_tac_fn(); expr const & get_repeat_tac_fn(); expr const & get_determ_tac_fn(); -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); - /** \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: @@ -71,11 +67,6 @@ 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 cannot use "std::function <...> const &" in the following procedures, for some obscure reason it produces diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp index 6bcb29a44..65a55413b 100644 --- a/src/library/tactic/rename_tactic.cpp +++ b/src/library/tactic/rename_tactic.cpp @@ -42,27 +42,18 @@ tactic rename_tactic(name const & from, name const & to) { }); } -static name * g_rename_tactic_name = nullptr; - -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); -} - static name const & get_rename_arg(expr const & e) { return tactic_expr_to_id(e, "invalid 'rename' tactic, arguments must be identifiers"); } void initialize_rename_tactic() { - g_rename_tactic_name = new name({"tactic", "rename"}); auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { return rename_tactic(get_rename_arg(app_arg(app_fn(e))), get_rename_arg(app_arg(e))); }; - register_tac(*g_rename_tactic_name, fn); + register_tac(name({"tactic", "rename"}), fn); } void finalize_rename_tactic() { - delete g_rename_tactic_name; } } diff --git a/src/library/tactic/rename_tactic.h b/src/library/tactic/rename_tactic.h index c983dbc69..3193e6563 100644 --- a/src/library/tactic/rename_tactic.h +++ b/src/library/tactic/rename_tactic.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura namespace lean { tactic rename_tactic(name const & from, name const & to); -expr mk_rename_tactic_macro(name const & from, name const & to); void initialize_rename_tactic(); void finalize_rename_tactic(); }