From ca57b4369861c54f4844e78f279f7e2dcca338c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Mar 2015 14:15:23 -0800 Subject: [PATCH] feat(library/tactic): add 'change' tactic --- hott/init/tactic.hlean | 3 ++ library/init/tactic.lean | 3 ++ src/emacs/lean-syntax.el | 2 +- src/library/constants.cpp | 8 ++++ src/library/constants.h | 2 + src/library/constants.txt | 2 + src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/change_tactic.cpp | 56 ++++++++++++++++++++++++++++ src/library/tactic/change_tactic.h | 13 +++++++ src/library/tactic/init_module.cpp | 3 ++ 10 files changed, 93 insertions(+), 2 deletions(-) create mode 100644 src/library/tactic/change_tactic.cpp create mode 100644 src/library/tactic/change_tactic.h diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index a568012e8..84b93e858 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -92,6 +92,9 @@ notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` opaque definition revert_lst (ids : expr_list) : tactic := builtin notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l +opaque definition change_goal (e : expr) : tactic := builtin +notation `change` e := change_goal e + opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin infixl `;`:15 := and_then diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 490955979..e5ed8ad0c 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -91,6 +91,9 @@ notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` opaque definition revert_lst (ids : expr_list) : tactic := builtin notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l +opaque definition change_goal (e : expr) : tactic := builtin +notation `change` e := change_goal e + opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin infixl `;`:15 := and_then diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index f7340f2e6..7ed655112 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -131,7 +131,7 @@ (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros" "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" - "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold")) + "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 0b872dc71..2c413a2c4 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -69,6 +69,8 @@ name const * g_tactic_assumption = nullptr; name const * g_tactic_at_most = nullptr; name const * g_tactic_beta = nullptr; name const * g_tactic_builtin = nullptr; +name const * g_tactic_change_goal = nullptr; +name const * g_tactic_change_hypothesis = nullptr; name const * g_tactic_clear = nullptr; name const * g_tactic_clear_lst = nullptr; name const * g_tactic_determ = nullptr; @@ -178,6 +180,8 @@ void initialize_constants() { g_tactic_at_most = new name{"tactic", "at_most"}; g_tactic_beta = new name{"tactic", "beta"}; g_tactic_builtin = new name{"tactic", "builtin"}; + g_tactic_change_goal = new name{"tactic", "change_goal"}; + g_tactic_change_hypothesis = new name{"tactic", "change_hypothesis"}; g_tactic_clear = new name{"tactic", "clear"}; g_tactic_clear_lst = new name{"tactic", "clear_lst"}; g_tactic_determ = new name{"tactic", "determ"}; @@ -288,6 +292,8 @@ void finalize_constants() { delete g_tactic_at_most; delete g_tactic_beta; delete g_tactic_builtin; + delete g_tactic_change_goal; + delete g_tactic_change_hypothesis; delete g_tactic_clear; delete g_tactic_clear_lst; delete g_tactic_determ; @@ -397,6 +403,8 @@ name const & get_tactic_assumption_name() { return *g_tactic_assumption; } name const & get_tactic_at_most_name() { return *g_tactic_at_most; } name const & get_tactic_beta_name() { return *g_tactic_beta; } name const & get_tactic_builtin_name() { return *g_tactic_builtin; } +name const & get_tactic_change_goal_name() { return *g_tactic_change_goal; } +name const & get_tactic_change_hypothesis_name() { return *g_tactic_change_hypothesis; } name const & get_tactic_clear_name() { return *g_tactic_clear; } name const & get_tactic_clear_lst_name() { return *g_tactic_clear_lst; } name const & get_tactic_determ_name() { return *g_tactic_determ; } diff --git a/src/library/constants.h b/src/library/constants.h index 0c6dcca58..b1a6df776 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -71,6 +71,8 @@ name const & get_tactic_assumption_name(); name const & get_tactic_at_most_name(); name const & get_tactic_beta_name(); name const & get_tactic_builtin_name(); +name const & get_tactic_change_goal_name(); +name const & get_tactic_change_hypothesis_name(); name const & get_tactic_clear_name(); name const & get_tactic_clear_lst_name(); name const & get_tactic_determ_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index b1386632a..c443389e4 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -64,6 +64,8 @@ tactic.assumption tactic.at_most tactic.beta tactic.builtin +tactic.change_goal +tactic.change_hypothesis tactic.clear tactic.clear_lst tactic.determ diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index c8df8ba15..60a675f37 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -3,6 +3,7 @@ apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp -rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp) +rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp +change_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp new file mode 100644 index 000000000..e0d1158f6 --- /dev/null +++ b/src/library/tactic/change_tactic.cpp @@ -0,0 +1,56 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/constants.h" +#include "kernel/type_checker.h" +#include "library/reducible.h" +#include "library/tactic/tactic.h" +#include "library/tactic/elaborate.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { + return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { + proof_state new_s = s; + goals const & gs = new_s.get_goals(); + if (!gs) { + throw_no_goal_if_enabled(s); + return none_proof_state(); + } + expr t = head(gs).get_type(); + bool report_unassigned = true; + if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) { + goals const & gs = new_s.get_goals(); + goal const & g = head(gs); + name_generator ngen = new_s.get_ngen(); + substitution subst = new_s.get_subst(); + auto tc = mk_type_checker(env, ngen.mk_child()); + constraint_seq cs; + if (tc->is_def_eq(t, *new_e, justification(), cs) && !cs) { + expr M = g.mk_meta(ngen.next(), *new_e); + goal new_g(M, *new_e); + expr val = g.abstract(M); + subst.assign(g.get_name(), val); + return some(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen)); + } else { + // generate error + return none_proof_state(); + } + } + return none_proof_state(); + }); +} + +void initialize_change_tactic() { + register_tac(get_tactic_change_goal_name(), + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'change' tactic, invalid argument"); + return change_goal_tactic(fn, get_tactic_expr_expr(app_arg(e))); + }); +} +void finalize_change_tactic() { +} +} diff --git a/src/library/tactic/change_tactic.h b/src/library/tactic/change_tactic.h new file mode 100644 index 000000000..5e849a494 --- /dev/null +++ b/src/library/tactic/change_tactic.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" + +namespace lean { +void initialize_change_tactic(); +void finalize_change_tactic(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index a31778a47..3f5e9ba5b 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/tactic/assert_tactic.h" #include "library/tactic/class_instance_synth.h" #include "library/tactic/rewrite_tactic.h" +#include "library/tactic/change_tactic.h" namespace lean { void initialize_tactic_module() { @@ -41,9 +42,11 @@ void initialize_tactic_module() { initialize_assert_tactic(); initialize_class_instance_elaborator(); initialize_rewrite_tactic(); + initialize_change_tactic(); } void finalize_tactic_module() { + finalize_change_tactic(); finalize_rewrite_tactic(); finalize_class_instance_elaborator(); finalize_assert_tactic();