refactor(kernel): cleanup interfaces

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

src/kernel/constraint.h

@@ -63,6 +63,11 @@ public:
 bool operator==(constraint const & c1, constraint const & c2);
 inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
 
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j);
+constraint mk_choice_cnstr(expr const & t, list<expr> const & s, justification const & j);
+
 bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 bool is_conv_cnstr(constraint const & c) { return c.kind() == constraint_kind::Convertible; }
 bool is_level_cnstr(constraint const & c) { return c.kind() == constraint_kind::Level; }
@@ -95,4 +100,5 @@ constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level c
 std::ostream & operator<<(std::ostream & out, constraint const & c);
 
 typedef list<constraint> constraints;
+inline constraints add(constraints const & cs, constraint const & c) { return cons(c, cs); }
 }

src/kernel/environment.h

@@ -157,17 +157,17 @@ public:
     bool has_object(name const & n) const { return static_cast<bool>(find_object(n)); }
 
     /**
-       \brief Type check the given expression, and return the type of \c e in the given context and this environment.
+       \brief Type check the given expression, and return the type of \c e in this environment.
     */
     expr type_check(expr const & e) const;
 
     /**
-       \brief Return the type of \c e in the given context and this environment.
+       \brief Return the type of \c e in this environment.
     */
     expr infer_type(expr const & e) const;
 
     /**
-       \brief Normalize \c e in the given context and this environment.
+       \brief Normalize \c e in this environment.
     */
     expr normalize(expr const & e) const;
 

src/kernel/justification.cpp

@@ -214,7 +214,7 @@ format justification::pp(formatter const & fmt, options const & opts, pos_info_p
     }
 }
 
-justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s) {
+justification mk_composite(justification const & j1, justification const & j2, optional<expr> const & s, pp_jst_fn const & fn) {
     if (j1.is_none())
         return j2;
     if (j2.is_none())
@@ -228,19 +228,18 @@ justification mk_composite1(justification const & j1, justification const & j2)
         return j1;
     return justification(new composite_cell(j1, j2));
 }
-justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s) {
+justification mk_assumption_justification(unsigned idx, optional<expr> const & s, pp_jst_fn const & fn) {
     return justification(new ext_assumption_cell(idx, fn, s));
 }
 justification mk_assumption_justification(unsigned idx) {
     return justification(new assumption_cell(idx));
 }
-justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s) {
+justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn) {
     return justification(new asserted_cell(fn, s));
 }
-justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s) {
+justification mk_justification(optional<expr> const & s, pp_jst_sfn const & fn) {
-    return mk_justification([=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) {
+    return mk_justification(s, [=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) {
-            return compose(to_pos(s, p), fn(fmt, opts, subst));
+            return compose(to_pos(s, p), fn(fmt, opts, subst)); });
-        }, s);
 }
 
 std::ostream & operator<<(std::ostream & out, justification const & j) {

src/kernel/justification.h

@@ -67,11 +67,11 @@ public:
     */
     optional<expr> get_main_expr() const;
 
-    friend justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
+    friend justification mk_composite(justification const & j1, justification const & j2, optional<expr> const & s, pp_jst_fn const & fn);
     friend justification mk_composite1(justification const & j1, justification const & j2);
-    friend justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
+    friend justification mk_assumption_justification(unsigned idx, optional<expr> const & s, pp_jst_fn const & fn);
     friend justification mk_assumption_justification(unsigned idx);
-    friend justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
+    friend justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn);
 };
 
 /**
@@ -86,7 +86,7 @@ format to_pos(optional<expr> const & e, pos_info_provider const * p);
    \brief Combine the two given justifications into a new justification object, and use
    the given function to convert the justification into a format object.
 */
-justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
+justification mk_composite(justification const & j1, justification const & j2, optional<expr> const & s, pp_jst_fn const & fn);
 /**
    \brief Similar to \c mk_composite, but uses \c j1.pp to convert the
    resulting justification into a format object.
@@ -99,7 +99,7 @@ justification mk_substitution_justification(justification const & j1, justificat
 /**
    \brief Create a "case-split" justification with the given \c idx.
 */
-justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
+justification mk_assumption_justification(unsigned idx, optional<expr> const & s, pp_jst_fn const & fn);
 /**
    \brief Similar to the previous function, but fn just returns the format object "assumption idx", and s is the none.
 */
@@ -107,12 +107,15 @@ justification mk_assumption_justification(unsigned idx);
 /**
    \brief Create a justification for constraints produced by the type checker.
 */
-justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
+justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn);
 /**
    \brief Create a justification for constraints produced by the type checker.
    It is similar to the previous function, but the position of \c s will be automatically included.
 */
-justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s);
+justification mk_justification(optional<expr> const & s, pp_jst_sfn const & fn);
+inline justification mk_justification(expr const & s, pp_jst_sfn const & fn) {
+    return mk_justification(some_expr(s), fn);
+}
 
 /**
    \brief Return the first child of a composite justification.

src/kernel/kernel_exception.cpp

@@ -37,15 +37,22 @@ public:
     throw_kernel_exception(env, strm.str().c_str(), m);
 }
 
-[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, pp_fn const & fn,
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn) {
-                                           optional<expr> const & m) {
     throw generic_kernel_exception(env, msg, m, fn);
 }
 
-[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m) {
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional<expr> const & m, pp_fn const & fn) {
     throw generic_kernel_exception(env, "kernel exception", m, fn);
 }
 
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, expr const & m, pp_fn const & fn) {
+    throw_kernel_exception(env, msg, some_expr(m), fn);
+}
+
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, expr const & m, pp_fn const & fn) {
+    throw_kernel_exception(env, some_expr(m), fn);
+}
+
 [[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n) {
     throw_kernel_exception(env, sstream() << "unknown object '" << n << "'");
 }

src/kernel/kernel_exception.h

@@ -37,10 +37,10 @@ public:
 [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m = none_expr());
 [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm,
                                            optional<expr> const & m = none_expr());
-[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg,
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn);
-                                           pp_fn const & fn, optional<expr> const & m = none_expr());
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional<expr> const & m, pp_fn const & fn);
-[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m = none_expr());
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, expr const & m, pp_fn const & fn);
-
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, expr const & m, pp_fn const & fn);
 [[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n);
 [[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n);
 [[ noreturn ]] void throw_read_only_environment(ro_environment const & env);

src/kernel/type_checker.cpp

@@ -14,6 +14,9 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
+#include "kernel/error_msgs.h"
+#include "kernel/constraint.h"
+#include "kernel/metavar.h"
 
 namespace lean {
 expr pi_body_at(expr const & pi, expr const & a) {
@@ -40,7 +43,14 @@ class type_checker::imp {
     ro_environment env() const { return ro_environment(m_env); }
     expr normalize(expr const & e) { return m_normalizer(e); }
 
-#if 0
+    level mk_meta_univ() {
+        return ::lean::mk_meta_univ(m_name_gen->next());
+    }
+
+    void add_eq_constraint(expr const & t, expr const & s, justification const & j) {
+        m_constraints = add(m_constraints, mk_eq_cnstr(t, s, j));
+    }
+
     expr check_sort(expr const & e, expr const & s) {
         if (is_sort(e))
             return e;
@@ -48,41 +58,24 @@ class type_checker::imp {
         if (is_sort(u))
             return u;
         if (has_metavar(u)) {
-            justification jst = mk_type_expected_justification(ctx, s);
+            expr r = mk_sort(mk_meta_univ());
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU1, jst));
+            justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & s) {
-            return u;
+                    return pp_type_expected(fmt, o, s.instantiate_metavars_wo_jst(e));
+                });
+            add_eq_constraint(e, r, j);
+            return r;
         }
-        throw type_expected_exception(env(), ctx, s);
+        throw_kernel_exception(env(), s, [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, e); });
     }
-#endif
-};
-
 
 #if 0
-static name g_x_name("x");
-/** \brief Auxiliary functional object used to implement infer_type. */
-class type_checker::imp {
-    expr check_type(expr const & e, expr const & s, context const & ctx) {
-        if (is_type(e) || is_bool(e))
-            return e;
-        expr u = normalize(e, ctx, false);
-        if (is_type(u) || is_bool(u))
-            return u;
-        if (has_metavar(u) && m_menv && m_uc) {
-            justification jst = mk_type_expected_justification(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU1, jst));
-            return u;
-        }
-        throw type_expected_exception(env(), ctx, s);
-    }
-
     expr check_pi(expr const & e, expr const & s, context const & ctx) {
         if (is_pi(e))
             return e;
-        expr r = normalize(e, ctx, false);
+        expr u = normalize(e);
-        if (is_pi(r))
+        if (is_pi(u))
-            return r;
+            return u;
-        if (has_metavar(r) && m_menv && m_uc) {
+        if (has_metavar(u)) {
             // Create two fresh variables A and B,
             // and assign r == (Pi(x : A), B)
             expr A   = m_menv->mk_metavar(ctx);
@@ -94,6 +87,16 @@ class type_checker::imp {
         }
         throw function_expected_exception(env(), ctx, s);
     }
+#endif
+
+};
+
+
+#if 0
+static name g_x_name("x");
+/** \brief Auxiliary functional object used to implement infer_type. */
+class type_checker::imp {
+
 
     // TODO(Leo): we should consider merging check_pi and check_sigma.
     // They are very similar