From eefc57af2f039a71d04e4a89ed04625767e91746 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Dec 2015 18:38:36 -0800 Subject: [PATCH] feat(library/blast/grinder): add grinder actions --- src/library/blast/actions/recursor_action.h | 1 + .../blast/backward/backward_action.cpp | 12 ++-- src/library/blast/backward/backward_action.h | 3 + src/library/blast/grinder/CMakeLists.txt | 3 +- src/library/blast/grinder/grinder_actions.cpp | 65 +++++++++++++++++++ src/library/blast/grinder/grinder_actions.h | 17 +++++ src/library/blast/grinder/init_module.cpp | 3 + .../blast/grinder/intro_elim_lemmas.cpp | 37 +++++++++++ src/library/blast/grinder/intro_elim_lemmas.h | 9 ++- 9 files changed, 144 insertions(+), 6 deletions(-) create mode 100644 src/library/blast/grinder/grinder_actions.cpp create mode 100644 src/library/blast/grinder/grinder_actions.h diff --git a/src/library/blast/actions/recursor_action.h b/src/library/blast/actions/recursor_action.h index f0764f3fc..fcb03685b 100644 --- a/src/library/blast/actions/recursor_action.h +++ b/src/library/blast/actions/recursor_action.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/blast/hypothesis.h" namespace lean { namespace blast { +action_result recursor_action(hypothesis_idx hidx, name const & R); action_result recursor_preprocess_action(hypothesis_idx hidx); action_result recursor_action(); diff --git a/src/library/blast/backward/backward_action.cpp b/src/library/blast/backward/backward_action.cpp index a657204b7..0372fd6be 100644 --- a/src/library/blast/backward/backward_action.cpp +++ b/src/library/blast/backward/backward_action.cpp @@ -114,7 +114,7 @@ public: } }; -action_result backward_action(list const & lemmas, bool prop_only_branches, char const * action_name) { +action_result backward_action_core(list const & lemmas, bool prop_only_branches, char const * action_name, bool cut) { state s = curr_state(); auto it = lemmas; while (!empty(it)) { @@ -122,7 +122,7 @@ action_result backward_action(list const & lemmas, bool prop_only_branche it = tail(it); if (!failed(r)) { // create choice point - if (!empty(it)) + if (!cut && !empty(it)) push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches))); trace_action(action_name); return r; @@ -133,7 +133,11 @@ action_result backward_action(list const & lemmas, bool prop_only_branche } action_result backward_action(list const & lemmas, bool prop_only_branches) { - return backward_action(lemmas, prop_only_branches, "backward"); + return backward_action_core(lemmas, prop_only_branches, "backward", false); +} + +action_result backward_cut_action(list const & lemmas, bool prop_only_branches) { + return backward_action_core(lemmas, prop_only_branches, "backward", true); } action_result constructor_action(bool prop_only_branches) { @@ -146,6 +150,6 @@ action_result constructor_action(bool prop_only_branches) { buffer lemmas; for (name c_name : c_names) lemmas.push_back(gexpr(c_name)); - return backward_action(to_list(lemmas), prop_only_branches, "constructor"); + return backward_action_core(to_list(lemmas), prop_only_branches, "constructor", false); } }} diff --git a/src/library/blast/backward/backward_action.h b/src/library/blast/backward/backward_action.h index b9bea2434..453a5f9db 100644 --- a/src/library/blast/backward/backward_action.h +++ b/src/library/blast/backward/backward_action.h @@ -11,5 +11,8 @@ Author: Leonardo de Moura namespace lean { namespace blast { action_result backward_action(list const & lemmas, bool prop_only_branches = true); +/** Similar to previous action, but does not generate a choice point. + It commits to the first lemma that unifies with the target */ +action_result backward_cut_action(list const & lemmas, bool prop_only_branches = true); action_result constructor_action(bool prop_only_branches = true); }} diff --git a/src/library/blast/grinder/CMakeLists.txt b/src/library/blast/grinder/CMakeLists.txt index 9ba50b59b..42e6c6c8a 100644 --- a/src/library/blast/grinder/CMakeLists.txt +++ b/src/library/blast/grinder/CMakeLists.txt @@ -1 +1,2 @@ -add_library(blast_grinder OBJECT init_module.cpp intro_elim_lemmas.cpp) +add_library(blast_grinder OBJECT init_module.cpp intro_elim_lemmas.cpp + grinder_actions.cpp) diff --git a/src/library/blast/grinder/grinder_actions.cpp b/src/library/blast/grinder/grinder_actions.cpp new file mode 100644 index 000000000..b3419da21 --- /dev/null +++ b/src/library/blast/grinder/grinder_actions.cpp @@ -0,0 +1,65 @@ +/* +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/blast/blast.h" +#include "library/blast/actions/recursor_action.h" +#include "library/blast/backward/backward_action.h" +#include "library/blast/grinder/intro_elim_lemmas.h" + +namespace lean { +namespace blast { +static unsigned g_ext_id = 0; + +struct grinder_branch_extension : public branch_extension { + head_map m_intro_lemmas; + name_map m_elim_lemmas; + + grinder_branch_extension() {} + grinder_branch_extension(grinder_branch_extension const &) {} + virtual ~grinder_branch_extension() {} + virtual branch_extension * clone() override { return new grinder_branch_extension(*this); } + virtual void initialized() override { + m_intro_lemmas = mk_intro_lemma_index(); + m_elim_lemmas = mk_elim_lemma_index(); + } +}; + +void initialize_grinder_actions() { + g_ext_id = register_branch_extension(new grinder_branch_extension()); +} + +void finalize_grinder_actions() {} + +static grinder_branch_extension & get_ext() { + return static_cast(curr_state().get_extension(g_ext_id)); +} + +action_result grinder_elim_action(hypothesis_idx hidx) { + grinder_branch_extension & ext = get_ext(); + state & s = curr_state(); + hypothesis const & h = s.get_hypothesis_decl(hidx); + expr const & f = get_app_fn(h.get_type()); + if (!is_constant(f)) + return action_result::failed(); + auto R = ext.m_elim_lemmas.find(const_name(f)); + if (!R) + return action_result::failed(); + return recursor_action(hidx, *R); +} + +action_result grinder_intro_action() { + grinder_branch_extension & ext = get_ext(); + state & s = curr_state(); + expr const & target = s.get_target(); + expr const & f = get_app_fn(target); + if (!is_constant(f)) + return action_result::failed(); + list const * lemmas = ext.m_intro_lemmas.find(head_index(f)); + if (!lemmas) + return action_result::failed(); + return backward_cut_action(*lemmas); +} +}} diff --git a/src/library/blast/grinder/grinder_actions.h b/src/library/blast/grinder/grinder_actions.h new file mode 100644 index 000000000..23c570454 --- /dev/null +++ b/src/library/blast/grinder/grinder_actions.h @@ -0,0 +1,17 @@ +/* +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/blast/action_result.h" +#include "library/blast/hypothesis.h" + +namespace lean { +namespace blast { +action_result grinder_elim_action(hypothesis_idx hidx); +action_result grinder_intro_action(); +void initialize_grinder_actions(); +void finalize_grinder_actions(); +}} diff --git a/src/library/blast/grinder/init_module.cpp b/src/library/blast/grinder/init_module.cpp index c4b4c6bf7..ca153d57d 100644 --- a/src/library/blast/grinder/init_module.cpp +++ b/src/library/blast/grinder/init_module.cpp @@ -6,14 +6,17 @@ Author: Leonardo de Moura */ #include "library/blast/grinder/init_module.h" #include "library/blast/grinder/intro_elim_lemmas.h" +#include "library/blast/grinder/grinder_actions.h" namespace lean { namespace blast { void initialize_grinder_module() { initialize_intro_elim_lemmas(); + initialize_grinder_actions(); } void finalize_grinder_module() { + finalize_grinder_actions(); finalize_intro_elim_lemmas(); } }} diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp index 4927ca839..ec24f93ad 100644 --- a/src/library/blast/grinder/intro_elim_lemmas.cpp +++ b/src/library/blast/grinder/intro_elim_lemmas.cpp @@ -11,6 +11,8 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/user_recursors.h" #include "library/tmp_type_context.h" +#include "library/blast/blast.h" +#include "library/blast/grinder/intro_elim_lemmas.h" namespace lean { static name * g_class_name = nullptr; @@ -119,4 +121,39 @@ void finalize_intro_elim_lemmas() { delete g_key; delete g_class_name; } + +namespace blast { +head_map mk_intro_lemma_index() { + head_map r; + buffer lemmas; + blast_tmp_type_context ctx; + get_intro_lemmas(env(), lemmas); + unsigned i = lemmas.size(); + while (i > 0) { + --i; + ctx->clear(); + optional target = get_intro_target(*ctx, lemmas[i]); + if (!target) { + // TODO(Leo): generate event + } else { + r.insert(head_index(*target), gexpr(lemmas[i])); + } + } + return r; } + +name_map mk_elim_lemma_index() { + name_map r; + buffer lemmas; + get_elim_lemmas(env(), lemmas); + for (name const & lemma : lemmas) { + try { + recursor_info info = get_recursor_info(env(), lemma); + r.insert(info.get_type_name(), lemma); + } catch (exception &) { + // TODO(Leo): generate event + } + } + return r; +} +}} diff --git a/src/library/blast/grinder/intro_elim_lemmas.h b/src/library/blast/grinder/intro_elim_lemmas.h index 7dd7b05dc..a409b7c32 100644 --- a/src/library/blast/grinder/intro_elim_lemmas.h +++ b/src/library/blast/grinder/intro_elim_lemmas.h @@ -7,6 +7,8 @@ Author: Leonardo de Moura #pragma once #include "kernel/environment.h" #include "library/io_state.h" +#include "library/head_map.h" +#include "library/blast/gexpr.h" #ifndef LEAN_ELIM_DEFAULT_PRIORITY #define LEAN_ELIM_DEFAULT_PRIORITY 1000 @@ -25,4 +27,9 @@ void get_elim_lemmas(environment const & env, buffer & r); void get_intro_lemmas(environment const & env, buffer & r); void initialize_intro_elim_lemmas(); void finalize_intro_elim_lemmas(); -} +namespace blast { +/* The following indices are based on blast current set of opaque/reducible constants. They + must be rebuilt whenever a key is "unfolded by blast */ +head_map mk_intro_lemma_index(); +name_map mk_elim_lemma_index(); +}}