From f9a669665a1f1cf71a9f8378016714cfcf3753ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Dec 2015 11:07:53 -0800
Subject: [PATCH] feat(library/blast/backward/backward_action): display lemma
 name in backward action

---
 .../blast/backward/backward_action.cpp        | 22 +++++++++++--------
 src/library/blast/gexpr.cpp                   |  3 ++-
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/library/blast/backward/backward_action.cpp b/src/library/blast/backward/backward_action.cpp
index 0372fd6be..089570343 100644
--- a/src/library/blast/backward/backward_action.cpp
+++ b/src/library/blast/backward/backward_action.cpp
@@ -94,12 +94,13 @@ static action_result try_lemma(gexpr const & e, bool prop_only_branches) {
 }
 
 class backward_choice_point_cell : public choice_point_cell {
-    state       m_state;
-    list<gexpr> m_lemmas;
-    bool        m_prop_only;
+    char const * m_action_name;
+    state        m_state;
+    list<gexpr>  m_lemmas;
+    bool         m_prop_only;
 public:
-    backward_choice_point_cell(state const & s, list<gexpr> const & lemmas, bool prop_only):
-        m_state(s), m_lemmas(lemmas), m_prop_only(prop_only) {}
+    backward_choice_point_cell(char const * a, state const & s, list<gexpr> const & lemmas, bool prop_only):
+        m_action_name(a), m_state(s), m_lemmas(lemmas), m_prop_only(prop_only) {}
 
     virtual action_result next() {
         while (!empty(m_lemmas)) {
@@ -107,8 +108,10 @@ public:
             gexpr lemma     = head(m_lemmas);
             m_lemmas        = tail(m_lemmas);
             action_result r = try_lemma(lemma, m_prop_only);
-            if (!failed(r))
+            if (!failed(r)) {
+                lean_trace(name({"blast", "action"}), tout() << m_action_name << " (next) " << lemma << "\n";);
                 return r;
+            }
         }
         return action_result::failed();
     }
@@ -118,13 +121,14 @@ action_result backward_action_core(list<gexpr> const & lemmas, bool prop_only_br
     state  s = curr_state();
     auto it  = lemmas;
     while (!empty(it)) {
-        action_result r = try_lemma(head(it), prop_only_branches);
+        gexpr H         = head(it);
+        action_result r = try_lemma(H, prop_only_branches);
         it              = tail(it);
         if (!failed(r)) {
             // create choice point
             if (!cut && !empty(it))
-                push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches)));
-            trace_action(action_name);
+                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";);
             return r;
         }
         curr_state() = s;
diff --git a/src/library/blast/gexpr.cpp b/src/library/blast/gexpr.cpp
index 912884579..584809c9d 100644
--- a/src/library/blast/gexpr.cpp
+++ b/src/library/blast/gexpr.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/blast/gexpr.h"
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 
 namespace lean {
 namespace blast {
@@ -36,7 +37,7 @@ std::ostream & operator<<(std::ostream & out, gexpr const & ge) {
 }
 
 io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge) {
-    out << ge.m_expr;
+    out << ppb(ge.m_expr);
     if (ge.is_universe_polymorphic()) out << " (poly)";
     return out;
 }