From 6fcba192b2cdd76fcd3fb62919869aa471f6b08f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Oct 2014 09:33:16 -0700 Subject: [PATCH] refactor(library/tactic): move 'unfold' tactic to separate module --- src/library/tactic/CMakeLists.txt | 4 +- src/library/tactic/expr_to_tactic.cpp | 8 -- src/library/tactic/init_module.cpp | 3 + src/library/tactic/tactic.cpp | 113 ---------------------- src/library/tactic/tactic.h | 4 - src/library/tactic/unfold_tactic.cpp | 129 ++++++++++++++++++++++++++ src/library/tactic/unfold_tactic.h | 18 ++++ 7 files changed, 152 insertions(+), 127 deletions(-) create mode 100644 src/library/tactic/unfold_tactic.cpp create mode 100644 src/library/tactic/unfold_tactic.h diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 61ace6088..149c3fafb 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 +add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp -exact_tactic.cpp expr_to_tactic.cpp elaborate.cpp init_module.cpp) +exact_tactic.cpp unfold_tactic.cpp expr_to_tactic.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 0a081c3f1..9976d8d0a 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -339,14 +339,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(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)); - if (!is_constant(id)) - return fail_tactic(); - else - return unfold_tactic(const_name(id)); - }); register_unary_num_tac(name(*g_tactic_name, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); }); register_unary_num_tac(name(*g_tactic_name, "discard"), diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 21fda67fc..1bc57c5b2 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/tactic/intros_tactic.h" #include "library/tactic/trace_tactic.h" #include "library/tactic/exact_tactic.h" +#include "library/tactic/unfold_tactic.h" namespace lean { void initialize_tactic_module() { @@ -21,9 +22,11 @@ void initialize_tactic_module() { initialize_intros_tactic(); initialize_trace_tactic(); initialize_exact_tactic(); + initialize_unfold_tactic(); } void finalize_tactic_module() { + finalize_unfold_tactic(); finalize_exact_tactic(); finalize_trace_tactic(); finalize_intros_tactic(); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index cf814fc3e..43da73a4b 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" -#include "library/replace_visitor.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" #include "library/io_state_stream.h" @@ -239,110 +238,6 @@ tactic focus(tactic const & t, unsigned i) { }); } -class unfold_core_fn : public replace_visitor { -protected: - bool m_unfolded; - - virtual expr visit_app(expr const & e) { - expr const & f = get_app_fn(e); - if (is_constant(f)) { - expr new_f = visit(f); - bool modified = new_f != f; - buffer new_args; - get_app_args(e, new_args); - for (unsigned i = 0; i < new_args.size(); i++) { - expr arg = new_args[i]; - new_args[i] = visit(arg); - if (!modified && new_args[i] != arg) - modified = true; - } - if (is_lambda(new_f)) { - std::reverse(new_args.begin(), new_args.end()); - return apply_beta(new_f, new_args.size(), new_args.data()); - } else if (modified) { - return mk_app(new_f, new_args); - } else { - return e; - } - } else { - return replace_visitor::visit_app(e); - } - } -public: - unfold_core_fn():m_unfolded(false) {} - bool unfolded() const { return m_unfolded; } -}; - -class unfold_fn : public unfold_core_fn { -protected: - name const & m_name; - level_param_names const & m_ps; - expr const & m_def; - - virtual expr visit_constant(expr const & c) { - if (const_name(c) == m_name) { - m_unfolded = true; - return instantiate_univ_params(m_def, m_ps, const_levels(c)); - } else { - return c; - } - } - -public: - unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {} -}; - -class unfold_all_fn : public unfold_core_fn { -protected: - environment m_env; - - virtual expr visit_constant(expr const & c) { - optional d = m_env.find(const_name(c)); - if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) { - m_unfolded = true; - return instantiate_value_univ_params(*d, const_levels(c)); - } else { - return c; - } - } - -public: - unfold_all_fn(environment const & env):m_env(env) {} -}; - -optional unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) { - bool reduced = false; - goals new_gs = map_goals(s, [&](goal const & g) -> optional { - expr new_meta = fn(g.get_meta()); - expr new_type = fn(g.get_type()); - if (new_meta != g.get_meta() || new_type != g.get_type()) - reduced = true; - return some(goal(new_meta, new_type)); - }); - if (reduced) { - return some(proof_state(s, new_gs)); - } else { - return none_proof_state(); - } -} - -tactic unfold_tactic(name const & n) { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { - optional d = env.find(n); - if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0)) - return none_proof_state(); // tactic failed - unfold_fn fn(n, d->get_univ_params(), d->get_value()); - return unfold_tactic_core(fn, s); - }); -} - -tactic unfold_tactic() { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { - unfold_all_fn fn(env); - return unfold_tactic_core(fn, s); - }); -} - DECL_UDATA(proof_state_seq) static const struct luaL_Reg proof_state_seq_m[] = { {"__gc", proof_state_seq_gc}, // never throws @@ -464,13 +359,6 @@ static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tact static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tactic()); } static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); } static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); } -static int mk_unfold_tactic(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_tactic(L, unfold_tactic()); - else - return push_tactic(L, unfold_tactic(to_name_ext(L, 1))); -} static int mk_beta_tactic(lua_State * L) { return push_tactic(L, beta_tactic()); } static const struct luaL_Reg tactic_m[] = { {"__gc", tactic_gc}, // never throws @@ -510,7 +398,6 @@ void open_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_now_tactic, "now_tac"); SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac"); SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tac"); - SET_GLOBAL_FUN(mk_unfold_tactic, "unfold_tac"); SET_GLOBAL_FUN(mk_beta_tactic, "beta_tac"); SET_GLOBAL_FUN(mk_lua_tactic01, "tactic01"); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 1f3ffe426..2ba71b1f7 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -129,10 +129,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 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. */ -tactic unfold_tactic(); /** \brief Return a tactic that applies beta-reduction. */ tactic beta_tactic(); diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp new file mode 100644 index 000000000..be9c1b207 --- /dev/null +++ b/src/library/tactic/unfold_tactic.cpp @@ -0,0 +1,129 @@ +/* +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/instantiate.h" +#include "library/replace_visitor.h" +#include "library/tactic/unfold_tactic.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +class unfold_core_fn : public replace_visitor { +protected: + bool m_unfolded; + + virtual expr visit_app(expr const & e) { + expr const & f = get_app_fn(e); + if (is_constant(f)) { + expr new_f = visit(f); + bool modified = new_f != f; + buffer new_args; + get_app_args(e, new_args); + for (unsigned i = 0; i < new_args.size(); i++) { + expr arg = new_args[i]; + new_args[i] = visit(arg); + if (!modified && new_args[i] != arg) + modified = true; + } + if (is_lambda(new_f)) { + std::reverse(new_args.begin(), new_args.end()); + return apply_beta(new_f, new_args.size(), new_args.data()); + } else if (modified) { + return mk_app(new_f, new_args); + } else { + return e; + } + } else { + return replace_visitor::visit_app(e); + } + } +public: + unfold_core_fn():m_unfolded(false) {} + bool unfolded() const { return m_unfolded; } +}; + +class unfold_fn : public unfold_core_fn { +protected: + name const & m_name; + level_param_names const & m_ps; + expr const & m_def; + + virtual expr visit_constant(expr const & c) { + if (const_name(c) == m_name) { + m_unfolded = true; + return instantiate_univ_params(m_def, m_ps, const_levels(c)); + } else { + return c; + } + } + +public: + unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {} +}; + +class unfold_all_fn : public unfold_core_fn { +protected: + environment m_env; + + virtual expr visit_constant(expr const & c) { + optional d = m_env.find(const_name(c)); + if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) { + m_unfolded = true; + return instantiate_value_univ_params(*d, const_levels(c)); + } else { + return c; + } + } + +public: + unfold_all_fn(environment const & env):m_env(env) {} +}; + +optional unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) { + bool reduced = false; + goals new_gs = map_goals(s, [&](goal const & g) -> optional { + expr new_meta = fn(g.get_meta()); + expr new_type = fn(g.get_type()); + if (new_meta != g.get_meta() || new_type != g.get_type()) + reduced = true; + return some(goal(new_meta, new_type)); + }); + if (reduced) { + return some(proof_state(s, new_gs)); + } else { + return none_proof_state(); + } +} + +tactic unfold_tactic(name const & n) { + return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { + optional d = env.find(n); + if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0)) + return none_proof_state(); // tactic failed + unfold_fn fn(n, d->get_univ_params(), d->get_value()); + return unfold_tactic_core(fn, s); + }); +} + +tactic unfold_tactic() { + return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { + unfold_all_fn fn(env); + return unfold_tactic_core(fn, s); + }); +} + +void initialize_unfold_tactic() { + register_tac(name({"tactic", "unfold"}), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + expr id = get_app_fn(app_arg(e)); + if (!is_constant(id)) + return fail_tactic(); + else + return unfold_tactic(const_name(id)); + }); +} +void finalize_unfold_tactic() { +} +} diff --git a/src/library/tactic/unfold_tactic.h b/src/library/tactic/unfold_tactic.h new file mode 100644 index 000000000..77f7bfbbb --- /dev/null +++ b/src/library/tactic/unfold_tactic.h @@ -0,0 +1,18 @@ +/* +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 { +/** \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. */ +tactic unfold_tactic(); + +void initialize_unfold_tactic(); +void finalize_unfold_tactic(); +}