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

chore(library/type_context): add more trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-14 16:24:54 -08:00
parent fffe69fdf9
commit 8d64376797
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/type_context.cpp
View file

@ -2841,6 +2841,7 @@ struct instance_synthesizer {
scope_trace_env scope(m_ctx.env(), m_ctx);
trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r););
if (!m_ctx.is_def_eq(mvar_type, type)) {
lean_trace_plain("class_instances", tout() << "failed is_def_eq\n";);
return false;
}
r = locals.mk_lambda(r);
@ -2852,7 +2853,8 @@ struct instance_synthesizer {
m_state.m_stack = cons(stack_entry(new_inst_mvars[i], e.m_depth+1), m_state.m_stack);
}
return true;
} catch (exception &) {
} catch (exception & ex) {
lean_trace_plain("class_instances", tout() << "exception: " << ex.what() << "\n";);
return false;
}
}
@ -3026,6 +3028,8 @@ struct instance_synthesizer {
return r;
}
}
lean_trace("class_instances",
tout() << "trying next solution, current solution has metavars\n" << *r << "\n";);
r = next_solution();
}
}