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

fix(library/unifier): bug in flex_rigid case: binding imitation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 20:43:49 -07:00
parent 50e21586b0
commit e55b4bf86d
2 changed files with 30 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/unifier.cpp
View file

@ -887,7 +887,7 @@ struct unifier_fn {
constraint c1 = mk_eq_cnstr(marg, rhs, j);
constraint c2 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j);
alts.push_back(constraints({c1, c2}));
} else if (is_local(marg) && marg == rhs) {
} else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
// if the argument is local, and rhs is equal to it, then we also add a projection
constraint c1 = mk_eq_cnstr(m, mk_lambda_for(mtype, mk_var(vidx)), j);
alts.push_back(constraints(c1));
@ -916,8 +916,9 @@ struct unifier_fn {
} else if (is_binding(rhs)) {
expr maux1 = mk_aux_metavar_for(mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j));
expr pi = mk_pi(binding_name(rhs), binding_domain(rhs), binding_body(rhs));
expr mtype2 = replace_range(mtype, pi); // trick for "extending" the context
expr dontcare;
expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
expr maux2 = mk_aux_metavar_for(mtype2);
expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs));
cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j));

26
tests/lua/unify7.lua Normal file
View file

@ -0,0 +1,26 @@
local env = environment()
local N = Const("N")
local P = Const("P")
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("P", mk_arrow(N, Bool)))
local a = Local("a", N)
local H = Local("H", P(a))
local t = Pi(H, Bool)
print(env:infer_type(t))
local m = mk_metavar("m", mk_arrow(N, N, Type))
local cs = { mk_eq_cnstr(m(a, a), t) }
local o = options({"unifier", "use_exceptions"}, false)
ss = unify(env, cs, o)
local n = 0
for s in ss do
print("solution: " .. tostring(s:instantiate(m)))
s:for_each_expr(function(n, v, j)
print(" " .. tostring(n) .. " := " .. tostring(v))
end)
s:for_each_level(function(n, v, j)
print(" " .. tostring(n) .. " := " .. tostring(v))
end)
n = n + 1
end
assert(n == 2)