feat(library/blast): add simp strategies

src/library/blast/simplifier/CMakeLists.txt

@@ -1 +1,2 @@
-add_library(simplifier OBJECT init_module.cpp simp_rule_set.cpp ceqv.cpp simplifier.cpp simplifier_actions.cpp)
+add_library(simplifier OBJECT init_module.cpp simp_rule_set.cpp ceqv.cpp simplifier.cpp
+  simplifier_actions.cpp simplifier_strategies.cpp)

src/library/blast/simplifier/simplifier_actions.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "library/blast/trace.h"
 #include "library/blast/options.h"
 #include "library/blast/simplifier/simplifier.h"
-#include "library/blast/actions/simple_actions.h"
+#include "library/blast/simplifier/ceqv.h"
 
 namespace lean {
 namespace blast {
@@ -121,4 +121,26 @@ action_result simplify_hypothesis_action(hypothesis_idx hidx) {
     s.del_hypothesis(hidx);
     return action_result::new_branch();
 }
+
+action_result add_simp_rule_action(hypothesis_idx hidx) {
+    if (!get_config().m_simp)
+        return action_result::failed();
+    blast_tmp_type_context ctx;
+    state & s            = curr_state();
+    hypothesis const & h = s.get_hypothesis_decl(hidx);
+    list<expr_pair> ps   = to_ceqvs(*ctx, h.get_type(), h.get_self());
+    if (!ps)
+        return action_result::failed();
+    auto & ext           = get_extension();
+    bool added           = false;
+    for (auto const & p : ps) {
+        try {
+            ext.m_srss = add(*ctx, ext.m_srss, h.get_name(), p.first, p.second, LEAN_SIMP_DEFAULT_PRIORITY);
+            added      = true;
+        } catch (exception &) {
+            // TODO(Leo, Daniel): store event
+        }
+    }
+    return added ? action_result::new_branch() : action_result::failed();
+}
 }}

src/library/blast/simplifier/simplifier_actions.h

@@ -11,6 +11,7 @@ namespace lean {
 namespace blast {
 action_result simplify_hypothesis_action(hypothesis_idx hidx);
 action_result simplify_target_action();
+action_result add_simp_rule_action(hypothesis_idx hidx);
 
 void initialize_simplifier_actions();
 void finalize_simplifier_actions();

src/library/blast/simplifier/simplifier_strategies.cpp

@@ -0,0 +1,69 @@
+/*
+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/strategy.h"
+#include "library/blast/simplifier/simplifier_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"
+
+namespace lean {
+namespace blast {
+
+class simplifier_strategy_fn : public strategy_fn {
+    bool m_simp_target;
+    bool m_simp_hyps;
+    bool m_use_hyps;
+
+    virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
+        Try(assumption_contradiction_actions(hidx));
+        if (m_simp_hyps) {
+            Try(simplify_hypothesis_action(hidx));
+        }
+        Try(no_confusion_action(hidx));
+        Try(discard_action(hidx));
+        if (m_use_hyps)
+            Try(subst_action(hidx));
+        return action_result::new_branch();
+    }
+
+    virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override {
+        if (m_use_hyps)
+            add_simp_rule_action(hidx);
+        return action_result::new_branch();
+    }
+
+    virtual action_result next_action() override {
+        if (m_simp_hyps || m_use_hyps) {
+            Try(intros_action());
+            Try(assumption_action());
+            Try(activate_hypothesis());
+        }
+        if (m_simp_target) {
+            Try(simplify_target_action());
+        }
+        Try(trivial_action());
+        return action_result::failed();
+    }
+public:
+    simplifier_strategy_fn(bool simp_target, bool simp_hyps, bool use_hyps):
+        m_simp_target(simp_target), m_simp_hyps(simp_hyps),
+        m_use_hyps(use_hyps) {}
+};
+
+strategy mk_simplify_target_strategy() {
+    return []() { return simplifier_strategy_fn(true, false, false)(); }; // NOLINT
+}
+
+strategy mk_simplify_all_strategy() {
+    return []() { return simplifier_strategy_fn(true, true, false)(); }; // NOLINT
+}
+
+strategy mk_simplify_using_hypotheses_strategy() {
+    return []() { return simplifier_strategy_fn(true, true, true)(); }; // NOLINT
+}
+}}

src/library/blast/simplifier/simplifier_strategies.h

@@ -0,0 +1,15 @@
+/*
+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 {
+strategy mk_simplify_target_strategy();
+strategy mk_simplify_all_strategy();
+strategy mk_simplify_using_hypotheses_strategy();
+}}

src/library/blast/strategies/portfolio.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include "library/blast/simplifier/simplifier_strategies.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 
@@ -14,6 +15,14 @@ static optional<expr> apply_preprocess() {
     return preprocess_and_then([]() { return none_expr(); })();
 }
 
+static optional<expr> apply_simp() {
+    return mk_simplify_using_hypotheses_strategy()();
+}
+
+static optional<expr> apply_simp_nohyps() {
+    return mk_simplify_all_strategy()();
+}
+
 static optional<expr> apply_simple() {
     return preprocess_and_then(mk_simple_strategy())();
 }
@@ -22,6 +31,10 @@ optional<expr> apply_strategy() {
     std::string s_name(get_config().m_strategy);
     if (s_name == "preprocess") {
         return apply_preprocess();
+    } else if (s_name == "simp") {
+        return apply_simp();
+    } else if (s_name == "simp_nohyps") {
+        return apply_simp_nohyps();
     } else if (s_name == "simple") {
         return apply_simple();
     } else {