refactor(library/blast): add strategy abstract object

src/library/blast/CMakeLists.txt

@@ -2,4 +2,4 @@ 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
-  simplify_actions.cpp)
+  simplify_actions.cpp strategy.cpp)

src/library/blast/blast.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/blast/proof_expr.h"
 #include "library/blast/blast_exception.h"
 #include "library/blast/simple_strategy.h"
+#include "library/blast/choice_point.h"
 
 namespace lean {
 namespace blast {
@@ -412,6 +413,7 @@ public:
         m_tctx(*this),
         m_normalizer(m_tctx) {
         init_uref_mref_href_idxs();
+        clear_choice_points();
     }
 
     ~blastenv() {

src/library/blast/choice_point.cpp

@@ -20,10 +20,10 @@ void push_choice_point(choice_point const & c) {
     get_choice_points().push_back(c);
 }
 
-action_result next_choice_point() {
+action_result next_choice_point(unsigned base) {
     auto & cs = get_choice_points();
     while (true) {
-        if (cs.empty())
+        if (cs.size() == base)
             return action_result::failed();
         action_result r = cs.back().next();
         if (!failed(r))

src/library/blast/choice_point.h

@@ -61,7 +61,7 @@ inline void push_choice_point(choice_point_cell * cell) {
     push_choice_point(choice_point(cell));
 }
 /** \brief Keep executing choice points until one of them doesn't fail. */
-action_result next_choice_point();
+action_result next_choice_point(unsigned base = 0);
 /** \brief Return size of the choice point stack */
 unsigned get_num_choice_points();
 /** \brief Shrink the size of the choice point stack.
@@ -69,4 +69,11 @@ unsigned get_num_choice_points();
 void shrink_choice_points(unsigned n);
 /** \brief Clear/remove all choice points */
 void clear_choice_points();
+
+class scope_choice_points {
+    unsigned m_num_choices;
+public:
+    scope_choice_points():m_num_choices(get_num_choice_points()) {}
+    ~scope_choice_points() { shrink_choice_points(m_num_choices); }
+};
 }}

src/library/blast/simple_strategy.cpp

@@ -14,41 +14,14 @@ Author: Leonardo de Moura
 #include "library/blast/backward_action.h"
 #include "library/blast/no_confusion_action.h"
 #include "library/blast/simplify_actions.h"
+#include "library/blast/recursor_action.h"
+#include "library/blast/strategy.h"
 
 namespace lean {
 namespace blast {
 /** \brief Implement a simple proof strategy for blast.
     We use it mainly for testing new actions and the whole blast infra-structure. */
-class simple_strategy {
+class simple_strategy : public strategy {
-    config m_config;
-
-    enum status { NoAction, ClosedBranch, Continue };
-
-    void display_msg(char const * msg) {
-        if (m_config.m_trace) {
-            ios().get_diagnostic_channel() << msg << "\n\n";
-        }
-    }
-
-    void display_action(char const * name) {
-        if (m_config.m_trace) {
-            ios().get_diagnostic_channel() << "== action: " << name << " ==>\n\n";
-        }
-    }
-
-    void display() {
-        if (m_config.m_trace) {
-            auto out = diagnostic(env(), ios());
-            out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n";
-            display_curr_state();
-        }
-    }
-
-    void display_if(action_result r) {
-        if (m_config.m_trace && !failed(r))
-            display();
-    }
-
     optional<hypothesis_idx> activate_hypothesis() {
         return curr_state().activate_hypothesis();
     }
@@ -56,7 +29,7 @@ class simple_strategy {
     /* \brief Preprocess state
        It keeps applying intros, activating and finally simplify target.
        Return an expression if the goal has been proved during preprocessing step. */
-    optional<expr> preprocess_core() {
+    virtual optional<expr> preprocess() {
         display_msg("* Preprocess");
         while (true) {
             if (intros_action())
@@ -79,20 +52,7 @@ class simple_strategy {
         return simplify_target_action().to_opt_expr();
     }
 
-    optional<expr> preprocess() {
+    virtual action_result next_action() {
-        if (auto pr = preprocess_core()) {
-            auto r = next_branch(*pr);
-            if (!solved(r)) {
-                throw exception("invalid blast preprocessing action, preprocessing actions should not create branches");
-            } else {
-                return r.to_opt_expr();
-            }
-        } else {
-            return none_expr();
-        }
-    }
-
-    action_result next_action() {
         if (intros_action()) {
             display_action("intros");
             return action_result::new_branch();
@@ -139,96 +99,6 @@ class simple_strategy {
         display_msg(">>> FAILED <<<");
         return action_result::failed();
     }
-
-    action_result next_branch(expr pr) {
-        while (curr_state().has_proof_steps()) {
-            proof_step s     = curr_state().top_proof_step();
-            action_result r  = s.resolve(unfold_hypotheses_ge(curr_state(), pr));
-            switch (r.get_kind()) {
-            case action_result::Failed:
-                display_msg(">>> next-branch FAILED <<<");
-                return r;
-            case action_result::Solved:
-                pr = r.get_proof();
-                curr_state().pop_proof_step();
-                break;
-            case action_result::NewBranch:
-                return action_result::new_branch();
-            }
-        }
-        return action_result::solved(pr);
-    }
-
-    optional<expr> search_upto(unsigned depth) {
-        if (m_config.m_trace) {
-            ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
-        }
-        display();
-        action_result r = next_action();
-        display_if(r);
-        while (true) {
-            lean_assert(curr_state().check_invariant());
-            if (curr_state().get_proof_depth() > depth) {
-                display_msg(">>> maximum search depth reached <<<");
-                r = action_result::failed();
-            }
-            switch (r.get_kind()) {
-            case action_result::Failed:
-                r = next_choice_point();
-                if (failed(r)) {
-                    // all choice points failed...
-                    display_msg(">>> proof not found, no choice points left <<<");
-                    return none_expr();
-                }
-                display_msg("* next choice point");
-                break;
-            case action_result::Solved:
-                r = next_branch(r.get_proof());
-                if (r.get_kind() == action_result::Solved) {
-                    // all branches have been solved
-                    display_msg("* found proof");
-                    return some_expr(r.get_proof());
-                }
-                display_msg("* next branch");
-                break;
-            case action_result::NewBranch:
-                r = next_action();
-                break;
-            }
-            display_if(r);
-        }
-    }
-
-    optional<expr> search() {
-        clear_choice_points();
-        curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
-        if (auto pr = preprocess())
-            return pr;
-        if (get_num_choice_points() > 0)
-            throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
-        state s    = curr_state();
-        unsigned d = m_config.m_init_depth;
-        while (true) {
-            if (auto r = search_upto(d))
-                return r;
-            d += m_config.m_inc_depth;
-            if (d > m_config.m_max_depth) {
-                display_curr_state();
-                return none_expr();
-            }
-            curr_state() = s;
-            clear_choice_points();
-        }
-    }
-
-public:
-    simple_strategy():
-        m_config(ios().get_options()) {
-    }
-
-    optional<expr> operator()() {
-        return search();
-    }
 };
 
 optional<expr> apply_simple_strategy() {

src/library/blast/strategy.cpp

@@ -0,0 +1,137 @@
+/*
+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/choice_point.h"
+#include "library/blast/blast.h"
+#include "library/blast/proof_expr.h"
+
+namespace lean {
+namespace blast {
+strategy::strategy():
+    m_config(ios().get_options()) {
+}
+
+void strategy::display_msg(char const * msg) {
+    if (m_config.m_trace) {
+        ios().get_diagnostic_channel() << msg << "\n\n";
+    }
+}
+
+void strategy::display_action(char const * name) {
+    if (m_config.m_trace) {
+        ios().get_diagnostic_channel() << "== action: " << name << " ==>\n\n";
+    }
+}
+
+void strategy::display() {
+    if (m_config.m_trace) {
+        auto out = diagnostic(env(), ios());
+        out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n";
+        display_curr_state();
+    }
+}
+
+void strategy::display_if(action_result r) {
+    if (m_config.m_trace && !failed(r))
+        display();
+}
+
+action_result strategy::next_branch(expr pr) {
+    while (curr_state().has_proof_steps()) {
+        proof_step s     = curr_state().top_proof_step();
+        action_result r  = s.resolve(unfold_hypotheses_ge(curr_state(), pr));
+        switch (r.get_kind()) {
+        case action_result::Failed:
+            display_msg(">>> next-branch FAILED <<<");
+            return r;
+        case action_result::Solved:
+            pr = r.get_proof();
+            curr_state().pop_proof_step();
+            break;
+        case action_result::NewBranch:
+            return action_result::new_branch();
+        }
+    }
+    return action_result::solved(pr);
+}
+
+optional<expr> strategy::search_upto(unsigned depth) {
+    if (m_config.m_trace) {
+        ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
+    }
+    display();
+    action_result r = next_action();
+    display_if(r);
+    while (true) {
+        lean_assert(curr_state().check_invariant());
+        if (curr_state().get_proof_depth() > depth) {
+            display_msg(">>> maximum search depth reached <<<");
+            r = action_result::failed();
+        }
+        switch (r.get_kind()) {
+        case action_result::Failed:
+            r = next_choice_point(m_init_num_choices);
+            if (failed(r)) {
+                // all choice points failed...
+                display_msg(">>> proof not found, no choice points left <<<");
+                return none_expr();
+            }
+            display_msg("* next choice point");
+            break;
+        case action_result::Solved:
+            r = next_branch(r.get_proof());
+            if (r.get_kind() == action_result::Solved) {
+                // all branches have been solved
+                display_msg("* found proof");
+                return some_expr(r.get_proof());
+            }
+            display_msg("* next branch");
+            break;
+        case action_result::NewBranch:
+            r = next_action();
+            break;
+        }
+        display_if(r);
+    }
+}
+
+optional<expr> strategy::invoke_preprocess() {
+    if (auto pr = preprocess()) {
+        auto r = next_branch(*pr);
+        if (!solved(r)) {
+            throw exception("invalid blast preprocessing action, preprocessing actions should not create branches");
+        } else {
+                return r.to_opt_expr();
+        }
+    } else {
+        return none_expr();
+    }
+}
+
+optional<expr> strategy::search() {
+    scope_choice_points scope1;
+    m_init_num_choices = get_num_choice_points();
+    curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
+    if (auto pr = invoke_preprocess())
+        return pr;
+    if (get_num_choice_points() > m_init_num_choices)
+        throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
+    state s    = curr_state();
+    unsigned d = m_config.m_init_depth;
+    while (true) {
+        if (auto r = search_upto(d))
+            return r;
+        d += m_config.m_inc_depth;
+        if (d > m_config.m_max_depth) {
+            display_curr_state();
+            return none_expr();
+        }
+        curr_state() = s;
+        shrink_choice_points(m_init_num_choices);
+    }
+}
+}}

src/library/blast/strategy.h

@@ -0,0 +1,39 @@
+/*
+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/action_result.h"
+#include "library/blast/options.h"
+
+namespace lean {
+namespace blast {
+/** Generic strategy for synthesizing proofs using the blast framework.
+    There are two main configuration options:
+
+    1- Preprocessing (preprocess method)
+    2- Next action to be performed (next_action method)
+ */
+class strategy {
+    config   m_config;
+    unsigned m_init_num_choices;
+    optional<expr> invoke_preprocess();
+protected:
+    virtual optional<expr> preprocess() = 0;
+    virtual action_result next_action() = 0;
+
+    void display_msg(char const * msg);
+    void display_action(char const * name);
+    void display();
+    void display_if(action_result r);
+
+    action_result next_branch(expr pr);
+    optional<expr> search_upto(unsigned depth);
+    optional<expr> search();
+public:
+    strategy();
+    optional<expr> operator()() { return search(); }
+};
+}}