feat(library/blast/grinder): add grinder strategy

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)

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
+    };
+}
+}}

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<action_result(hypothesis_idx)> m_pre;
+    std::function<action_result(hypothesis_idx)> m_post;
+    std::function<action_result()>               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<action_result(hypothesis_idx)> const & pre,
+                        std::function<action_result(hypothesis_idx)> const & post,
+                        std::function<action_result()> const & next):
+        m_pre(pre), m_post(post), m_next(next) {}
+};
+
+strategy grind_and_then(strategy & S);
+}}