max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/type_context): disable all trace messages inside type class resolution if trace.class_instances is not set to true

Browse source
This commit is contained in:
Leonardo de Moura 2017-04-25 14:16:10 -07:00
parent d0dede53f5
commit e51ff591f7
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/type_context.cpp
View file

@ -3450,9 +3450,7 @@ struct instance_synthesizer {
return ensure_no_meta(r);
}
optional<expr> operator()(expr const & type) {
lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false);
lean_trace_init_bool("class_instances", get_pp_implicit_name(), true);
optional<expr> main(expr const & type) {
auto r = mk_class_instance_core(type);
if (r) {
for (unsigned i = 0; i < m_choices.size(); i++) {
@ -3462,6 +3460,17 @@ struct instance_synthesizer {
}
return r;
}
optional<expr> operator()(expr const & type) {
if (is_trace_enabled() && !is_trace_class_enabled("class_instances")) {
scope_trace_silent scope(true);
return main(type);
} else {
lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false);
lean_trace_init_bool("class_instances", get_pp_implicit_name(), true);
return main(type);
}
}
};
static bool depends_on_mvar(expr const & e, buffer<expr> const & mvars) {