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

feat(library/unifier): when projecting give preference to most recent locals

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 09:01:29 -07:00
parent e3ab0a1d10
commit c9994ca00c
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/unifier.cpp
View file

@ -1008,8 +1008,11 @@ struct unifier_fn {
lean_assert(!is_meta(rhs)); lean_assert(!is_meta(rhs));
lean_assert(!is_app(rhs)); lean_assert(!is_app(rhs));
expr const & mtype = mlocal_type(m); expr const & mtype = mlocal_type(m);
unsigned vidx = margs.size() - 1; unsigned i = margs.size();
for (expr const & marg : margs) { while (i > 0) {
unsigned vidx = margs.size() - i;
--i;
expr const & marg = margs[i];
if (!is_local(marg) && !is_local(rhs)) { if (!is_local(marg) && !is_local(rhs)) {
// if rhs is not local, then we only add projections for the nonlocal arguments of lhs // if rhs is not local, then we only add projections for the nonlocal arguments of lhs
constraint c1 = mk_eq_cnstr(marg, rhs, j); constraint c1 = mk_eq_cnstr(marg, rhs, j);
@ -1020,7 +1023,6 @@ struct unifier_fn {
constraint c1 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j); constraint c1 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j);
alts.push_back(constraints(c1)); alts.push_back(constraints(c1));
} }
vidx--;
} }
} }
@ -1055,11 +1057,13 @@ struct unifier_fn {
expr const & f = get_app_fn(rhs); expr const & f = get_app_fn(rhs);
lean_assert(is_constant(f) || is_local(f)); lean_assert(is_constant(f) || is_local(f));
if (is_local(f)) { if (is_local(f)) {
unsigned vidx = margs.size() - 1; unsigned i = margs.size();
for (expr const & marg : margs) { while (i > 0) {
unsigned vidx = margs.size() - i;
--i;
expr const & marg = margs[i];
if (is_local(marg) && mlocal_name(marg) == mlocal_name(f)) if (is_local(marg) && mlocal_name(marg) == mlocal_name(f))
alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j)); alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j));
vidx--;
} }
} else if (is_constant(f)) { } else if (is_constant(f)) {
alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j)); alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j));