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

fix(library/unifier): when imitating (f a), abstract local constants occurring in f

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 16:11:31 -07:00
parent 1d4352aeb4
commit a42a80407a
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/unifier.cpp
View file

@ -855,9 +855,12 @@ struct unifier_fn {
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j)); cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
sargs.push_back(mk_app_vars(maux, margs.size())); sargs.push_back(mk_app_vars(maux, margs.size()));
} }
f = abstract_locals(f, margs.size(), margs.data());
if (!has_local(f)) {
expr v = mk_app(f, sargs); expr v = mk_app(f, sargs);
v = mk_lambda_for(mtype, v); v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j)); cs.push_back(mk_eq_cnstr(m, v, j));
}
} else if (is_binding(rhs)) { } else if (is_binding(rhs)) {
expr maux1 = mk_aux_metavar_for(mtype); expr maux1 = mk_aux_metavar_for(mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j)); cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j));