From 57c9ced111a6c955d6fd4aa59bf13ee763e23628 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jan 2016 17:18:05 -0800
Subject: [PATCH] feat(library/blast): add fail_action and fail_strategy helper
 functions

---
 src/library/blast/actions/simple_actions.cpp |  8 ++++++++
 src/library/blast/actions/simple_actions.h   |  5 +++++
 src/library/blast/strategies/portfolio.cpp   | 10 ++++++----
 src/library/blast/strategy.cpp               |  4 ++++
 src/library/blast/strategy.h                 |  3 +++
 5 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/src/library/blast/actions/simple_actions.cpp b/src/library/blast/actions/simple_actions.cpp
index b55f7f4089..08c276bc75 100644
--- a/src/library/blast/actions/simple_actions.cpp
+++ b/src/library/blast/actions/simple_actions.cpp
@@ -11,6 +11,14 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
+action_result fail_action() {
+    return action_result::failed();
+}
+
+action_result fail_action_h(hypothesis_idx) {
+    return action_result::failed();
+}
+
 // TODO(Leo): we should create choice points when there are meta-variables
 action_result assumption_action() {
     state const & s     = curr_state();
diff --git a/src/library/blast/actions/simple_actions.h b/src/library/blast/actions/simple_actions.h
index a02fdd1c56..315ae4e363 100644
--- a/src/library/blast/actions/simple_actions.h
+++ b/src/library/blast/actions/simple_actions.h
@@ -10,6 +10,11 @@ Author: Leonardo de Moura
 #include "library/blast/action_result.h"
 namespace lean {
 namespace blast {
+/** \brief Actions that always fails */
+action_result fail_action();
+action_result fail_action_h(hypothesis_idx);
+
+/** \brief Apply 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. */
diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index 2eb3331275..7ce5d630c4 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include "util/sstream.h"
+#include "library/blast/strategy.h"
+#include "library/blast/actions/simple_actions.h"
 #include "library/blast/actions/assert_cc_action.h"
 #include "library/blast/actions/no_confusion_action.h"
 #include "library/blast/unit/unit_actions.h"
@@ -22,7 +24,7 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 static optional<expr> apply_preprocess() {
-    return preprocess_and_then([]() { return none_expr(); })();
+    return preprocess_and_then(fail_strategy())();
 }
 
 static optional<expr> apply_simp() {
@@ -85,15 +87,15 @@ static optional<expr> apply_unit() {
     return mk_action_strategy("unit",
                               unit_preprocess,
                               unit_propagate,
-                              []() { return action_result::failed(); })();
+                              fail_action)();
 }
 
 static optional<expr> apply_grind() {
-    return preprocess_and_then(grind_and_then([]() { return none_expr(); }))();
+    return preprocess_and_then(grind_and_then(fail_strategy()))();
 }
 
 static optional<expr> apply_core_grind() {
-    return grind_and_then([]() { return none_expr(); })();
+    return grind_and_then(fail_strategy())();
 }
 
 optional<expr> apply_strategy() {
diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp
index 084aaa9c3a..9123bfb02e 100644
--- a/src/library/blast/strategy.cpp
+++ b/src/library/blast/strategy.cpp
@@ -111,4 +111,8 @@ strategy operator||(strategy const & s1, strategy const & s2) {
             return s2();
     };
 }
+
+strategy fail_strategy() {
+    return []() { return none_expr(); }; // NOLINT
+}
 }}
diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h
index 66cf0e0ba2..46508d54e8 100644
--- a/src/library/blast/strategy.h
+++ b/src/library/blast/strategy.h
@@ -44,5 +44,8 @@ public:
 
 typedef std::function<optional<expr>()> strategy;
 
+/** \brief Strategy that always returns none_expr */
+strategy fail_strategy();
+
 strategy operator||(strategy const & s1, strategy const & s2);
 }}