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

feat(library/blast/forward/ematch): trace match-ss

Browse source
This commit is contained in:
Daniel Selsam 2016-01-23 14:50:47 -08:00 committed by Leonardo de Moura
parent 98fb43e991
commit 568b3bbeeb
1 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -465,25 +465,35 @@ struct ematch_fn {
typeof(p) and typeof(t) are subsingletons */
bool process_matchss(expr const & p, expr const & t) {
lean_assert(is_standard(env()));
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() << "process_matchss: " << 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.
We should improve this case in the future.
TODO(Leo, Daniel): add debug.blast.ematch message here */
We should improve this case in the future. */
lean_trace_debug_ematch(tout() << "(p not a metavar)\n";);
return true;
}
expr p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t);
if (m_ctx->is_def_eq(p_type, t_type)) {
return m_ctx->assign(p, t);
bool success = m_ctx->assign(p, t);
lean_trace_debug_ematch(tout() << "types are def_eq and assignment..." << (success ? "succeeded" : "failed") << "\n";);
return success;
} else {
/* Check if the types are provably equal, and cast t */
m_cc.internalize(get_eq_name(), p_type, false);
if (auto H = m_cc.get_eqv_proof(get_eq_name(), t_type, p_type)) {
expr cast_H_t = get_app_builder().mk_app(get_cast_name(), *H, t);
return m_ctx->assign(p, cast_H_t);
bool success = m_ctx->assign(p, cast_H_t);
lean_trace_debug_ematch(tout() << "types can be proved equal and assignment..." << (success ? "succeeded" : "failed") << "\n";);
return success;
}
}
/* TODO(Leo, Daniel): add debug.blast.ematch message here */
lean_trace_debug_ematch(tout() << "types cannot be proved equal\n";);
return false;
}