From 7c617955d098ed45bfdd7e4d18f01318394fca3c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Oct 2014 14:23:14 -0700 Subject: [PATCH] refactor(library/tactic): move 'exact' tactic to separate module --- src/frontends/lean/builtin_exprs.cpp | 1 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/exact_tactic.cpp | 50 +++++++++++++++++++++++++++ src/library/tactic/exact_tactic.h | 16 +++++++++ src/library/tactic/expr_to_tactic.cpp | 10 ------ src/library/tactic/expr_to_tactic.h | 1 - src/library/tactic/init_module.cpp | 3 ++ src/library/tactic/tactic.cpp | 22 ------------ src/library/tactic/tactic.h | 2 -- 9 files changed, 71 insertions(+), 36 deletions(-) create mode 100644 src/library/tactic/exact_tactic.cpp create mode 100644 src/library/tactic/exact_tactic.h diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 36242a518..17cb81398 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" +#include "library/tactic/exact_tactic.h" #include "library/typed_expr.h" #include "library/choice.h" #include "library/let.h" diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index d7b922e6c..328cb7726 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp -expr_to_tactic.cpp init_module.cpp) +exact_tactic.cpp expr_to_tactic.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp new file mode 100644 index 000000000..945a1a8a6 --- /dev/null +++ b/src/library/tactic/exact_tactic.cpp @@ -0,0 +1,50 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/type_checker.h" +#include "library/tactic/tactic.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +tactic exact_tactic(expr const & _e) { + return tactic01([=](environment const & env, io_state const &, proof_state const & s) { + type_checker tc(env); + substitution subst = s.get_subst(); + goals const & gs = s.get_goals(); + goal const & g = head(gs); + expr e = subst.instantiate(_e); + auto e_t_cs = tc.infer(e); + expr e_t = subst.instantiate(e_t_cs.first); + expr t = subst.instantiate(g.get_type()); + auto dcs = tc.is_def_eq(e_t, t); + if (dcs.first && !dcs.second && !e_t_cs.second) { + expr new_p = g.abstract(e); + check_has_no_local(new_p, _e, "exact"); + subst.assign(g.get_name(), new_p); + return some(proof_state(s, tail(gs), subst)); + } else { + return none_proof_state(); + } + }); +} + +static expr * g_exact_tac_fn = nullptr; + +expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } + +void initialize_exact_tactic() { + name exact_tac_name({"tactic", "exact"}); + g_exact_tac_fn = new expr(Const(exact_tac_name)); + register_tac(exact_tac_name, + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + // TODO(Leo): use elaborate_fn + return exact_tactic(app_arg(e)); + }); +} +void finalize_exact_tactic() { + delete g_exact_tac_fn; +} +} diff --git a/src/library/tactic/exact_tactic.h b/src/library/tactic/exact_tactic.h new file mode 100644 index 000000000..c229033a8 --- /dev/null +++ b/src/library/tactic/exact_tactic.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2014 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 { +expr const & get_exact_tac_fn(); +/** \brief Solve first goal iff it is definitionally equal to type of \c e */ +tactic exact_tactic(expr const & e); +void initialize_exact_tactic(); +void finalize_exact_tactic(); +} diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 3372b56df..dba5a5199 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -static expr * g_exact_tac_fn = nullptr; static expr * g_and_then_tac_fn = nullptr; static expr * g_or_else_tac_fn = nullptr; static expr * g_id_tac_fn = nullptr; @@ -26,7 +25,6 @@ static expr * g_determ_tac_fn = nullptr; static expr * g_tac_type = nullptr; static expr * g_builtin_tac = nullptr; static expr * g_fixpoint_tac = nullptr; -expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; } expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; } expr const & get_id_tac_fn() { return *g_id_tac_fn; } @@ -303,14 +301,12 @@ void initialize_expr_to_tactic() { }); 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"); name or_else_tac_name(*g_tactic_name, "or_else"); name repeat_tac_name(*g_tactic_name, "repeat"); name fixpoint_name(*g_tactic_name, "fixpoint"); name determ_tac_name(*g_tactic_name, "determ"); name id_tac_name(*g_tactic_name, "id"); - g_exact_tac_fn = new expr(Const(exact_tac_name)); g_and_then_tac_fn = new expr(Const(and_then_tac_name)); g_or_else_tac_fn = new expr(Const(or_else_tac_name)); g_id_tac_fn = new expr(Const(id_tac_name)); @@ -342,11 +338,6 @@ void initialize_expr_to_tactic() { [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); register_unary_tac(repeat_tac_name, [](tactic const & t1) { return repeat(t1); }); - register_tac(exact_tac_name, - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - // TODO(Leo): use elaborate_fn - return exact_tactic(app_arg(e)); - }); register_tac(name(*g_tactic_name, "unfold"), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { expr id = get_app_fn(app_arg(e)); @@ -381,7 +372,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_exact_tac_fn; 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 2a8ab340f..c33993287 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -41,7 +41,6 @@ bool is_by(expr const & t); expr const & get_by_arg(expr const & t); expr const & get_tactic_type(); -expr const & get_exact_tac_fn(); expr const & get_and_then_tac_fn(); expr const & get_or_else_tac_fn(); expr const & get_id_tac_fn(); diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index d899e41ca..21fda67fc 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/tactic/rename_tactic.h" #include "library/tactic/intros_tactic.h" #include "library/tactic/trace_tactic.h" +#include "library/tactic/exact_tactic.h" namespace lean { void initialize_tactic_module() { @@ -19,9 +20,11 @@ void initialize_tactic_module() { initialize_rename_tactic(); initialize_intros_tactic(); initialize_trace_tactic(); + initialize_exact_tactic(); } void finalize_tactic_module() { + finalize_exact_tactic(); finalize_trace_tactic(); finalize_intros_tactic(); finalize_rename_tactic(); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 226ef8b4b..cf814fc3e 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -200,28 +200,6 @@ tactic assumption_tactic() { }); } -tactic exact_tactic(expr const & _e) { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) { - type_checker tc(env); - substitution subst = s.get_subst(); - goals const & gs = s.get_goals(); - goal const & g = head(gs); - expr e = subst.instantiate(_e); - auto e_t_cs = tc.infer(e); - expr e_t = subst.instantiate(e_t_cs.first); - expr t = subst.instantiate(g.get_type()); - auto dcs = tc.is_def_eq(e_t, t); - if (dcs.first && !dcs.second && !e_t_cs.second) { - expr new_p = g.abstract(e); - check_has_no_local(new_p, _e, "exact"); - subst.assign(g.get_name(), new_p); - return some(proof_state(s, tail(gs), subst)); - } else { - return none_proof_state(); - } - }); -} - tactic beta_tactic() { return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { bool reduced = false; diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 0e3d2f39b..48539b7a4 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -134,8 +134,6 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_ */ tactic focus(tactic const & t, unsigned i); inline tactic focus(tactic const & t) { return focus(t, 1); } -/** \brief Solve first goal iff it is definitionally equal to \c e */ -tactic exact_tactic(expr const & e); /** \brief Return a tactic that unfolds the definition named \c n. */ tactic unfold_tactic(name const & n); /** \brief Return a tactic that unfolds all (non-opaque) definitions. */