michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/app_builder): add trace messages to app_builder

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 13:43:15 -08:00
parent 9df10a4048
commit 9b69ccd2f8
3 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/app_builder.cpp
View file

@ -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) {

5
src/library/blast/blast.cpp
View file

@ -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());

3
src/library/blast/simplifier/simplifier.cpp
View file

@ -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);
}