refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
                     return optional<a_choice>(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<list<constraint>>(); }),
-        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { add_cnstr(c); },
+        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional<module_idx>(0))),
-                           mk_default_converter(m_env, optional<module_idx>(0))),
         m_subst(s), m_ctx(ctx) {
     }
 
@@ -530,6 +535,7 @@ public:
     }
 
     lazy_list<substitution> solve() {
+        consume_tc_cnstrs();
         buffer<constraint> cs;
         cs.append(m_constraints);
         m_constraints.clear();

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(tc), m_keep(false) {
-    m_tc.m_infer_type_cache[0].push();
+    m_tc.push();
-    m_tc.m_infer_type_cache[1].push();
-    m_tc.m_cache_cs = true;
 }
 type_checker::scope::~scope() {
-    if (m_keep) {
+    if (m_keep)
-        // keep results
+        m_tc.keep();
-        m_tc.m_infer_type_cache[0].keep();
+    else
-        m_tc.m_infer_type_cache[1].keep();
+        m_tc.pop();
-    } 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;
 }
 
 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<expr> type_checker::expand_macro(expr const & m) {
@@ -84,10 +55,17 @@ std::pair<expr, expr> 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);
-        m_cs.push_back(c);
+}
-    else
+
-        m_add_cnstr_fn(c);
+optional<constraint> type_checker::next_cnstr() {
+    if (m_cs_qhead < m_cs.size()) {
+        constraint c = m_cs[m_cs_qhead];
+        m_cs_qhead++;
+        return optional<constraint>(c);
+    } else {
+        return optional<constraint>();
+    }
 }
 
 /**
@@ -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<converter> && 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<converter> && 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() {}
 

src/kernel/type_checker.h

@@ -16,19 +16,6 @@ Author: Leonardo de Moura
 #include "kernel/converter.h"
 
 namespace lean {
-typedef std::function<void(constraint const & c)> 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<converter> 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<constraint>         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<std::pair<unsigned, unsigned>> 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<converter> && 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<converter> && 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<constraint> 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();
+    };
 };
 
 /**

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<constraint> 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> 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<type_checker>(to_environment(L, 1)));
     } else if (nargs == 2) {
         return push_type_checker_ref(L, std::make_shared<type_checker>(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<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
-                                                                       to_add_cnstr_fn(L, 3)));
     } else {
         optional<module_idx> mod_idx; bool memoize; name_set extra_opaque;
-        if (nargs == 3) {
+        get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque);
-            get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque);
+        auto t = std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
-            auto t = std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
+                                                mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque),
-                                                    mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque),
+                                                memoize);
-                                                    memoize);
+        return push_type_checker_ref(L, t);
-            return push_type_checker_ref(L, t);
-        } else {
-            get_type_checker_args(L, 4, mod_idx, memoize, extra_opaque);
-            auto t = std::make_shared<type_checker>(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);
-        }
     }
 }
 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<type_checker_is_prop>},
     {"push",        safe_function<type_checker_push>},
     {"pop",         safe_function<type_checker_pop>},
+    {"keep",        safe_function<type_checker_keep>},
+    {"next_cnstr",  safe_function<type_checker_next_cnstr>},
     {"num_scopes",  safe_function<type_checker_num_scopes>},
     {0, 0}
 };

src/library/kernel_bindings.h

@@ -25,6 +25,7 @@ int push_optional_level(lua_State * L, optional<level> const & e);
 int push_optional_expr(lua_State * L, optional<expr> const & e);
 int push_optional_justification(lua_State * L, optional<justification> const & j);
 int push_optional_declaration(lua_State * L, optional<declaration> const & e);
+int push_optional_constraint(lua_State * L, optional<constraint> const & c);
 int push_list_expr(lua_State * L, list<expr> const & l);
 /**
    \brief Return the formatter object associated with the given Lua State.

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<substitution>();
         }
-        while (!m_cnstrs.empty()) {
+        while (true) {
-            check_system();
+            consume_tc_cnstrs();
-            lean_assert(!in_conflict());
+            if (!in_conflict()) {
-            bool ok = process_next();
+                if (m_cnstrs.empty())
-            if (!ok && !resolve_conflict())
+                    break;
+                process_next();
+            }
+            if (in_conflict() && !resolve_conflict())
                 return failure();
         }
         lean_assert(!in_conflict());
@@ -1016,25 +1027,15 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
                               unsigned max_steps) {
     substitution s;
-    buffer<constraint> cs;
     name_generator new_ngen(ngen);
-    bool failed = false;
+    type_checker tc(env, new_ngen.mk_child());
-    type_checker tc(env, new_ngen.mk_child(), [&](constraint const & c) {
+    if (!tc.is_def_eq(lhs, rhs))
-            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) {
         return lazy_list<substitution>();
-    } else if (cs.empty()) {
+    buffer<constraint> cs;
+    while (auto c = tc.next_cnstr()) {
+        cs.push_back(*c);
+    }
+    if (cs.empty()) {
         return lazy_list<substitution>(s);
     } else {
         return unify(std::make_shared<unifier_fn>(env, cs.size(), cs.data(), ngen, s, p, false, max_steps));

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
+

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
+print(env:type_check(m3(a)))
--- 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("before end")

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)
-local tc2 = type_checker(env, g, function (c) print(c); cs[#cs+1] = c end)
 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())

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)
-local tc2 = type_checker(env, g, function (c) print(c); cs[#cs+1] = c end)
 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)

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))))
-                    print(tc:check(mk_lambda("x", mk_metavar("m", mk_metavar("t", mk_sort(mk_meta_univ("l")))), Var(0))))
+assert(tc:next_cnstr())
-                 end
-))
 print(tc:ensure_sort(Const("B2")))
 assert(not pcall(function()
                     print(tc:ensure_sort(Const("A")))

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))

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)

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)
+assert(not tc:next_cnstr())
-local cs  = {}
+local tc  = type_checker(env, ng)
-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), 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
+local c = tc:next_cnstr()
-assert(cs[1]:lhs() == m1)
+assert(c)
-assert(cs[1]:rhs() == q(a))
+assert(not tc:next_cnstr())
-cs = {}
+assert(c:lhs() == m1)
-local tc  = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
+assert(c:rhs() == q(a))
-assert(#cs == 0)
+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
+assert(not tc:next_cnstr())
-cs = {}
+local tc  = type_checker(env, ng)
-local tc  = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
 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
+assert(not tc:next_cnstr())
-cs = {}
 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
+assert(tc:next_cnstr())
-
+assert(not tc:next_cnstr())
--- 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))))