feat(library/blast): improve trace messages

src/library/blast/actions/recursor_action.cpp

@@ -290,7 +290,7 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
         return action_result::failed(); // ill-formed recursor
 
     save_state.commit();
-    lean_trace(name({"blast", "action"}), tout() << "recursor " << R << "\n";);
+    lean_trace_action(tout() << "recursor " << R << "\n";);
     if (new_goals.empty()) {
         return action_result::solved(rec);
     }

src/library/blast/actions/simple_actions.cpp

@@ -18,14 +18,14 @@ action_result assumption_action() {
     for (hypothesis_idx hidx : s.get_head_related()) {
         hypothesis const & h = s.get_hypothesis_decl(hidx);
         if (is_def_eq(h.get_type(), target)) {
-            trace_action("assumption");
+            lean_trace_action(tout() << "assumption " << h << "\n";);
             return action_result(h.get_self());
         }
     }
     return action_result::failed();
 }
 
-/* Close branch IF h is of the form (H : a ~ a) where ~ is a reflexive relation */
+/* Close branch IF h is of the form (H : not a ~ a) where ~ is a reflexive relation */
 static optional<expr> try_not_refl_relation(hypothesis const & h) {
     expr p;
     if (!is_not(h.get_type(), p))
@@ -62,15 +62,15 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
     hypothesis const & h = s.get_hypothesis_decl(hidx);
     expr const & type    = h.get_type();
     if (blast::is_false(type)) {
-        trace_action("contradiction");
+        lean_trace_action(tout() << "contradiction " << h << "\n";);
         return action_result(b.mk_false_rec(s.get_target(), h.get_self()));
     }
     if (is_def_eq(type, s.get_target())) {
-        trace_action("assumption");
+        lean_trace_action(tout() << "assumption " << h << "\n";);
         return action_result(h.get_self());
     }
     if (auto pr = try_not_refl_relation(h)) {
-        trace_action("contradiction");
+        lean_trace_action(tout() << "contradiction " << h << "\n";);
         return action_result(*pr);
     }
     expr p1 = type;
@@ -82,7 +82,7 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
         unsigned num_not2 = consume_not(p2);
         if ((num_not1 % 2) != (num_not2 % 2)) {
             if (is_def_eq(p1, p2)) {
-                trace_action("contradiction");
+                lean_trace_action(tout() << "contradiction " << h << " " << h2 << "\n";);
                 expr pr1 = h.get_self();
                 expr pr2 = h2.get_self();
                 reduce_nots(pr1, num_not1);
@@ -158,7 +158,7 @@ bool discard(hypothesis_idx hidx) {
 action_result discard_action(hypothesis_idx hidx) {
     if (discard(hidx)) {
         curr_state().del_hypothesis(hidx);
-        trace_action("discard");
+        lean_trace_action(tout() << "discard " << curr_state().get_hypothesis_decl(hidx) << "\n";);
         return action_result::new_branch();
     } else {
         return action_result::failed();

src/library/blast/backward/backward_action.cpp

@@ -109,7 +109,7 @@ public:
             m_lemmas        = tail(m_lemmas);
             action_result r = try_lemma(lemma, m_prop_only);
             if (!failed(r)) {
-                lean_trace(name({"blast", "action"}), tout() << m_action_name << " (next) " << lemma << "\n";);
+                lean_trace_action(tout() << m_action_name << " (next) " << lemma << "\n";);
                 return r;
             }
         }
@@ -128,7 +128,7 @@ action_result backward_action_core(list<gexpr> const & lemmas, bool prop_only_br
             // create choice point
             if (!cut && !empty(it))
                 push_choice_point(choice_point(new backward_choice_point_cell(action_name, s, it, prop_only_branches)));
-            lean_trace(name({"blast", "action"}), tout() << action_name << " " << H << "\n";);
+            lean_trace_action(tout() << action_name << " " << H << "\n";);
             return r;
         }
         curr_state() = s;

src/library/blast/state.cpp

@@ -841,9 +841,9 @@ optional<unsigned> state::select_hypothesis_to_activate() {
 }
 
 void state::activate_hypothesis(hypothesis_idx hidx) {
-    lean_trace(name({"blast", "search"}),
-               hypothesis const & h = get_hypothesis_decl(hidx);
-               tout() << "activate " << h.get_name() << " : " << ppb(h.get_type()) << "\n";);
+    lean_trace_search(
+        hypothesis const & h = get_hypothesis_decl(hidx);
+        tout() << "activate " << h.get_name() << " : " << ppb(h.get_type()) << "\n";);
     m_branch.m_active.insert(hidx);
     update_indices(hidx);
 }

src/library/blast/strategy.cpp

@@ -57,7 +57,7 @@ optional<expr> strategy_fn::search() {
     m_init_num_choices        = get_num_choice_points();
     unsigned init_proof_depth = curr_state().get_proof_depth();
     unsigned max_depth        = get_config().m_max_depth;
-    lean_trace(name({"blast", "search"}), tout() << "search upto depth " << max_depth << "\n";);
+    lean_trace_search(tout() << "search upto depth " << max_depth << "\n";);
     trace_curr_state();
     trace_target();
     action_result r = next_action();

src/library/blast/trace.cpp

@@ -19,7 +19,7 @@ MK_THREAD_LOCAL_GET_DEF(expr, get_last_target);
 void trace_target() {
     if (lean_is_trace_enabled(name({"blast", "search"})) &&
         curr_state().get_target() != get_last_target()) {
-        lean_trace(name({"blast", "search"}), tout() << "target " << ppb(curr_state().get_target()) << "\n";);
+        lean_trace_search(tout() << "target " << ppb(curr_state().get_target()) << "\n";);
         get_last_target() = curr_state().get_target();
     }
 }
@@ -67,16 +67,15 @@ void trace_depth_nchoices() {
         p.second == get_num_choice_points())
         return;
     p = mk_pair(curr_state().get_proof_depth(), get_num_choice_points());
-    lean_trace(name({"blast", "search"}),
-               tout() << "depth: " << p.first << ", #choice: " << p.second << "\n";);
+    lean_trace_search(tout() << "depth: " << p.first << ", #choice: " << p.second << "\n";);
 }
 
 void trace_search(char const * msg) {
-    lean_trace(name({"blast", "search"}), tout() << msg << "\n";);
+    lean_trace_search(tout() << msg << "\n";);
 }
 
 void trace_action(char const * a) {
-    lean_trace(name({"blast", "action"}), tout() << a << "\n";);
+    lean_trace_action(tout() << a << "\n";);
 }
 
 void trace_curr_state_if(action_result r) {
@@ -89,4 +88,9 @@ io_state_stream const & operator<<(io_state_stream const & out, ppb const & e) {
     out << tmp;
     return out;
 }
+
+io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h) {
+    out << ppb(h.get_self());
+    return out;
+}
 }}

src/library/blast/trace.h

@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/trace.h"
-#include "library/blast/action_result.h"
 #include "library/io_state_stream.h"
+#include "library/blast/action_result.h"
+#include "library/blast/hypothesis.h"
 
 namespace lean {
 namespace blast {
@@ -17,6 +18,9 @@ void trace_depth_nchoices();
 void trace_action(char const * a);
 void trace_curr_state_if(action_result r);
 
+#define lean_trace_action(Code) lean_trace(name({"blast", "action"}), Code)
+#define lean_trace_search(Code) lean_trace(name({"blast", "search"}), Code)
+
 /** \brief Helper class for pretty printing blast expressions.
     It uses state::to_kernel_expr to export a blast expression
     into an expression that can be processed by the pretty printer */
@@ -26,4 +30,5 @@ struct ppb {
 };
 
 io_state_stream const & operator<<(io_state_stream const & out, ppb const & e);
+io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h);
 }}