From d915f0cc32d913ba7173f7eaf4cbeae4b4f4bad7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Jun 2014 09:00:14 -0700 Subject: [PATCH] refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 5 ----- tests/lua/tc7.lua | 6 +++--- tests/lua/tc_bug1.lua | 8 ++------ tests/lua/unify3.lua | 4 +--- 4 files changed, 6 insertions(+), 17 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 1b1a05117..b25351e4f 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -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; } diff --git a/tests/lua/tc7.lua b/tests/lua/tc7.lua index 77af56ffb..80f9e2e1a 100644 --- a/tests/lua/tc7.lua +++ b/tests/lua/tc7.lua @@ -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))) diff --git a/tests/lua/tc_bug1.lua b/tests/lua/tc_bug1.lua index 4149f2582..013116539 100644 --- a/tests/lua/tc_bug1.lua +++ b/tests/lua/tc_bug1.lua @@ -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))) diff --git a/tests/lua/unify3.lua b/tests/lua/unify3.lua index 653902494..4e4bfdf84 100644 --- a/tests/lua/unify3.lua +++ b/tests/lua/unify3.lua @@ -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)())