refactor(library/blast): move recursor action and strategy to its own directory

src/CMakeLists.txt

@@ -355,6 +355,8 @@ add_subdirectory(library/blast/actions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_actions>)
 add_subdirectory(library/blast/strategies)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_strategies>)
+add_subdirectory(library/blast/recursor)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_recursor>)
 add_subdirectory(library/blast/grinder)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_grinder>)
 add_subdirectory(library/blast/simplifier)

src/library/blast/actions/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(blast_actions OBJECT init_module.cpp simple_actions.cpp
   intros_action.cpp subst_action.cpp no_confusion_action.cpp
-  recursor_action.cpp assert_cc_action.cpp by_contradiction_action.cpp)
+  assert_cc_action.cpp by_contradiction_action.cpp)

src/library/blast/actions/init_module.cpp

@@ -4,14 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/blast/actions/recursor_action.h"
-
 namespace lean {
 namespace blast {
 void initialize_actions_module() {
-    initialize_recursor_action();
 }
 void finalize_actions_module() {
-    finalize_recursor_action();
 }
 }}

src/library/blast/grinder/grinder_actions.cpp

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/blast/blast.h"
 #include "library/blast/trace.h"
-#include "library/blast/actions/recursor_action.h"
+#include "library/blast/recursor/recursor_action.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/grinder/intro_elim_lemmas.h"
 

src/library/blast/init_module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/blast/congruence_closure.h"
 #include "library/blast/discr_tree.h"
 #include "library/blast/simplifier/init_module.h"
+#include "library/blast/recursor/init_module.h"
 #include "library/blast/backward/init_module.h"
 #include "library/blast/forward/init_module.h"
 #include "library/blast/unit/init_module.h"
@@ -30,10 +31,12 @@ void initialize_blast_module() {
     initialize_blast_tactic();
     blast::initialize_actions_module();
     blast::initialize_congruence_closure();
+    blast::initialize_recursor_module();
     blast::initialize_grinder_module();
 }
 void finalize_blast_module() {
     blast::finalize_grinder_module();
+    blast::finalize_recursor_module();
     blast::finalize_congruence_closure();
     blast::finalize_actions_module();
     finalize_blast_tactic();

src/library/blast/recursor/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(blast_recursor OBJECT init_module.cpp recursor_action.cpp recursor_strategy.cpp)

src/library/blast/recursor/init_module.cpp

@@ -0,0 +1,18 @@
+/*
+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/recursor/recursor_action.h"
+#include "library/blast/recursor/recursor_strategy.h"
+
+namespace lean {
+namespace blast {
+void initialize_recursor_module() {
+    initialize_recursor_action();
+}
+void finalize_recursor_module() {
+    finalize_recursor_action();
+}
+}}

src/library/blast/recursor/init_module.h

@@ -0,0 +1,12 @@
+/*
+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
+namespace lean {
+namespace blast {
+void initialize_recursor_module();
+void finalize_recursor_module();
+}}

src/library/blast/recursor/recursor_strategy.cpp

@@ -10,8 +10,8 @@ Author: Leonardo de Moura
 #include "library/blast/trace.h"
 #include "library/blast/choice_point.h"
 #include "library/blast/actions/intros_action.h"
-#include "library/blast/actions/recursor_action.h"
-#include "library/blast/strategies/rec_strategy.h"
+#include "library/blast/recursor/recursor_action.h"
+#include "library/blast/recursor/recursor_strategy.h"
 
 namespace lean {
 namespace blast {

src/library/blast/strategies/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(blast_strategies OBJECT simple_strategy.cpp iterative_deepening.cpp
-  preprocess_strategy.cpp action_strategy.cpp rec_strategy.cpp portfolio.cpp)
+  preprocess_strategy.cpp action_strategy.cpp portfolio.cpp)

src/library/blast/strategies/portfolio.cpp

@@ -10,13 +10,13 @@ Author: Leonardo de Moura
 #include "library/blast/simplifier/simplifier_strategies.h"
 #include "library/blast/unit/unit_actions.h"
 #include "library/blast/forward/ematch.h"
+#include "library/blast/recursor/recursor_strategy.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/backward/backward_strategy.h"
 #include "library/blast/grinder/grinder_strategy.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 #include "library/blast/strategies/action_strategy.h"
-#include "library/blast/strategies/rec_strategy.h"
 
 namespace lean {
 namespace blast {

src/library/blast/strategies/preprocess_strategy.cpp

@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "library/blast/actions/subst_action.h"
 #include "library/blast/actions/no_confusion_action.h"
 #include "library/blast/actions/assert_cc_action.h"
-#include "library/blast/actions/recursor_action.h"
+#include "library/blast/recursor/recursor_action.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 
 namespace lean {

src/library/blast/strategies/simple_strategy.cpp

@@ -10,19 +10,19 @@ Author: Leonardo de Moura
 #include "library/blast/proof_expr.h"
 #include "library/blast/strategy.h"
 #include "library/blast/trace.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/by_contradiction_action.h"
+#include "library/blast/actions/assert_cc_action.h"
+#include "library/blast/actions/no_confusion_action.h"
+#include "library/blast/recursor/recursor_action.h"
 #include "library/blast/simplifier/simplifier_actions.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/backward/backward_strategy.h"
 #include "library/blast/forward/forward_actions.h"
 #include "library/blast/forward/ematch.h"
 #include "library/blast/unit/unit_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/recursor_action.h"
-#include "library/blast/actions/by_contradiction_action.h"
-#include "library/blast/actions/assert_cc_action.h"
-#include "library/blast/actions/no_confusion_action.h"
 
 namespace lean {
 namespace blast {