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

perf(library/unifier): do not explore branches that will trigger type errors

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-05 20:16:16 -07:00
parent bbc4380a52
commit da616f69ea
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/unifier.cpp
View file

@ -1392,7 +1392,8 @@ struct unifier_fn {
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) { if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
// Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them. // Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
// The unifier assumes the eq constraints are reduced. // The unifier assumes the eq constraints are reduced.
if (m_tc[relax]->is_def_eq(marg, rhs, j, cs)) { if (m_tc[relax]->is_def_eq_types(marg, rhs, j, cs) &&
m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx)); expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j, relax)); cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end())); alts.push_back(to_list(cs.begin(), cs.end()));