fix(library/blast): spurious trace messages, typo

src/library/blast/backward/backward_strategy.cpp

@@ -71,6 +71,7 @@ class backward_strategy : public strategy {
         Try(assumption_action());
         list<gexpr> backward_rules = get_extension().get_backward_rule_set().find(head_index(curr_state().get_target()));
         Try(backward_action(backward_rules, true));
+        Try(constructor_action());
         return action_result::failed();
     }
 };

src/library/blast/simple_strategy.cpp

@@ -25,7 +25,7 @@ namespace blast {
     We use it mainly for testing new actions and the whole blast infra-structure. */
 class simple_strategy : public strategy {
     action_result activate_hypothesis(bool preprocess) {
-        scope_trace scope(!preprocess);
+        scope_trace scope(!preprocess && cfg().m_trace);
 
         auto hidx = curr_state().activate_hypothesis();
         if (!hidx) return action_result::failed();

src/library/blast/strategy.cpp

@@ -39,9 +39,9 @@ optional<expr> strategy::search_upto(unsigned depth) {
     if (is_trace_enabled()) {
         ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
     }
-    trace_curre_state();
+    trace_curr_state();
     action_result r = next_action();
-    trace_curre_state_if(r);
+    trace_curr_state_if(r);
     while (true) {
         lean_assert(curr_state().check_invariant());
         if (curr_state().get_proof_depth() > depth) {
@@ -71,7 +71,7 @@ optional<expr> strategy::search_upto(unsigned depth) {
             r = next_action();
             break;
         }
-        trace_curre_state_if(r);
+        trace_curr_state_if(r);
     }
 }
 
@@ -103,7 +103,7 @@ optional<expr> strategy::search() {
             return r;
         d += m_config.m_inc_depth;
         if (d > m_config.m_max_depth) {
-            display_curr_state();
+            trace_curr_state();
             return none_expr();
         }
         curr_state() = s;

src/library/blast/strategy.h

@@ -32,6 +32,7 @@ protected:
 public:
     strategy();
     optional<expr> operator()() { return search(); }
+    config cfg() const { return m_config; }
 };
 
 #define TryStrategy(Code) {\

src/library/blast/trace.cpp

@@ -17,7 +17,7 @@ bool is_trace_enabled() {
     return g_trace;
 }
 
-void trace_curre_state() {
+void trace_curr_state() {
     if (g_trace) {
         auto out = diagnostic(env(), ios());
         out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n";
@@ -37,9 +37,9 @@ void trace_action(char const * a) {
     }
 }
 
-void trace_curre_state_if(action_result r) {
+void trace_curr_state_if(action_result r) {
     if (g_trace && !failed(r))
-        trace_curre_state();
+        trace_curr_state();
 }
 
 scope_trace::scope_trace(bool enable):

src/library/blast/trace.h

@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-void trace_curre_state();
+void trace_curr_state();
 void trace(char const * msg);
 void trace_action(char const * a);
-void trace_curre_state_if(action_result r);
+void trace_curr_state_if(action_result r);
 bool is_trace_enabled();
 class scope_trace {
     bool m_old;