From 453e90261b8f757b9d15c9ceb19dbea4cf30bb8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Nov 2015 12:27:24 -0800 Subject: [PATCH] refactor(library/blast): make sure all actions return action_result, add macros for simplifying strategy definition revert is not an action, but a procedure for helping us to build actions. --- src/library/blast/CMakeLists.txt | 2 +- src/library/blast/action_result.h | 5 +- src/library/blast/intros_action.cpp | 10 +- src/library/blast/intros_action.h | 8 +- src/library/blast/recursor_action.cpp | 40 ++++++- src/library/blast/recursor_action.h | 11 +- .../blast/{revert_action.cpp => revert.cpp} | 8 +- .../blast/{revert_action.h => revert.h} | 4 +- src/library/blast/simple_actions.cpp | 41 ++++--- src/library/blast/simple_actions.h | 9 +- src/library/blast/simple_strategy.cpp | 104 +++--------------- src/library/blast/subst_action.cpp | 20 ++-- src/library/blast/subst_action.h | 4 +- 13 files changed, 118 insertions(+), 148 deletions(-) rename src/library/blast/{revert_action.cpp => revert.cpp} (86%) rename src/library/blast/{revert_action.h => revert.h} (76%) diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 1c8b52ff8..284234793 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp - gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp + gexpr.cpp revert.cpp subst_action.cpp no_confusion_action.cpp simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp) diff --git a/src/library/blast/action_result.h b/src/library/blast/action_result.h index 4d7e01a6c..4e7c98408 100644 --- a/src/library/blast/action_result.h +++ b/src/library/blast/action_result.h @@ -21,9 +21,9 @@ public: private: kind m_kind; expr m_proof; +public: action_result(bool b = true):m_kind(b ? NewBranch : Failed) {} action_result(expr const & pr):m_kind(Solved), m_proof(pr) {} -public: kind get_kind() const { return m_kind; } expr get_proof() const { lean_assert(m_kind == Solved); return m_proof; } static action_result failed() { return action_result(false); } @@ -34,4 +34,7 @@ public: inline bool failed(action_result const & r) { return r.get_kind() == action_result::Failed; } inline bool solved(action_result const & r) { return r.get_kind() == action_result::Solved; } + +#define Try(Code) { action_result r = Code; if (!failed(r)) return r; } +#define TrySolve(Code) { action_result r = Code; if (solved(r)) return r.to_opt_expr(); } }} diff --git a/src/library/blast/intros_action.cpp b/src/library/blast/intros_action.cpp index e26b72547..313370730 100644 --- a/src/library/blast/intros_action.cpp +++ b/src/library/blast/intros_action.cpp @@ -23,13 +23,13 @@ struct intros_proof_step_cell : public proof_step_cell { virtual bool is_silent() const override { return true; } }; -bool intros_action(unsigned max) { +action_result intros_action(unsigned max) { if (max == 0) - return true; + return action_result::new_branch(); state & s = curr_state(); expr target = whnf(s.get_target()); if (!is_pi(target)) - return false; + return action_result::failed(); auto pcell = new intros_proof_step_cell(); s.push_proof_step(pcell); buffer new_hs; @@ -48,10 +48,10 @@ bool intros_action(unsigned max) { } pcell->m_new_hs = to_list(new_hs); s.set_target(target); - return true; + return action_result::new_branch(); } -bool intros_action() { +action_result intros_action() { return intros_action(std::numeric_limits::max()); } }} diff --git a/src/library/blast/intros_action.h b/src/library/blast/intros_action.h index 182cfea57..0e69012d2 100644 --- a/src/library/blast/intros_action.h +++ b/src/library/blast/intros_action.h @@ -5,11 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "library/blast/action_result.h" namespace lean { namespace blast { /** \brief Introduce upto \c max hypotheses. - Return false if there is nothing to introduce, that is, target is not a Pi-type. */ -bool intros_action(unsigned max); + Return failed if there is nothing to introduce, that is, target is not a Pi-type. + \remark if max == 0, and it returns new_branch. */ +action_result intros_action(unsigned max); /** \brief Keep introducing until target is not a Pi-type. */ -bool intros_action(); +action_result intros_action(); }} diff --git a/src/library/blast/recursor_action.cpp b/src/library/blast/recursor_action.cpp index 25d9d5fac..d8b7bae41 100644 --- a/src/library/blast/recursor_action.cpp +++ b/src/library/blast/recursor_action.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" #include "library/user_recursors.h" -#include "library/blast/revert_action.h" +#include "library/blast/revert.h" #include "library/blast/blast.h" namespace lean { @@ -174,7 +174,7 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) { s.collect_direct_forward_deps(hidx, to_revert); for (auto i : indices) s.collect_direct_forward_deps(href_index(i), to_revert); - revert_action(to_revert); + revert(to_revert); expr target = s.get_target(); auto target_level = get_type_context().get_level_core(target); @@ -290,4 +290,40 @@ action_result recursor_action(hypothesis_idx hidx) { } return action_result::failed(); } + +action_result recursor_preprocess_action(hypothesis_idx hidx) { + if (optional R = is_recursor_action_target(hidx)) { + unsigned num_minor = get_num_minor_premises(*R); + if (num_minor == 1) { + action_result r = recursor_action(hidx, *R); + if (!failed(r)) { + // if (!preprocess) display_action("recursor"); + return r; + } + } else { + // If the hypothesis recursor has more than 1 minor premise, we + // put it in a priority queue. + // TODO(Leo): refine + + // TODO(Leo): the following weight computation is too simple... + double w = 1.0 / (static_cast(hidx) + 1.0); + if (!is_recursive_recursor(*R)) { + // TODO(Leo): we need a better strategy for handling recursive recursors... + w += static_cast(num_minor); + curr_state().add_to_rec_queue(hidx, w); + return action_result::new_branch(); + } + } + } + return action_result::failed(); +} + +action_result recursor_action() { + while (auto hidx = curr_state().select_rec_hypothesis()) { + if (optional R = is_recursor_action_target(*hidx)) { + Try(recursor_action(*hidx, *R)); + } + } + return action_result::failed(); +} }} diff --git a/src/library/blast/recursor_action.h b/src/library/blast/recursor_action.h index 5a8f40abf..f10f84dd4 100644 --- a/src/library/blast/recursor_action.h +++ b/src/library/blast/recursor_action.h @@ -9,13 +9,6 @@ Author: Leonardo de Moura #include "library/blast/hypothesis.h" namespace lean { namespace blast { -/** \brief Return the name of the recursor that can be used with the given hypothesis */ -optional is_recursor_action_target(hypothesis_idx hidx); - -/** \brief Return the number of minor premises of the given recursor */ -unsigned get_num_minor_premises(name const & R); -bool is_recursive_recursor(name const & R); - -action_result recursor_action(hypothesis_idx hidx, name const & R); -action_result recursor_action(hypothesis_idx hidx); +action_result recursor_preprocess_action(hypothesis_idx hidx); +action_result recursor_action(); }} diff --git a/src/library/blast/revert_action.cpp b/src/library/blast/revert.cpp similarity index 86% rename from src/library/blast/revert_action.cpp rename to src/library/blast/revert.cpp index 4988cab9a..aa015fbdb 100644 --- a/src/library/blast/revert_action.cpp +++ b/src/library/blast/revert.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/blast/revert_action.h" +#include "library/blast/revert.h" #include "library/blast/blast.h" namespace lean { @@ -23,7 +23,7 @@ struct revert_proof_step_cell : public proof_step_cell { virtual bool is_silent() const override { return true; } }; -unsigned revert_action(hypothesis_idx_buffer_set & hidxs) { +unsigned revert(hypothesis_idx_buffer_set & hidxs) { state & s = curr_state(); unsigned hidxs_size = hidxs.as_buffer().size(); for (unsigned i = 0; i < hidxs_size; i++) { @@ -40,8 +40,8 @@ unsigned revert_action(hypothesis_idx_buffer_set & hidxs) { return hidxs.as_buffer().size(); } -unsigned revert_action(buffer & hidxs) { +unsigned revert(buffer & hidxs) { hypothesis_idx_buffer_set _hidxs(hidxs); - return revert_action(_hidxs); + return revert(_hidxs); } }} diff --git a/src/library/blast/revert_action.h b/src/library/blast/revert.h similarity index 76% rename from src/library/blast/revert_action.h rename to src/library/blast/revert.h index bf778019a..681f267c0 100644 --- a/src/library/blast/revert_action.h +++ b/src/library/blast/revert.h @@ -11,6 +11,6 @@ namespace lean { namespace blast { /** \brief Revert the given hypotheses and their dependencies. Return the total number of hypotheses reverted. */ -unsigned revert_action(buffer & hidxs); -unsigned revert_action(hypothesis_idx_buffer_set & hidxs); +unsigned revert(buffer & hidxs); +unsigned revert(hypothesis_idx_buffer_set & hidxs); }} diff --git a/src/library/blast/simple_actions.cpp b/src/library/blast/simple_actions.cpp index d5196b9b0..a1b6629ac 100644 --- a/src/library/blast/simple_actions.cpp +++ b/src/library/blast/simple_actions.cpp @@ -11,16 +11,16 @@ Author: Leonardo de Moura namespace lean { namespace blast { // TODO(Leo): we should create choice points when there are meta-variables -optional assumption_action() { +action_result assumption_action() { state const & s = curr_state(); expr const & target = s.get_target(); for (hypothesis_idx hidx : s.get_head_related()) { hypothesis const * h = s.get_hypothesis_decl(hidx); lean_assert(h); if (is_def_eq(h->get_type(), target)) - return some_expr(h->get_self()); + return action_result(h->get_self()); } - return none_expr(); + return action_result::failed(); } /* Close branch IF h is of the form (H : a ~ a) where ~ is a reflexive relation */ @@ -39,20 +39,20 @@ static optional try_not_refl_relation(hypothesis const & h) { return none_expr(); } -optional assumption_contradiction_actions(hypothesis_idx hidx) { +action_result assumption_contradiction_actions(hypothesis_idx hidx) { state const & s = curr_state(); app_builder & b = get_app_builder(); hypothesis const * h = s.get_hypothesis_decl(hidx); lean_assert(h); expr const & type = h->get_type(); if (blast::is_false(type)) { - return some_expr(b.mk_false_rec(s.get_target(), h->get_self())); + return action_result(b.mk_false_rec(s.get_target(), h->get_self())); } if (is_def_eq(type, s.get_target())) { - return some_expr(h->get_self()); + return action_result(h->get_self()); } if (auto pr = try_not_refl_relation(*h)) - return pr; + return action_result(*pr); expr p1 = type; bool is_neg1 = is_not(type, p1); /* try to find complement */ @@ -64,39 +64,39 @@ optional assumption_contradiction_actions(hypothesis_idx hidx) { if (is_neg1 != is_neg2) { if (is_def_eq(p1, p2)) { if (is_neg1) { - return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()})); + return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()})); } else { lean_assert(is_neg2); - return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h->get_self(), h2->get_self()})); + return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h->get_self(), h2->get_self()})); } } } } - return none_expr(); + return action_result::failed(); } -optional trivial_action() { +action_result trivial_action() { try { state s = curr_state(); expr target = s.get_target(); /* ignore if target contains meta-variables */ if (has_expr_metavar(target)) - return none_expr(); + return action_result::failed(); /* true */ if (target == mk_true()) { - return some_expr(mk_true_intro()); + return action_result(mk_true_intro()); } /* a ~ a */ name rop; expr lhs, rhs; if (is_relation_app(target, rop, lhs, rhs) && is_def_eq(lhs, rhs)) { - return some_expr(get_app_builder().mk_refl(rop, lhs)); + return action_result(get_app_builder().mk_refl(rop, lhs)); } - return none_expr(); + return action_result::failed(); } catch (app_builder_exception &) { - return none_expr(); + return action_result::failed(); } } @@ -129,4 +129,13 @@ bool discard(hypothesis_idx hidx) { } return false; } + +action_result discard_action(hypothesis_idx hidx) { + if (discard(hidx)) { + curr_state().del_hypothesis(hidx); + return action_result::new_branch(); + } else { + return action_result::failed(); + } +} }} diff --git a/src/library/blast/simple_actions.h b/src/library/blast/simple_actions.h index f4a3dccc2..a02fdd1c5 100644 --- a/src/library/blast/simple_actions.h +++ b/src/library/blast/simple_actions.h @@ -7,14 +7,15 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" #include "library/blast/hypothesis.h" +#include "library/blast/action_result.h" namespace lean { namespace blast { -optional assumption_action(); +action_result assumption_action(); /** \brief Apply assumption and contradiction actions using the given hypothesis. \remark This action is supposed to be applied when a hypothesis is activated. */ -optional assumption_contradiction_actions(hypothesis_idx hidx); +action_result assumption_contradiction_actions(hypothesis_idx hidx); /** \brief Solve trivial targets (e.g., true, a = a, a <-> a, etc). */ -optional trivial_action(); +action_result trivial_action(); /** \brief Return true if the given hypothesis is "redundant". We consider a hypothesis redundant if it is a proposition, no other hypothesis type depends on it, @@ -30,5 +31,5 @@ optional trivial_action(); (well, it may be useful for the HoTT library). TODO(Leo): subsumption. 3 is just a very simple case of subsumption. */ -bool discard(hypothesis_idx hidx); +action_result discard_action(hypothesis_idx hidx); }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index bb66b2c75..bf9e1a2c8 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -25,54 +25,13 @@ class simple_strategy : public strategy { action_result activate_hypothesis(bool preprocess) { auto hidx = curr_state().activate_hypothesis(); if (!hidx) return action_result::failed(); - if (!preprocess) display_action("activate"); - if (auto pr = assumption_contradiction_actions(*hidx)) { - if (!preprocess) display_action("assumption-contradiction"); - return action_result::solved(*pr); - } - - if (subst_action(*hidx)) { - if (!preprocess) display_action("subst"); - return action_result::new_branch(); - } - - action_result r = no_confusion_action(*hidx); - if (!failed(r)) { - if (!preprocess) display_action("no_confusion"); - return r; - } - - if (discard(*hidx)) { - if (!preprocess) display_action("discard redudant hypothesis"); - curr_state().del_hypothesis(*hidx); - return action_result::new_branch(); - } - - if (optional R = is_recursor_action_target(*hidx)) { - unsigned num_minor = get_num_minor_premises(*R); - if (num_minor == 1) { - action_result r = recursor_action(*hidx, *R); - if (!failed(r)) { - if (!preprocess) display_action("recursor"); - return r; - } - } else { - // If the hypothesis recursor has more than 1 minor premise, we - // put it in a priority queue. - // TODO(Leo): refine - - // TODO(Leo): the following weight computation is too simple... - double w = 1.0 / (static_cast(*hidx) + 1.0); - if (!is_recursive_recursor(*R)) { - // TODO(Leo): we need a better strategy for handling recursive recursors... - w += static_cast(num_minor); - curr_state().add_to_rec_queue(*hidx, w); - } - } - } - + Try(assumption_contradiction_actions(*hidx)); + Try(subst_action(*hidx)); + Try(no_confusion_action(*hidx)); + Try(discard_action(*hidx)); + Try(recursor_preprocess_action(*hidx)); return action_result::new_branch(); } @@ -82,57 +41,24 @@ class simple_strategy : public strategy { virtual optional preprocess() { display_msg("* Preprocess"); while (true) { - if (intros_action()) + if (!failed(intros_action())) continue; auto r = activate_hypothesis(true); if (solved(r)) return r.to_opt_expr(); if (failed(r)) break; } - if (auto pr = assumption_action()) - return pr; - return simplify_target_action().to_opt_expr(); + TrySolve(assumption_action()); + TrySolve(simplify_target_action()); + return none_expr(); } virtual action_result next_action() { - if (intros_action()) { - display_action("intros"); - return action_result::new_branch(); - } - - action_result r = activate_hypothesis(false); - if (!failed(r)) return r; - - if (auto pr = trivial_action()) { - display_action("trivial"); - return action_result::solved(*pr); - } - - if (auto pr = assumption_action()) { - // Remark: this action is only relevant - // when the target has been modified. - display_action("assumption"); - return action_result::solved(*pr); - } - - while (auto hidx = curr_state().select_rec_hypothesis()) { - if (optional R = is_recursor_action_target(*hidx)) { - r = recursor_action(*hidx, *R); - if (!failed(r)) { - display_action("recursor"); - return r; - } - } - } - - r = constructor_action(); - if (!failed(r)) { - display_action("constructor"); - return r; - } - - // TODO(Leo): add more actions... - - display_msg(">>> FAILED <<<"); + Try(intros_action()); + Try(activate_hypothesis(false)); + Try(trivial_action()); + Try(assumption_action()); + Try(recursor_action()); + Try(constructor_action()); return action_result::failed(); } }; diff --git a/src/library/blast/subst_action.cpp b/src/library/blast/subst_action.cpp index 406858dee..b2ca6adde 100644 --- a/src/library/blast/subst_action.cpp +++ b/src/library/blast/subst_action.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "library/blast/revert_action.h" +#include "library/blast/revert.h" #include "library/blast/intros_action.h" #include "library/blast/blast.h" @@ -57,7 +57,7 @@ bool subst_core(hypothesis_idx hidx) { to_revert, [&](hypothesis_idx d) { return d != hidx; }); s.collect_direct_forward_deps(hidx, to_revert); - unsigned num = revert_action(to_revert); + unsigned num = revert(to_revert); expr target = s.get_target(); expr new_target = abstract(target, h->get_self()); bool dep = !closed(new_target); @@ -84,7 +84,7 @@ bool subst_core(hypothesis_idx hidx) { } } -bool subst_action(hypothesis_idx hidx) { +action_result subst_action(hypothesis_idx hidx) { state & s = curr_state(); app_builder & b = get_app_builder(); hypothesis const * h = s.get_hypothesis_decl(hidx); @@ -92,14 +92,14 @@ bool subst_action(hypothesis_idx hidx) { expr type = h->get_type(); expr lhs, rhs; if (!is_eq(type, lhs, rhs)) - return false; + return action_result::failed(); if (is_href(rhs)) { - return subst_core(hidx); + return action_result(subst_core(hidx)); } else if (is_href(lhs)) { if (s.has_forward_deps(href_index(lhs))) { // TODO(Leo): we don't handle this case yet. // Other hypotheses depend on this equality. - return false; + return action_result::failed(); } state saved = s; try { @@ -107,17 +107,17 @@ bool subst_action(hypothesis_idx hidx) { expr new_pr = b.mk_eq_symm(h->get_self()); expr new_href = s.mk_hypothesis(new_eq, new_pr); if (subst_core(href_index(new_href))) { - return true; + return action_result::new_branch(); } else { s = saved; - return false; + return action_result::failed(); } } catch (app_builder_exception &) { s = saved; - return false; + return action_result::failed(); } } else { - return false; + return action_result::failed(); } } }} diff --git a/src/library/blast/subst_action.h b/src/library/blast/subst_action.h index d0d79ac91..94ae4ef51 100644 --- a/src/library/blast/subst_action.h +++ b/src/library/blast/subst_action.h @@ -9,6 +9,6 @@ Author: Leonardo de Moura namespace lean { namespace blast { /** \brief If the given hypothesis is of the form (H : t = x) or (H : x = s), then - eliminate x (and H). Return true if success. */ -bool subst_action(hypothesis_idx hidx); + eliminate x (and H). */ +action_result subst_action(hypothesis_idx hidx); }}