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

refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-24 09:00:14 -07:00
parent d8a8300a4f
commit d915f0cc32
4 changed files with 6 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/converter.cpp
View file

@ -445,11 +445,6 @@ struct default_converter : public converter {
}
}
if (has_metavar(t_n) || has_metavar(s_n)) {
add_cnstr(c, mk_eq_cnstr(t_n, s_n, jst.get()));
return true;
}
return false;
}

6
tests/lua/tc7.lua
View file

@ -14,9 +14,9 @@ local m1 = mk_metavar("m1", N)
local cs = {}
local ngen = name_generator("tst")
local tc = type_checker(env, ngen, function (c) print(c); cs[#cs+1] = c end)
assert(tc:is_def_eq(f(m1), g(a)))
assert(tc:is_def_eq(f(m1), a))
assert(not tc:is_def_eq(f(m1), g(a)))
assert(not tc:is_def_eq(f(m1), a))
assert(not tc:is_def_eq(f(a), a))
assert(tc:is_def_eq(mk_lambda("x", N, Var(0)), h(m1)))
assert(not tc:is_def_eq(mk_lambda("x", N, Var(0)), h(m1)))
assert(tc:is_def_eq(h(a), f(a)))
assert(tc:is_def_eq(h(a), f(m1)))

8
tests/lua/tc_bug1.lua
View file

@ -34,12 +34,8 @@ local ng = name_generator("foo")
local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
local m1 = mk_metavar("m1", Bool)
print("before is_def_eq")
assert(tc:is_def_eq(and_intro(m1, q(a)), and_intro(q(a), q(b))))
-- The constraint and_intro(m1, q(a)) == and_intro(q(a), q(b)) is added.
-- Reason: a unification hint may be able to solve it
assert(#cs == 1)
assert(cs[1]:lhs() == and_intro(m1, q(a)))
assert(cs[1]:rhs() == and_intro(q(a), q(b)))
assert(not tc:is_def_eq(and_intro(m1, q(a)), and_intro(q(a), q(b))))
assert(#cs == 0)
local cs = {}
local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
assert(tc:is_def_eq(foo_intro(m1, q(a), Ax1), foo_intro(q(a), q(a), Ax2)))

4
tests/lua/unify3.lua
View file

@ -12,9 +12,7 @@ env = add_decl(env, mk_var_decl("nat_group", group))
local real_group = Const("real_group")
local nat_group = Const("nat_group")
local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))
local cs = {}
local tc = type_checker(env, name_generator("foo"), function (c) print(c); cs[#cs+1] = c end)
assert(tc:is_def_eq(carrier(m), real))
local cs = { mk_eq_cnstr(carrier(m), real) }
local o = options({"unifier", "use_exceptions"}, false)
print(o)
assert(not unify(env, cs, o)())