feat(library/blast): add option 'blast.recursor' for disabling recursor action

src/library/blast/options.cpp

@@ -31,6 +31,10 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEFAULT_BLAST_CC
 #define LEAN_DEFAULT_BLAST_CC true
 #endif
+#ifndef LEAN_DEFAULT_BLAST_RECURSOR
+#define LEAN_DEFAULT_BLAST_RECURSOR true
+#endif
+
 
 namespace lean {
 namespace blast {
@@ -42,6 +46,7 @@ static name * g_blast_trace        = nullptr;
 static name * g_blast_subst        = nullptr;
 static name * g_blast_simp         = nullptr;
 static name * g_blast_cc           = nullptr;
+static name * g_blast_recursor     = nullptr;
 static name * g_blast_show_failure = nullptr;
 
 unsigned get_blast_max_depth(options const & o) {
@@ -65,6 +70,9 @@ bool get_blast_simp(options const & o) {
 bool get_blast_cc(options const & o) {
     return o.get_bool(*g_blast_cc, LEAN_DEFAULT_BLAST_CC);
 }
+bool get_blast_recursor(options const & o) {
+    return o.get_bool(*g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR);
+}
 bool get_blast_show_failure(options const & o) {
     return o.get_bool(*g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE);
 }
@@ -77,6 +85,7 @@ config::config(options const & o) {
     m_subst        = get_blast_subst(o);
     m_simp         = get_blast_simp(o);
     m_cc           = get_blast_cc(o);
+    m_recursor     = get_blast_recursor(o);
     m_show_failure = get_blast_show_failure(o);
 }
 
@@ -105,6 +114,7 @@ void initialize_options() {
     g_blast_subst        = new name{"blast", "subst"};
     g_blast_simp         = new name{"blast", "simp"};
     g_blast_cc           = new name{"blast", "cc"};
+    g_blast_recursor     = new name{"blast", "recursor"};
     g_blast_show_failure = new name{"blast", "show_failure"};
 
     register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
@@ -121,6 +131,8 @@ void initialize_options() {
                          "(blast) enable simplier actions");
     register_bool_option(*blast::g_blast_cc, LEAN_DEFAULT_BLAST_CC,
                          "(blast) enable congruence closure");
+    register_bool_option(*blast::g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR,
+                         "(blast) enable recursor action");
     register_bool_option(*blast::g_blast_cc, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
                          "(blast) show failure state");
 }
@@ -132,6 +144,7 @@ void finalize_options() {
     delete g_blast_subst;
     delete g_blast_simp;
     delete g_blast_cc;
+    delete g_blast_recursor;
     delete g_blast_show_failure;
 }
 }}

src/library/blast/options.h

@@ -17,6 +17,7 @@ struct config {
     bool                       m_trace;
     bool                       m_subst;
     bool                       m_simp;
+    bool                       m_recursor;
     bool                       m_cc;
     bool                       m_show_failure;
     config(options const & o);

src/library/blast/recursor_action.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/blast/revert.h"
 #include "library/blast/blast.h"
 #include "library/blast/trace.h"
+#include "library/blast/options.h"
 
 namespace lean {
 namespace blast {
@@ -311,6 +312,8 @@ action_result recursor_action(hypothesis_idx hidx) {
 }
 
 action_result recursor_preprocess_action(hypothesis_idx hidx) {
+    if (!get_config().m_recursor)
+        return action_result::failed();
     if (optional<name> R = is_recursor_action_target(hidx)) {
         unsigned num_minor = get_num_minor_premises(*R);
         if (num_minor == 1) {
@@ -339,6 +342,8 @@ action_result recursor_preprocess_action(hypothesis_idx hidx) {
 }
 
 action_result recursor_action() {
+    if (!get_config().m_recursor)
+        return action_result::failed();
     recursor_branch_extension & ext = get_extension();
     while (true) {
         if (ext.m_rec_queue.empty())