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

feat(library/blast/forward/ematch): even more tracing

Browse source
This commit is contained in:
Daniel Selsam 2016-01-26 21:37:35 -08:00 committed by Leonardo de Moura
parent 30b5313118
commit 12e148c7b6
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/blast/forward/ematch.cpp
View file

@ -388,8 +388,12 @@ struct ematch_fn {
}
bool process_match(name const & R, expr const & p, expr const & t) {
lean_trace_debug_ematch(tout() << "try process_match: "
<< ppb(p) << " <=?=> " << ppb(t) << "\n";);
lean_trace_debug_ematch(
expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t);
tout() << "try process_match: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> "
<< ppb(t) << " : " << ppb(t_type) << "\n";);
if (!is_app(p)) {
bool success = match_leaf(R, p, t);
return success;
@ -469,7 +473,7 @@ struct ematch_fn {
expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t);
tout() << "process_matchss: " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> "
tout() << "process_matchss: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> "
<< ppb(t) << " : " << ppb(t_type) << "\n";);
if (!is_metavar(p)) {
/* If p is not a metavariable we simply ignore it.