From e6606ef2acf52a3cff47bf91d2cb813073b768b4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Oct 2014 18:19:34 -0700 Subject: [PATCH] feat(library/tactic): add 'rename' hypothesis tactic --- src/emacs/lean-syntax.el | 3 ++- src/frontends/lean/builtin_tactics.cpp | 9 ++++++- src/frontends/lean/token_table.cpp | 2 +- src/library/tactic/expr_to_tactic.cpp | 15 ++++++++++++ src/library/tactic/expr_to_tactic.h | 1 + src/library/tactic/tactic.cpp | 34 ++++++++++++++++++++++++++ src/library/tactic/tactic.h | 3 +++ tests/lean/run/rename_tac.lean | 10 ++++++++ 8 files changed, 74 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/rename_tac.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 2c6681c0b2..1bcf3287b3 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -118,7 +118,8 @@ (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics (,(rx word-start - (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat") + (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" + "back" "beta" "done" "exact" "repeat") word-end) . 'font-lock-constant-face) ;; Types diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index cd5ceb30a1..d6f8cd2c9f 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -20,9 +20,16 @@ static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos return p.save_pos(mk_apply_tactic_macro(e), pos); } +static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & pos) { + name from = p.check_id_next("invalid 'rename' tactic, identifier expected"); + name to = p.check_id_next("invalid 'rename' tactic, identifier expected"); + return p.save_pos(mk_rename_tactic_macro(from, to), pos); +} + void init_nud_tactic_table(parse_table & r) { expr x0 = mk_var(0); - r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0); + r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0); + r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0); } void initialize_builtin_tactics() { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 98e1008825..2265d3eef1 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -76,7 +76,7 @@ void init_token_table(token_table & t) { {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0}, - {"apply", 0}, {nullptr, 0}}; + {"apply", 0}, {"rename", 0}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 2a9b93d3a6..d8181eeb99 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -137,11 +137,17 @@ bool is_tactic_macro(expr const & e) { } static name * g_apply_tactic_name = nullptr; +static name * g_rename_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); +} + 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(); @@ -307,6 +313,7 @@ void initialize_expr_to_tactic() { }); g_apply_tactic_name = new name(*g_tactic_name, "apply"); + g_rename_tactic_name = new name(*g_tactic_name, "rename"); name builtin_tac_name(*g_tactic_name, "builtin"); name exact_tac_name(*g_tactic_name, "exact"); @@ -376,6 +383,13 @@ void initialize_expr_to_tactic() { 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"); + if (!is_constant(macro_arg(e, 0)) || !is_constant(macro_arg(e, 1))) + throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers"); + return rename_tactic(const_name(macro_arg(e, 0)), const_name(macro_arg(e, 1))); + }); register_tac(exact_tac_name, [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { // TODO(Leo): use elaborate_fn @@ -417,6 +431,7 @@ void finalize_expr_to_tactic() { delete g_id_tac_fn; delete g_exact_tac_fn; delete g_apply_tactic_name; + delete g_rename_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 210887a75f..683dc150d8 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -52,6 +52,7 @@ 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_apply_tactic_macro(expr const & e); +expr mk_rename_tactic_macro(name const & from, name const & to); /** \brief Exception used to report a problem when an expression is being converted into a tactic. */ class expr_to_tactic_exception : public tactic_exception { diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 78dadf0920..7458f9b3a6 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/type_checker.h" #include "kernel/for_each_fn.h" +#include "kernel/replace_fn.h" #include "kernel/replace_visitor.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" @@ -211,6 +212,39 @@ tactic discard(tactic const & t, unsigned k) { }); } +tactic rename_tactic(name const & from, name const & to) { + return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + goals const & gs = s.get_goals(); + if (empty(gs)) + return none_proof_state(); + goal const & g = head(gs); + goals const & rest_gs = tail(gs); + buffer locals; + get_app_args(g.get_meta(), locals); + unsigned i = locals.size(); + optional from_local; + while (i > 0) { + --i; + expr const & local = locals[i]; + if (local_pp_name(local) == from) { + from_local = local; + break; + } + } + if (!from_local) + return none_proof_state(); + expr to_local = mk_local(mlocal_name(*from_local), to, mlocal_type(*from_local), local_info(*from_local)); + auto fn = [&](expr const & e) { + if (is_local(e) && mlocal_name(e) == mlocal_name(*from_local)) + return some_expr(to_local); + else + return none_expr(); + }; + goal new_g(replace(g.get_meta(), fn), replace(g.get_type(), fn)); + return some(proof_state(s, goals(new_g, rest_gs))); + }); +} + tactic assumption_tactic() { return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { substitution subst = s.get_subst(); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 0c3c90e82b..c45297e072 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -127,6 +127,9 @@ tactic take(tactic const & t, unsigned k); */ tactic discard(tactic const & t, unsigned k); +/** \brief Return a tactic that renames hypothesis \c from into \c to in the current goal. */ +tactic rename_tactic(name const & from, name const & to); + typedef std::function proof_state_pred; // NOLINT /** \brief Return a tactic that applies the predicate \c p to the input state. diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean new file mode 100644 index 0000000000..f6b27c3001 --- /dev/null +++ b/tests/lean/run/rename_tac.lean @@ -0,0 +1,10 @@ +import tools.tactic +open tactic + +theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := +begin + apply eq.trans, + apply Hbc, + rename Hab Foo, + apply Foo +end