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

fix(library/class_instance_resolution): bug when creating auxiliary meta-variables at try_instance

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-18 14:09:56 -07:00
parent 919d55b799
commit 6b4a891adb
1 changed files with 23 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/library/class_instance_resolution.cpp
View file

@ -600,15 +600,18 @@ struct cienv {
} }
virtual expr visit_meta(expr const & m) { virtual expr visit_meta(expr const & m) {
lean_assert(is_mvar(m)); if (is_mvar(m)) {
if (auto v1 = m_owner.get_assignment(m)) { if (auto v1 = m_owner.get_assignment(m)) {
if (!has_expr_metavar(*v1)) { if (!has_expr_metavar(*v1)) {
return *v1; return *v1;
} else {
expr v2 = m_owner.instantiate_uvars_mvars(*v1);
if (v2 != *v1)
m_owner.update_assignment(m, v2);
return v2;
}
} else { } else {
expr v2 = m_owner.instantiate_uvars_mvars(*v1); return m;
if (v2 != *v1)
m_owner.update_assignment(m, v2);
return v2;
} }
} else { } else {
return m; return m;
@ -871,9 +874,8 @@ struct cienv {
return lean::diagnostic(m_env, ios); return lean::diagnostic(m_env, ios);
} }
void trace(unsigned depth, expr const & mvar, expr const & r) { void trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r) {
if (!m_trace_instances) lean_assert(m_trace_instances);
return;
auto out = diagnostic(); auto out = diagnostic();
if (!m_displayed_trace_header && m_choices.size() == 1) { if (!m_displayed_trace_header && m_choices.size() == 1) {
if (m_pip) { if (m_pip) {
@ -890,7 +892,7 @@ struct cienv {
out << " "; out << " ";
if (depth > 0) if (depth > 0)
out << "[" << depth << "] "; out << "[" << depth << "] ";
out << mvar << " : " << instantiate_uvars_mvars(mlocal_type(mvar)) << " := " << r << endl; out << mvar << " : " << instantiate_uvars_mvars(mvar_type) << " := " << r << endl;
} }
bool try_instance(unsigned depth, expr const & mvar, expr const & inst, expr const & inst_type) { bool try_instance(unsigned depth, expr const & mvar, expr const & inst, expr const & inst_type) {
@ -912,16 +914,20 @@ struct cienv {
type = whnf(type); type = whnf(type);
if (!is_pi(type)) if (!is_pi(type))
break; break;
expr new_mvar = mk_mvar(binding_domain(type)); expr new_mvar = mk_mvar(Pi(locals, binding_domain(type)));
if (binding_info(type).is_inst_implicit()) { if (binding_info(type).is_inst_implicit()) {
new_inst_mvars.push_back(new_mvar); new_inst_mvars.push_back(new_mvar);
} }
r = mk_app(r, new_mvar); expr new_arg = mk_app(new_mvar, locals);
type = instantiate(binding_body(type), new_mvar); r = mk_app(r, new_arg);
type = instantiate(binding_body(type), new_arg);
} }
trace(depth, mvar, r); if (m_trace_instances) {
if (!is_def_eq(mvar_type, type)) trace(depth, mk_app(mvar, locals), mvar_type, r);
}
if (!is_def_eq(mvar_type, type)) {
return false; return false;
}
r = Fun(locals, r); r = Fun(locals, r);
assign(mvar, r); assign(mvar, r);
// copy new_inst_mvars to stack // copy new_inst_mvars to stack