diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index d1a8a66d2..191f435ca 100644 --- a/src/kernel/constraint.h +++ b/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 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 constraints; +inline constraints add(constraints const & cs, constraint const & c) { return cons(c, cs); } } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index d4d3f073b..9fb83c5b0 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -157,17 +157,17 @@ public: bool has_object(name const & n) const { return static_cast(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; diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 1ea3233df..93a8b9163 100644 --- a/src/kernel/justification.cpp +++ b/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 const & s) { +justification mk_composite(justification const & j1, justification const & j2, optional 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 const & s) { +justification mk_assumption_justification(unsigned idx, optional 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 const & s) { +justification mk_justification(optional const & s, pp_jst_fn const & fn) { return justification(new asserted_cell(fn, s)); } -justification mk_justification(pp_jst_sfn const & fn, optional const & s) { - return mk_justification([=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) { - return compose(to_pos(s, p), fn(fmt, opts, subst)); - }, s); +justification mk_justification(optional const & s, pp_jst_sfn const & fn) { + 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)); }); } std::ostream & operator<<(std::ostream & out, justification const & j) { diff --git a/src/kernel/justification.h b/src/kernel/justification.h index 8cfb8662a..9dcac36dc 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -67,11 +67,11 @@ public: */ optional get_main_expr() const; - friend justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional const & s); + friend justification mk_composite(justification const & j1, justification const & j2, optional 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 const & s); + friend justification mk_assumption_justification(unsigned idx, optional const & s, pp_jst_fn const & fn); friend justification mk_assumption_justification(unsigned idx); - friend justification mk_justification(pp_jst_fn const & fn, optional const & s); + friend justification mk_justification(optional const & s, pp_jst_fn const & fn); }; /** @@ -86,7 +86,7 @@ format to_pos(optional 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 const & s); +justification mk_composite(justification const & j1, justification const & j2, optional 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 const & s); +justification mk_assumption_justification(unsigned idx, optional 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 const & s); +justification mk_justification(optional 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 const & s); +justification mk_justification(optional 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. diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 9f241fd20..502c58547 100644 --- a/src/kernel/kernel_exception.cpp +++ b/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, - optional const & m) { +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m, pp_fn const & fn) { throw generic_kernel_exception(env, msg, m, fn); } -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional const & m) { +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional 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 << "'"); } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 9d1815b8a..e594f31d9 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -37,10 +37,10 @@ public: [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m = none_expr()); [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm, optional const & m = none_expr()); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, - pp_fn const & fn, optional const & m = none_expr()); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional const & m = none_expr()); - +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m, pp_fn const & fn); +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional const & m, pp_fn const & fn); +[[ 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); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index d7a45512d..a634d3465 100644 --- a/src/kernel/type_checker.cpp +++ b/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); - m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU1, jst)); - return u; + expr r = mk_sort(mk_meta_univ()); + justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & s) { + 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); - if (is_pi(r)) - return r; - if (has_metavar(r) && m_menv && m_uc) { + expr u = normalize(e); + if (is_pi(u)) + return u; + 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