diff --git a/src/library/blast/grinder/CMakeLists.txt b/src/library/blast/grinder/CMakeLists.txt index 42e6c6c8a..e2b7a3de8 100644 --- a/src/library/blast/grinder/CMakeLists.txt +++ b/src/library/blast/grinder/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(blast_grinder OBJECT init_module.cpp intro_elim_lemmas.cpp - grinder_actions.cpp) + grinder_actions.cpp grinder_strategy.cpp) diff --git a/src/library/blast/grinder/grinder_strategy.cpp b/src/library/blast/grinder/grinder_strategy.cpp new file mode 100644 index 000000000..78b66d623 --- /dev/null +++ b/src/library/blast/grinder/grinder_strategy.cpp @@ -0,0 +1,50 @@ +/* +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/unit/unit_actions.h" +#include "library/blast/actions/simple_actions.h" +#include "library/blast/actions/intros_action.h" +#include "library/blast/actions/subst_action.h" +#include "library/blast/actions/no_confusion_action.h" +#include "library/blast/actions/assert_cc_action.h" +#include "library/blast/grinder/grinder_strategy.h" +#include "library/blast/grinder/grinder_actions.h" + +namespace lean { +namespace blast { +action_result grinder_strategy_core_fn::hypothesis_pre_activation(hypothesis_idx hidx) { + Try(assumption_contradiction_actions(hidx)); + Try(no_confusion_action(hidx)); + TrySolve(assert_cc_action(hidx)); + Try(discard_action(hidx)); + Try(subst_action(hidx)); + Try(pre(hidx)); + return action_result::new_branch(); +} + +action_result grinder_strategy_core_fn::hypothesis_post_activation(hypothesis_idx hidx) { + Try(unit_propagate(hidx)); + Try(grinder_elim_action(hidx)); + Try(post(hidx)); + return action_result::new_branch(); +} + +action_result grinder_strategy_core_fn::next_action() { + Try(intros_action()); + Try(assumption_action()); + Try(activate_hypothesis()); + Try(grinder_intro_action()); + Try(next()); + return action_result::failed(); +} + +strategy grind_and_then(strategy const & S) { + return [=]() { return grinder_strategy_fn([](hypothesis_idx) { return action_result::failed(); }, // NOLINT + [](hypothesis_idx) { return action_result::failed(); }, // NOLINT + [=]() { TryStrategy(S); return action_result::failed(); })(); // NOLINT + }; +} +}} diff --git a/src/library/blast/grinder/grinder_strategy.h b/src/library/blast/grinder/grinder_strategy.h new file mode 100644 index 000000000..4b6ea0832 --- /dev/null +++ b/src/library/blast/grinder/grinder_strategy.h @@ -0,0 +1,41 @@ +/* +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/strategy.h" + +namespace lean { +namespace blast { +/** \brief Base class for grinder-like strategies. + The methods pre/post/next can be redefined to extend the set of actions + applied by the grinder. This strategy applies the grinder intro/elim actions. */ +class grinder_strategy_core_fn : public strategy_fn { + virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override; + virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override; + virtual action_result next_action() override; +protected: + virtual action_result pre(hypothesis_idx) { return action_result::failed(); } + virtual action_result post(hypothesis_idx) { return action_result::failed(); } + virtual action_result next() { return action_result::failed(); } +public: +}; + +class grinder_strategy_fn : public grinder_strategy_core_fn { + std::function m_pre; + std::function m_post; + std::function m_next; + virtual action_result pre(hypothesis_idx hidx) override { return m_pre(hidx); } + virtual action_result post(hypothesis_idx hidx) override { return m_post(hidx); } + virtual action_result next() override { return m_next(); } +public: + grinder_strategy_fn(std::function const & pre, + std::function const & post, + std::function const & next): + m_pre(pre), m_post(post), m_next(next) {} +}; + +strategy grind_and_then(strategy & S); +}}