feat(library/blast): add trace module

src/library/blast/CMakeLists.txt

@@ -2,4 +2,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.cpp subst_action.cpp no_confusion_action.cpp
-  simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp)
+  simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp
+  trace.cpp)

src/library/blast/backward_action.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/blast/proof_expr.h"
 #include "library/blast/choice_point.h"
 #include "library/blast/gexpr.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -114,7 +115,7 @@ public:
     }
 };
 
-action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches) {
+action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches, char const * action_name) {
     state  s = curr_state();
     auto it  = lemmas;
     while (!empty(it)) {
@@ -124,6 +125,7 @@ action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branche
             // create choice point
             if (!empty(it))
                 push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches)));
+            trace_action(action_name);
             return r;
         }
         curr_state() = s;
@@ -131,6 +133,10 @@ action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branche
     return action_result::failed();
 }
 
+action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches) {
+    return backward_action(lemmas, prop_only_branches, "backward");
+}
+
 action_result constructor_action(bool prop_only_branches) {
     state s = curr_state();
     expr I  = get_app_fn(s.get_target());
@@ -141,6 +147,6 @@ action_result constructor_action(bool prop_only_branches) {
     buffer<gexpr> lemmas;
     for (name c_name : c_names)
         lemmas.push_back(gexpr(c_name));
-    return backward_action(to_list(lemmas), prop_only_branches);
+    return backward_action(to_list(lemmas), prop_only_branches, "constructor");
 }
 }}

src/library/blast/blast.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/blast/simple_strategy.h"
 #include "library/blast/choice_point.h"
 #include "library/blast/congruence_closure.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -757,10 +758,12 @@ struct scope_debug::imp {
     blastenv                 m_benv;
     scope_blastenv           m_scope2;
     scope_congruence_closure m_scope3;
+    scope_trace              m_scope4;
     imp(environment const & env, io_state const & ios):
         m_scope1(true),
         m_benv(env, ios, list<name>(), list<name>()),
-        m_scope2(m_benv) {
+        m_scope2(m_benv),
+        m_scope4(ios.get_options()) {
         expr aux_mvar = mk_metavar("dummy_mvar", mk_true());
         goal aux_g(aux_mvar, mlocal_type(aux_mvar));
         m_benv.init_state(aux_g);
@@ -854,6 +857,7 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
     blast::blastenv                 b(env, ios, ls, ds);
     blast::scope_blastenv           scope2(b);
     blast::scope_congruence_closure scope3;
+    blast::scope_trace              scope4(ios.get_options());
     return b(g);
 }
 void initialize_blast() {

src/library/blast/intros_action.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "library/blast/blast.h"
 #include "library/blast/proof_expr.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -48,6 +49,7 @@ action_result intros_action(unsigned max) {
     }
     pcell->m_new_hs = to_list(new_hs);
     s.set_target(target);
+    trace_action("intros");
     return action_result::new_branch();
 }
 

src/library/blast/no_confusion_action.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -92,10 +93,12 @@ action_result no_confusion_action(hypothesis_idx hidx) {
             s.push_proof_step(new no_confusion_proof_step_cell(const_name(I), target, h->get_self(), num_new_eqs));
             s.set_target(binding_domain(nct));
             s.del_hypothesis(hidx);
+            trace_action("no_confusion");
             return action_result::new_branch();
         } else {
             name nc_name(const_name(I), "no_confusion");
             expr pr = b.mk_app(nc_name, {target, lhs, rhs, h->get_self()});
+            trace_action("no_confusion");
             return action_result::solved(pr);
         }
     } catch (app_builder_exception &) {

src/library/blast/options.h

@@ -17,6 +17,7 @@ struct config {
     bool                       m_trace;
     config(options const & o);
 };
+bool get_blast_trace(options const & o);
 void initialize_options();
 void finalize_options();
 }}

src/library/blast/recursor_action.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/user_recursors.h"
 #include "library/blast/revert.h"
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -265,9 +266,10 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
         return action_result::failed(); // ill-formed recursor
 
     save_state.commit();
-
-    if (new_goals.empty())
+    trace_action("recursor");
+    if (new_goals.empty()) {
         return action_result::solved(rec);
+    }
     s.del_hypothesis(hidx);
     s.push_proof_step(new recursor_proof_step_cell(rec_info.has_dep_elim(), s.get_branch(), rec, to_list(new_goals), list<expr>()));
     s.set_target(mlocal_type(new_goals[0]));

src/library/blast/simple_actions.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/blast/util.h"
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -17,8 +18,10 @@ action_result assumption_action() {
     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))
+        if (is_def_eq(h->get_type(), target)) {
+            trace_action("assumption");
             return action_result(h->get_self());
+        }
     }
     return action_result::failed();
 }
@@ -46,13 +49,17 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
     lean_assert(h);
     expr const & type    = h->get_type();
     if (blast::is_false(type)) {
+        trace_action("contradiction");
         return action_result(b.mk_false_rec(s.get_target(), h->get_self()));
     }
     if (is_def_eq(type, s.get_target())) {
+        trace_action("assumption");
         return action_result(h->get_self());
     }
-    if (auto pr = try_not_refl_relation(*h))
+    if (auto pr = try_not_refl_relation(*h)) {
+        trace_action("contradiction");
         return action_result(*pr);
+    }
     expr p1 = type;
     bool is_neg1 = is_not(type, p1);
     /* try to find complement */
@@ -63,6 +70,7 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
         bool is_neg2 = is_not(type2, p2);
         if (is_neg1 != is_neg2) {
             if (is_def_eq(p1, p2)) {
+                trace_action("contradiction");
                 if (is_neg1) {
                     return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()}));
                 } else {
@@ -85,12 +93,14 @@ action_result trivial_action() {
 
         /* true */
         if (target == mk_true()) {
+            trace_action("trivial");
             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)) {
+            trace_action("trivial");
             return action_result(get_app_builder().mk_refl(rop, lhs));
         }
 
@@ -133,6 +143,7 @@ bool discard(hypothesis_idx hidx) {
 action_result discard_action(hypothesis_idx hidx) {
     if (discard(hidx)) {
         curr_state().del_hypothesis(hidx);
+        trace_action("discard");
         return action_result::new_branch();
     } else {
         return action_result::failed();

src/library/blast/simple_strategy.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/blast/simplify_actions.h"
 #include "library/blast/recursor_action.h"
 #include "library/blast/strategy.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -23,9 +24,11 @@ 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);
+
         auto hidx = curr_state().activate_hypothesis();
         if (!hidx) return action_result::failed();
-        if (!preprocess) display_action("activate");
+        trace_action("activate");
 
         Try(assumption_contradiction_actions(*hidx));
         Try(subst_action(*hidx));
@@ -39,7 +42,7 @@ class simple_strategy : public strategy {
        It keeps applying intros, activating and finally simplify target.
        Return an expression if the goal has been proved during preprocessing step. */
     virtual optional<expr> preprocess() {
-        display_msg("* Preprocess");
+        trace("* Preprocess");
         while (true) {
             if (!failed(intros_action()))
                 continue;

src/library/blast/simplify_actions.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/blast/simple_actions.h"
 #include "library/blast/blast.h"
 #include "library/blast/simplifier.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -47,6 +48,7 @@ action_result simplify_target_action() {
         return action_result::failed(); // did nothing
     s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof()));
     s.set_target(r.get_new());
+    trace_action("simplify");
     return action_result::new_branch();
 }
 }}

src/library/blast/strategy.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/blast/choice_point.h"
 #include "library/blast/blast.h"
 #include "library/blast/proof_expr.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -15,38 +16,13 @@ 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 <<<");
+            trace(">>> next-branch FAILED <<<");
             return r;
         case action_result::Solved:
             pr = r.get_proof();
@@ -60,16 +36,16 @@ action_result strategy::next_branch(expr pr) {
 }
 
 optional<expr> strategy::search_upto(unsigned depth) {
-    if (m_config.m_trace) {
+    if (is_trace_enabled()) {
         ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
     }
-    display();
+    trace_curre_state();
     action_result r = next_action();
-    display_if(r);
+    trace_curre_state_if(r);
     while (true) {
         lean_assert(curr_state().check_invariant());
         if (curr_state().get_proof_depth() > depth) {
-            display_msg(">>> maximum search depth reached <<<");
+            trace(">>> maximum search depth reached <<<");
             r = action_result::failed();
         }
         switch (r.get_kind()) {
@@ -77,25 +53,25 @@ optional<expr> strategy::search_upto(unsigned depth) {
             r = next_choice_point(m_init_num_choices);
             if (failed(r)) {
                 // all choice points failed...
-                display_msg(">>> proof not found, no choice points left <<<");
+                trace(">>> proof not found, no choice points left <<<");
                 return none_expr();
             }
-            display_msg("* next choice point");
+            trace("* 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");
+                trace("* found proof");
                 return some_expr(r.get_proof());
             }
-            display_msg("* next branch");
+            trace("* next branch");
             break;
         case action_result::NewBranch:
             r = next_action();
             break;
         }
-        display_if(r);
+        trace_curre_state_if(r);
     }
 }
 

src/library/blast/strategy.h

@@ -24,11 +24,6 @@ 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();

src/library/blast/subst_action.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/blast/revert.h"
 #include "library/blast/intros_action.h"
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -77,6 +78,7 @@ bool subst_core(hypothesis_idx hidx) {
         }
         lean_verify(s.del_hypothesis(hidx));
         lean_verify(s.del_hypothesis(href_index(rhs)));
+        trace_action("subst");
         return true;
     } catch (app_builder_exception &) {
         s = saved;

src/library/blast/trace.cpp

@@ -0,0 +1,57 @@
+/*
+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/blast.h"
+#include "library/blast/choice_point.h"
+#include "library/blast/trace.h"
+#include "library/blast/options.h"
+
+namespace lean {
+namespace blast {
+LEAN_THREAD_VALUE(bool, g_trace, false);
+
+bool is_trace_enabled() {
+    return g_trace;
+}
+
+void trace_curre_state() {
+    if (g_trace) {
+        auto out = diagnostic(env(), ios());
+        out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n";
+        display_curr_state();
+    }
+}
+
+void trace(char const * msg) {
+    if (g_trace) {
+        ios().get_diagnostic_channel() << msg << "\n\n";
+    }
+}
+
+void trace_action(char const * a) {
+    if (g_trace) {
+        ios().get_diagnostic_channel() << "== action: " << a << " ==>\n\n";
+    }
+}
+
+void trace_curre_state_if(action_result r) {
+    if (g_trace && !failed(r))
+        trace_curre_state();
+}
+
+scope_trace::scope_trace(bool enable):
+    m_old(g_trace) {
+    g_trace = enable;
+}
+
+scope_trace::scope_trace(options const & o):
+    scope_trace(get_blast_trace(o)) {
+}
+
+scope_trace::~scope_trace() {
+    g_trace = m_old;
+}
+}}

src/library/blast/trace.h

@@ -0,0 +1,23 @@
+/*
+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/action_result.h"
+
+namespace lean {
+namespace blast {
+void trace_curre_state();
+void trace(char const * msg);
+void trace_action(char const * a);
+void trace_curre_state_if(action_result r);
+bool is_trace_enabled();
+class scope_trace {
+    bool m_old;
+public:
+    scope_trace(options const & o);
+    scope_trace(bool enable);
+    ~scope_trace();
+};
+}}