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

@@ -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)

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(); }
 }}

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<expr> 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<unsigned>::max());
 }
 }}

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. */
+    Return failed if there is nothing to introduce, that is, target is not a Pi-type.
-bool intros_action(unsigned max);
+    \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();
 }}

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<name> 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<double>(hidx) + 1.0);
+            if (!is_recursive_recursor(*R)) {
+                // TODO(Leo): we need a better strategy for handling recursive recursors...
+                w += static_cast<double>(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<name> R = is_recursor_action_target(*hidx)) {
+            Try(recursor_action(*hidx, *R));
+        }
+    }
+    return action_result::failed();
+}
 }}

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 */
+action_result recursor_preprocess_action(hypothesis_idx hidx);
-optional<name> is_recursor_action_target(hypothesis_idx hidx);
+action_result recursor_action();
-
-/** \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);
 }}

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<hypothesis_idx> & hidxs) {
+unsigned revert(buffer<hypothesis_idx> & hidxs) {
     hypothesis_idx_buffer_set _hidxs(hidxs);
-    return revert_action(_hidxs);
+    return revert(_hidxs);
 }
 }}

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<hypothesis_idx> & hidxs);
+unsigned revert(buffer<hypothesis_idx> & hidxs);
-unsigned revert_action(hypothesis_idx_buffer_set & hidxs);
+unsigned revert(hypothesis_idx_buffer_set & hidxs);
 }}

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<expr> 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<expr> try_not_refl_relation(hypothesis const & h) {
     return none_expr();
 }
 
-optional<expr> 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<expr> 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<expr> 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();
+    }
+}
 }}

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<expr> 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<expr> 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<expr> 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<expr> 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);
 }}

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)) {
+        Try(assumption_contradiction_actions(*hidx));
-            if (!preprocess) display_action("assumption-contradiction");
+        Try(subst_action(*hidx));
-            return action_result::solved(*pr);
+        Try(no_confusion_action(*hidx));
-        }
+        Try(discard_action(*hidx));
-
+        Try(recursor_preprocess_action(*hidx));
-        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<name> 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<double>(*hidx) + 1.0);
-                if (!is_recursive_recursor(*R)) {
-                    // TODO(Leo): we need a better strategy for handling recursive recursors...
-                    w += static_cast<double>(num_minor);
-                    curr_state().add_to_rec_queue(*hidx, w);
-                }
-            }
-        }
-
         return action_result::new_branch();
     }
 
@@ -82,57 +41,24 @@ class simple_strategy : public strategy {
     virtual optional<expr> 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())
+        TrySolve(assumption_action());
-            return pr;
+        TrySolve(simplify_target_action());
-        return simplify_target_action().to_opt_expr();
+        return none_expr();
     }
 
     virtual action_result next_action() {
-        if (intros_action()) {
+        Try(intros_action());
-            display_action("intros");
+        Try(activate_hypothesis(false));
-            return action_result::new_branch();
+        Try(trivial_action());
-        }
+        Try(assumption_action());
-
+        Try(recursor_action());
-        action_result r = activate_hypothesis(false);
+        Try(constructor_action());
-        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<name> 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 <<<");
         return action_result::failed();
     }
 };

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();
     }
 }
 }}

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. */
+    eliminate x (and H). */
-bool subst_action(hypothesis_idx hidx);
+action_result subst_action(hypothesis_idx hidx);
 }}