From 9b69ccd2f802f82be77ee5c973095147db8788e8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Dec 2015 13:43:15 -0800
Subject: [PATCH] feat(library/app_builder): add trace messages to app_builder

---
 src/library/app_builder.cpp                 | 2 +-
 src/library/blast/blast.cpp                 | 5 +++++
 src/library/blast/simplifier/simplifier.cpp | 3 ++-
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 796a01ccf..f6660d6a7 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -602,7 +602,7 @@ struct app_builder::imp {
 
     void trace_inst_failure(expr const & A, char const * n) {
         lean_trace("app_builder",
-                   tout() << "failed to build instance of '" << n << "' for:\n" << A << "\n";);
+                   tout() << "failed to build instance of '" << n << "' for " << A << "\n";);
     }
 
     expr mk_partial_add(expr const & A) {
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index a82b16282..dd8594731 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/util.h"
+#include "library/trace.h"
 #include "library/reducible.h"
 #include "library/class.h"
 #include "library/constants.h"
@@ -1147,6 +1148,10 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
     return b(g);
 }
 void initialize_blast() {
+    register_trace_class("blast");
+    register_trace_class(name({"blast", "event"}));
+    register_trace_class_alias("app_builder", name({"blast", "event"}));
+    register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));
     blast::g_prefix                  = new name(name::mk_internal_unique_name());
     blast::g_tmp_prefix              = new name(name::mk_internal_unique_name());
     blast::g_ref_prefix              = new name(name::mk_internal_unique_name());
diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp
index b5f931cfe..809fbe9d9 100644
--- a/src/library/blast/simplifier/simplifier.cpp
+++ b/src/library/blast/simplifier/simplifier.cpp
@@ -914,7 +914,8 @@ result simplifier::fuse(expr const & e) {
         one = get_app_builder().mk_one(T);
         expr left_distrib = get_app_builder().mk_partial_left_distrib(T);
     } catch (app_builder_exception & ex) {
-        ios().get_diagnostic_channel() << "Cannot synthesize necessary instances\n";
+        lean_trace(name({"simplifier", "failure"}),
+                   tout() << "cannot synthesize necessary instances\n";);
         return result(e);
     }