From 16bdc51fc49929674bbd1240df633c884e454712 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 13:35:36 -0700 Subject: [PATCH] refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 10 +++- src/kernel/type_checker.cpp | 83 ++++++++++++------------------- src/kernel/type_checker.h | 56 +++++++-------------- src/library/kernel_bindings.cpp | 45 ++++++----------- src/library/kernel_bindings.h | 1 + src/library/unifier.cpp | 47 ++++++++--------- tests/lean/run/e15.lean | 28 +++++++++++ tests/lua/expr9.lua | 8 +-- tests/lua/tc1.lua | 7 +-- tests/lua/tc2.lua | 6 +-- tests/lua/tc5.lua | 6 +-- tests/lua/tc7.lua | 3 +- tests/lua/tc8.lua | 12 +++-- tests/lua/tc_bug1.lua | 36 ++++++-------- 14 files changed, 157 insertions(+), 191 deletions(-) create mode 100644 tests/lean/run/e15.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 5d617cfd6..090520735 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -66,6 +66,11 @@ class elaborator { } }; + void consume_tc_cnstrs() { + while (auto c = m_tc.next_cnstr()) + m_constraints.push_back(*c); + } + struct choice_elaborator { elaborator & m_elab; expr m_choice; @@ -84,6 +89,7 @@ class elaborator { scope s(m_elab, m_ctx, m_subst); expr r = m_elab.visit(c); justification j = m_elab.m_accumulated; + m_elab.consume_tc_cnstrs(); list cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end()); return optional(r, j, cs); } catch (exception &) {} @@ -107,8 +113,7 @@ public: substitution const & s = substitution(), context const & ctx = context()): m_env(env), m_ios(ios), m_plugin([](constraint const &, name_generator const &) { return lazy_list>(); }), - m_ngen(ngen), m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { add_cnstr(c); }, - mk_default_converter(m_env, optional(0))), + m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional(0))), m_subst(s), m_ctx(ctx) { } @@ -530,6 +535,7 @@ public: } lazy_list solve() { + consume_tc_cnstrs(); buffer cs; cs.append(m_constraints); m_constraints.clear(); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b44023542..38fe26e6d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -24,48 +24,19 @@ Author: Leonardo de Moura namespace lean { static name g_x_name("x"); -no_constraints_allowed_exception::no_constraints_allowed_exception():exception("constraints are not allowed in this type checker") {} -exception * no_constraints_allowed_exception::clone() const { return new no_constraints_allowed_exception(); } -void no_constraints_allowed_exception::rethrow() const { throw *this; } - -add_cnstr_fn mk_no_contranint_fn() { - return add_cnstr_fn([](constraint const &) { throw no_constraints_allowed_exception(); }); -} - type_checker::scope::scope(type_checker & tc): - m_tc(tc), m_old_cs_size(m_tc.m_cs.size()), m_old_cache_cs(m_tc.m_cache_cs), m_keep(false) { - m_tc.m_infer_type_cache[0].push(); - m_tc.m_infer_type_cache[1].push(); - m_tc.m_cache_cs = true; + m_tc(tc), m_keep(false) { + m_tc.push(); } type_checker::scope::~scope() { - if (m_keep) { - // keep results - m_tc.m_infer_type_cache[0].keep(); - m_tc.m_infer_type_cache[1].keep(); - } else { - // restore caches - m_tc.m_infer_type_cache[0].pop(); - m_tc.m_infer_type_cache[1].pop(); - m_tc.m_cs.shrink(m_old_cs_size); - } - m_tc.m_cache_cs = m_old_cache_cs; + if (m_keep) + m_tc.keep(); + else + m_tc.pop(); } void type_checker::scope::keep() { m_keep = true; - if (!m_old_cache_cs) { - lean_assert(m_old_cs_size == 0); - // send results to m_add_cnstr_fn - try { - for (auto const & c : m_tc.m_cs) - m_tc.m_add_cnstr_fn(c); - } catch (...) { - m_tc.m_cs.clear(); - throw; - } - m_tc.m_cs.clear(); - } } optional type_checker::expand_macro(expr const & m) { @@ -84,10 +55,17 @@ std::pair type_checker::open_binding_body(expr const & e) { /** \brief Add given constraint using m_add_cnstr_fn. */ void type_checker::add_cnstr(constraint const & c) { - if (m_cache_cs) - m_cs.push_back(c); - else - m_add_cnstr_fn(c); + m_cs.push_back(c); +} + +optional type_checker::next_cnstr() { + if (m_cs_qhead < m_cs.size()) { + constraint c = m_cs[m_cs_qhead]; + m_cs_qhead++; + return optional(c); + } else { + return optional(); + } } /** @@ -405,15 +383,23 @@ expr type_checker::whnf(expr const & t) { } void type_checker::push() { - lean_assert(!m_cache_cs); m_infer_type_cache[0].push(); m_infer_type_cache[1].push(); + m_trail.emplace_back(m_cs.size(), m_cs_qhead); } void type_checker::pop() { - lean_assert(!m_cache_cs); m_infer_type_cache[0].pop(); m_infer_type_cache[1].pop(); + m_cs.shrink(m_trail.back().first); + m_cs_qhead = m_trail.back().second; + m_trail.pop_back(); +} + +void type_checker::keep() { + m_infer_type_cache[0].keep(); + m_infer_type_cache[1].keep(); + m_trail.pop_back(); } unsigned type_checker::num_scopes() const { @@ -421,21 +407,16 @@ unsigned type_checker::num_scopes() const { return m_infer_type_cache[0].num_scopes(); } -static add_cnstr_fn g_no_constraint_fn = mk_no_contranint_fn(); - -type_checker::type_checker(environment const & env, name_generator const & g, add_cnstr_fn const & h, - std::unique_ptr && conv, bool memoize): - m_env(env), m_gen(g), m_add_cnstr_fn(h), m_conv(std::move(conv)), m_tc_ctx(*this), - m_memoize(memoize), m_cache_cs(false) { -} - type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize): - type_checker(env, g, g_no_constraint_fn, std::move(conv), memoize) {} + m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this), + m_memoize(memoize) { + m_cs_qhead = 0; +} static name g_tmp_prefix = name::mk_internal_unique_name(); type_checker::type_checker(environment const & env): - type_checker(env, name_generator(g_tmp_prefix), g_no_constraint_fn, mk_default_converter(env), true) {} + type_checker(env, name_generator(g_tmp_prefix), mk_default_converter(env), true) {} type_checker::~type_checker() {} diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 76d296536..8452cdfc5 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -16,19 +16,6 @@ Author: Leonardo de Moura #include "kernel/converter.h" namespace lean { -typedef std::function add_cnstr_fn; - -/** \brief This handler always throw an exception (\c no_constraints_allowed_exception) when \c add_cnstr is invoked. */ -add_cnstr_fn mk_no_contranint_fn(); - -/** \brief Exception used in \c no_constraint_handler. */ -class no_constraints_allowed_exception : public exception { -public: - no_constraints_allowed_exception(); - virtual exception * clone() const; - virtual void rethrow() const; -}; - /** \brief Lean Type Checker. It can also be used to infer types, check whether a type \c A is convertible to a type \c B, etc. @@ -53,7 +40,6 @@ class type_checker { environment m_env; name_generator m_gen; - add_cnstr_fn m_add_cnstr_fn; std::unique_ptr m_conv; // In the type checker cache, we must take into account binder information. // Examples: @@ -65,7 +51,8 @@ class type_checker { // temp flag level_param_names m_params; buffer m_cs; // temporary cache of constraints - bool m_cache_cs; // true if we should cache the constraints; false if we should send to m_add_cnstr_fn + unsigned m_cs_qhead; + buffer> m_trail; friend class converter; // allow converter to access the following methods name mk_fresh_name() { return m_gen.next(); } @@ -81,18 +68,6 @@ class type_checker { expr infer_type_core(expr const & e, bool infer_only); expr infer_type(expr const & e); extension_context & get_extension() { return m_tc_ctx; } -public: - class scope { - type_checker & m_tc; - unsigned m_old_cs_size; - bool m_old_cache_cs; - bool m_keep; - public: - scope(type_checker & tc); - ~scope(); - void keep(); - }; - public: /** \brief Create a type checker for the given environment. The auxiliary names created by this @@ -100,14 +75,6 @@ public: memoize: if true, then inferred types are memoized/cached */ - type_checker(environment const & env, name_generator const & g, add_cnstr_fn const & h, std::unique_ptr && conv, - bool memoize = true); - type_checker(environment const & env, name_generator const & g, add_cnstr_fn const & h, bool memoize = true): - type_checker(env, g, h, mk_default_converter(env), memoize) {} - /** - \brief Similar to the previous constructor, but if a method tries to create a constraint, then an - exception is thrown. - */ type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize = true); type_checker(environment const & env, name_generator const & g, bool memoize = true): type_checker(env, g, mk_default_converter(env), memoize) {} @@ -157,12 +124,23 @@ public: /** \brief Mare sure type of \c e is a sort, and return it. Throw an exception otherwise. */ expr ensure_type(expr const & e) { return ensure_sort(infer(e), e); } - /** \brief Create a backtracking point for cache and generated constraints. */ - void push(); - /** \brief Restore backtracking point. */ - void pop(); /** \brief Return the number of backtracking points. */ unsigned num_scopes() const; + /** \brief Consume next constraint in the produced constraint queue */ + optional next_cnstr(); + + void push(); + void pop(); + void keep(); + + class scope { + type_checker & m_tc; + bool m_keep; + public: + scope(type_checker & tc); + ~scope(); + void keep(); + }; }; /** diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 7a4e675a3..853e739e9 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1518,7 +1518,7 @@ static void open_justification(lua_State * L) { // Constraint DECL_UDATA(constraint) - +int push_optional_constraint(lua_State * L, optional const & c) { return c ? push_constraint(L, *c) : push_nil(L); } #define CNSTR_PRED(P) static int constraint_ ## P(lua_State * L) { check_num_args(L, 1); return push_boolean(L, P(to_constraint(L, 1))); } CNSTR_PRED(is_eq_cnstr) CNSTR_PRED(is_level_eq_cnstr) @@ -1835,18 +1835,6 @@ static void open_substitution(lua_State * L) { SET_GLOBAL_FUN(substitution_pred, "is_substitution"); } -// add_cnstr_fn -add_cnstr_fn to_add_cnstr_fn(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun - luaref f(L, idx); - return add_cnstr_fn([=](constraint const & c) { - lua_State * L = f.get_state(); - f.push(); - push_constraint(L, c); - pcall(L, 1, 0, 0); - }); -} - // type_checker typedef std::shared_ptr type_checker_ref; DECL_UDATA(type_checker_ref) @@ -1863,25 +1851,13 @@ static int mk_type_checker(lua_State * L) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1))); } else if (nargs == 2) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); - } else if (nargs == 3 && lua_isfunction(L, 3)) { - return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2), - to_add_cnstr_fn(L, 3))); } else { optional mod_idx; bool memoize; name_set extra_opaque; - if (nargs == 3) { - get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque); - auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), - mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque), - memoize); - return push_type_checker_ref(L, t); - } else { - get_type_checker_args(L, 4, mod_idx, memoize, extra_opaque); - auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), - to_add_cnstr_fn(L, 3), - mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque), - memoize); - return push_type_checker_ref(L, t); - } + get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque); + auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), + mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque), + memoize); + return push_type_checker_ref(L, t); } } static int type_checker_whnf(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); } @@ -1914,7 +1890,14 @@ static int type_checker_pop(lua_State * L) { to_type_checker_ref(L, 1)->pop(); return 0; } +static int type_checker_keep(lua_State * L) { + if (to_type_checker_ref(L, 1)->num_scopes() == 0) + throw exception("invalid pop method, type_checker does not have backtracking points"); + to_type_checker_ref(L, 1)->keep(); + return 0; +} static int type_checker_num_scopes(lua_State * L) { return push_integer(L, to_type_checker_ref(L, 1)->num_scopes()); } +static int type_checker_next_cnstr(lua_State * L) { return push_optional_constraint(L, to_type_checker_ref(L, 1)->next_cnstr()); } static const struct luaL_Reg type_checker_ref_m[] = { {"__gc", type_checker_ref_gc}, @@ -1927,6 +1910,8 @@ static const struct luaL_Reg type_checker_ref_m[] = { {"is_prop", safe_function}, {"push", safe_function}, {"pop", safe_function}, + {"keep", safe_function}, + {"next_cnstr", safe_function}, {"num_scopes", safe_function}, {0, 0} }; diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index c4b0a86c8..5bd291dff 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -25,6 +25,7 @@ int push_optional_level(lua_State * L, optional const & e); int push_optional_expr(lua_State * L, optional const & e); int push_optional_justification(lua_State * L, optional const & j); int push_optional_declaration(lua_State * L, optional const & e); +int push_optional_constraint(lua_State * L, optional const & c); int push_list_expr(lua_State * L, list const & l); /** \brief Return the formatter object associated with the given Lua State. diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 6f95d4aa3..90be06047 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -284,7 +284,7 @@ struct unifier_fn { name_generator const & ngen, substitution const & s, unifier_plugin const & p, bool use_exception, unsigned max_steps): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(p), - m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { process_constraint(c); }), + m_tc(env, m_ngen.mk_child()), m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) { m_next_assumption_idx = 0; m_next_cidx = 0; @@ -936,6 +936,14 @@ struct unifier_fn { return true; } + void consume_tc_cnstrs() { + while (auto c = m_tc.next_cnstr()) { + if (in_conflict()) + return; + process_constraint(*c); + } + } + /** \brief Process the next constraint in the constraint queue m_cnstrs */ bool process_next() { lean_assert(!m_cnstrs.empty()); @@ -969,11 +977,14 @@ struct unifier_fn { // We don't throw an exception since there are no more solutions. return optional(); } - while (!m_cnstrs.empty()) { - check_system(); - lean_assert(!in_conflict()); - bool ok = process_next(); - if (!ok && !resolve_conflict()) + while (true) { + consume_tc_cnstrs(); + if (!in_conflict()) { + if (m_cnstrs.empty()) + break; + process_next(); + } + if (in_conflict() && !resolve_conflict()) return failure(); } lean_assert(!in_conflict()); @@ -1016,25 +1027,15 @@ lazy_list unify(environment const & env, unsigned num_cs, constrai lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p, unsigned max_steps) { substitution s; - buffer cs; name_generator new_ngen(ngen); - bool failed = false; - type_checker tc(env, new_ngen.mk_child(), [&](constraint const & c) { - if (!failed) { - auto r = unify_simple(s, c); - switch (r.first) { - case unify_status::Solved: - s = r.second; break; - case unify_status::Failed: - failed = true; break; - case unify_status::Unsupported: - cs.push_back(c); break; - } - } - }); - if (!tc.is_def_eq(lhs, rhs) || failed) { + type_checker tc(env, new_ngen.mk_child()); + if (!tc.is_def_eq(lhs, rhs)) return lazy_list(); - } else if (cs.empty()) { + buffer cs; + while (auto c = tc.next_cnstr()) { + cs.push_back(*c); + } + if (cs.empty()) { return lazy_list(s); } else { return unify(std::make_shared(env, cs.size(), cs.data(), ngen, s, p, false, max_steps)); diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean new file mode 100644 index 000000000..b775260d7 --- /dev/null +++ b/tests/lean/run/e15.lean @@ -0,0 +1,28 @@ +inductive nat : Type := +| zero : nat +| succ : nat → nat + +inductive list (A : Type) : Type := +| nil : list A +| cons : A → list A → list A + +check nil +check nil.{1} +check @nil.{1} nat +check @nil nat + +check cons zero nil + +inductive vector (A : Type) : nat → Type := +| vnil : vector A zero +| vcons : forall {n : nat}, A → vector A n → vector A (succ n) + +check vcons zero vnil +variable n : nat +check vcons n vnil + +check vector_rec + +definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A +:= vector_rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v + diff --git a/tests/lua/expr9.lua b/tests/lua/expr9.lua index 84216e80c..2f7ddda0e 100644 --- a/tests/lua/expr9.lua +++ b/tests/lua/expr9.lua @@ -15,11 +15,5 @@ local m3 = mk_metavar("m3", mk_metavar("m4", mk_sort(mk_meta_univ("l")))) print("step4") env:type_check(m3) print("step5") --- The following call fails, because the type checker will try to --- create a constraint, but constraint generation is not supported by --- the type checker used to implement the method type_check -assert(not pcall(function() - env:type_check(m3(a)) - end -)) +print(env:type_check(m3(a))) print("before end") diff --git a/tests/lua/tc1.lua b/tests/lua/tc1.lua index f1f4c4c4f..1536f415e 100644 --- a/tests/lua/tc1.lua +++ b/tests/lua/tc1.lua @@ -12,8 +12,7 @@ print(tc:infer(t)) local m = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("u")))) print(tc:infer(m)) -local cs = {} -local tc2 = type_checker(env, g, function (c) print(c); cs[#cs+1] = c end) +local tc2 = type_checker(env, g) local t2 = Fun(a, Bool, m(a)) print("---------") print("t2: ") @@ -22,4 +21,6 @@ print("check(t): ") print(tc2:check(t)) print("check(t2): ") print(tc2:check(t2)) -assert(#cs == 2) +assert(tc2:next_cnstr()) +assert(tc2:next_cnstr()) +assert(not tc2:next_cnstr()) diff --git a/tests/lua/tc2.lua b/tests/lua/tc2.lua index 3021441cd..13dc78a6d 100644 --- a/tests/lua/tc2.lua +++ b/tests/lua/tc2.lua @@ -52,9 +52,8 @@ print(tc:check(Fun({{A, mk_sort(u)}, {a, A}, {b, A}, {c, A}, {d, A}, trans_u(A, a, b, d, symm_u(A, b, a, H1), trans_u(A, b, c, d, H2, H3))))) -local cs = {} local g = name_generator("tst") -local tc2 = type_checker(env, g, function (c) print(c); cs[#cs+1] = c end) +local tc2 = type_checker(env, g) print("=================") local f = Const("f") local mf_ty = mk_metavar("f_ty", Pi(A, mk_sort(u), mk_sort(mk_meta_univ("l_f")))) @@ -63,8 +62,7 @@ print(tc2:check(Fun({{A, mk_sort(u)}, {f, mf_ty(A)}, {a, A}}, id_u(mA1(A, f, a), f(a), a)))) -local cs = {} -local tc2 = type_checker(env, g, function (c) print(c); cs[#cs+1] = c end) +local tc2 = type_checker(env, g) local scope = {{A, mk_sort(u)}, {a, A}, {b, A}, {c, A}, {d, A}, {H1, id_u(A, b, a)}, {H2, id_u(A, b, c)}, {H3, id_u(A, c, d)}} local mP = mk_metavar("P", Pi(scope, mk_metavar("P_ty", Pi(scope, mk_sort(mk_meta_univ("l_P"))))(A, a, b, c, d, H1, H2, H3)))(A, a, b, c, d, H1, H2, H3) diff --git a/tests/lua/tc5.lua b/tests/lua/tc5.lua index ddcc38d9b..7a495ed17 100644 --- a/tests/lua/tc5.lua +++ b/tests/lua/tc5.lua @@ -9,10 +9,8 @@ assert(tc:is_prop(Const("A"))) assert(tc:is_prop(Const("C"))) assert(not tc:is_prop(Const("T"))) assert(not tc:is_prop(Const("B2"))) -assert(not pcall(function() - print(tc:check(mk_lambda("x", mk_metavar("m", mk_metavar("t", mk_sort(mk_meta_univ("l")))), Var(0)))) - end -)) +print(tc:check(mk_lambda("x", mk_metavar("m", mk_metavar("t", mk_sort(mk_meta_univ("l")))), Var(0)))) +assert(tc:next_cnstr()) print(tc:ensure_sort(Const("B2"))) assert(not pcall(function() print(tc:ensure_sort(Const("A"))) diff --git a/tests/lua/tc7.lua b/tests/lua/tc7.lua index 80f9e2e1a..f4e65b6f9 100644 --- a/tests/lua/tc7.lua +++ b/tests/lua/tc7.lua @@ -11,9 +11,8 @@ env = add_decl(env, mk_definition("h", mk_arrow(N, N), Fun(x, f(x)), {opaque=fal local h = Const("h") local a = Const("a") 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) +local tc = type_checker(env, ngen) 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)) diff --git a/tests/lua/tc8.lua b/tests/lua/tc8.lua index f5f9fe76d..f7c1d157c 100644 --- a/tests/lua/tc8.lua +++ b/tests/lua/tc8.lua @@ -6,17 +6,19 @@ env = add_decl(env, mk_var_decl("a", N)) local f = Const("f") local a = Const("a") local m1 = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("l")))) -local cs = {} local ngen = name_generator("tst") -local tc = type_checker(env, ngen, function (c) print(c); cs[#cs+1] = c end) +local tc = type_checker(env, ngen) assert(tc:num_scopes() == 0) tc:push() assert(tc:num_scopes() == 1) print(tc:check(f(m1))) -assert(#cs == 1) +assert(tc:next_cnstr()) +assert(not tc:next_cnstr()) print(tc:check(f(f(m1)))) -assert(#cs == 1) -- New constraint is not generated +assert(not tc:next_cnstr()) -- New constraint is not generated tc:pop() -- forget that we checked f(m1) print(tc:check(f(m1))) -assert(#cs == 2) -- constraint is generated again +-- constraint is generated again +assert(tc:next_cnstr()) +assert(not tc:next_cnstr()) check_error(function() tc:pop() end) diff --git a/tests/lua/tc_bug1.lua b/tests/lua/tc_bug1.lua index 1f7862009..3298036c4 100644 --- a/tests/lua/tc_bug1.lua +++ b/tests/lua/tc_bug1.lua @@ -30,38 +30,32 @@ local Ax2 = Const("Ax2") local Ax3 = Const("Ax3") local foo_intro = Const("foo_intro") local foo_intro2 = Const("foo_intro2") -local cs = {} local ng = name_generator("foo") -local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) +local tc = type_checker(env, ng) local m1 = mk_metavar("m1", Bool) print("before is_def_eq") 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(not tc:next_cnstr()) +local tc = type_checker(env, ng) assert(tc:is_def_eq(foo_intro(m1, q(a), q(a), Ax1), foo_intro(q(a), q(a), q(a), Ax2))) -assert(#cs == 1) -- constraint is used, but there is an alternative that does not use it -assert(cs[1]:lhs() == m1) -assert(cs[1]:rhs() == q(a)) -cs = {} -local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) -assert(#cs == 0) +local c = tc:next_cnstr() +assert(c) +assert(not tc:next_cnstr()) +assert(c:lhs() == m1) +assert(c:rhs() == q(a)) +local tc = type_checker(env, ng) +assert(not tc:next_cnstr()) print(tostring(foo_intro) .. " : " .. tostring(tc:check(foo_intro))) print(tostring(foo_intro2) .. " : " .. tostring(tc:check(foo_intro2))) assert(tc:is_def_eq(foo_intro, foo_intro2)) print("before is_def_eq2") assert(tc:is_def_eq(foo_intro(m1, q(a), q(b), Ax1), foo_intro2(q(a), q(a), q(a), Ax2))) -assert(#cs == 0) -- constraint should be ignored since we have shown definitional equality using proof irrelevance -cs = {} -local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) +assert(not tc:next_cnstr()) +local tc = type_checker(env, ng) print("before failure") assert(not pcall(function() print(tc:check(and_intro(m1, q(a), Ax1, Ax3))) end)) -assert(#cs == 0) -- the check failed, so the constraints should be preserved -cs = {} +assert(not tc:next_cnstr()) print("before success") print(tc:check(and_intro(m1, q(a), Ax1, Ax2))) -assert(#cs == 1) -- the check succeeded, and we must get one constraint - --- Demo: infer method may generate constraints --- local m2 = mk_metavar("m2", mk_metavar("ty_m2", mk_sort(mk_meta_univ("s_m2")))) --- print(tc:infer(mk_pi("x", m2, Var(0)))) +assert(tc:next_cnstr()) +assert(not tc:next_cnstr())