From a55c3c617de39b3f092e5f8cd53ebb9cba74e6c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Apr 2014 17:44:43 -0700 Subject: [PATCH] feat(kernel/type_checker): add infer_type Signed-off-by: Leonardo de Moura --- src/kernel/expr.h | 3 +- src/kernel/instantiate.cpp | 13 +- src/kernel/instantiate.h | 12 ++ src/kernel/level.cpp | 9 + src/kernel/level.h | 5 + src/kernel/metavar.cpp | 8 + src/kernel/metavar.h | 6 + src/kernel/type_checker.cpp | 317 +++++++++++++++++++++++++++++++----- 8 files changed, 333 insertions(+), 40 deletions(-) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 5d620d80d..53d034d8f 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -260,9 +260,10 @@ public: macro():m_rc(0) {} virtual ~macro() {} virtual name get_name() const = 0; - virtual expr get_type(unsigned num_args, expr const * arg_types) const = 0; + virtual expr get_type(unsigned num_args, expr const * args, expr const * arg_types) const = 0; virtual optional expand1(unsigned num_args, expr const * args) const = 0; virtual optional expand(unsigned num_args, expr const * args) const = 0; + virtual unsigned trust_level() const = 0; virtual int push_lua(lua_State * L) const; virtual bool operator==(macro const & other) const; bool operator<(macro const & other) const; diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 0fdc5a2b0..f747b1029 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -11,7 +11,8 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" namespace lean { -expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) { +template +expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, P const & p = P()) { if (s >= get_free_var_range(a) || n == 0) return a; return replace(a, [=](expr const & m, unsigned offset) -> optional { @@ -32,7 +33,7 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) { } } return none_expr(); - }); + }, p); } expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, 0, n, s); } @@ -40,6 +41,14 @@ expr instantiate(expr const & e, std::initializer_list const & l) { retur expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); } expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); } +expr instantiate(expr const & e, unsigned n, expr const * s, std::function const & new_eh) { + return instantiate(e, 0, n, s, new_eh); +} + +expr instantiate(expr const & e, expr const & s, std::function const & new_eh) { + return instantiate(e, 1, &s, new_eh); +} + bool is_head_beta(expr const & t) { expr const * it = &t; while (is_app(*it)) { diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index acc9badc6..084d2726a 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "kernel/expr.h" namespace lean { @@ -17,6 +18,17 @@ expr instantiate(expr const & e, unsigned i, expr const & s); /** \brief Replace free variable \c 0 with \c s in \c e. */ expr instantiate(expr const & e, expr const & s); +/** + \brief Replace the free variables in \c e. + Whenever a new sub-expression is created in the process, the procedure \c new_eh is invoked. +*/ +expr instantiate(expr const & e, unsigned n, expr const * s, std::function const & new_eh); +/** + \brief Replace free variable \c 0 with \c s in \c e. + Whenever a new sub-expression is created in the process, the procedure \c new_eh is invoked. +*/ +expr instantiate(expr const & e, expr const & s, std::function const & new_eh); + expr apply_beta(expr f, unsigned num_args, expr const * args); bool is_head_beta(expr const & t); expr head_beta_reduce(expr const & t); diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 714940e34..7312d9ccf 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -622,6 +622,15 @@ format pp(level const & l, options const & opts) { return pp(l, get_pp_unicode(opts), get_pp_indent(opts)); } +format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent) { + format leq = unicode ? format("≤") : format("<="); + return group(format{pp(lhs, unicode, indent), space(), leq, line(), pp(rhs, unicode, indent)}); +} + +format pp(level const & lhs, level const & rhs, options const & opts) { + return pp(lhs, rhs, get_pp_unicode(opts), get_pp_indent(opts)); +} + bool is_trivial(level const & lhs, level const & rhs) { check_system("level constraints"); if (is_zero(lhs) || lhs == rhs) { diff --git a/src/kernel/level.h b/src/kernel/level.h index 30ca75276..6ad09fd7f 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -212,6 +212,11 @@ format pp(level l, bool unicode, unsigned indent); /** \brief Pretty print the given level expression using the given configuration options. */ format pp(level const & l, options const & opts = options()); +/** \brief Pretty print lhs <= rhs, unicode characters are used if \c unicode is \c true. */ +format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent); +/** \brief Pretty print lhs <= rhs using the given configuration options. */ +format pp(level const & lhs, level const & rhs, options const & opts = options()); + /** \brief Auxiliary class used to manage universe constraints. */ class universe_context { struct imp; diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 0c6e4f140..d3b1ad904 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -216,6 +216,10 @@ std::pair substitution::d_instantiate_metavars(expr const & return mk_pair(r, fn.get_justification()); } +std::pair substitution::instantiate_metavars(level const & l) const { + return lean::instantiate_metavars(l, const_cast(*this), true, false); +} + expr substitution::instantiate_metavars_wo_jst(expr const & e) const { return instantiate_metavars_fn(const_cast(*this), false, false)(e); } @@ -224,6 +228,10 @@ expr substitution::d_instantiate_metavars_wo_jst(expr const & e) { return instantiate_metavars_fn(*this, false, true)(e); } +level substitution::instantiate_metavars_wo_jst(level const & l) const { + return lean::instantiate_metavars(l, const_cast(*this), false, false).first; +} + bool substitution::occurs_expr(name const & m, expr const & e) const { if (!has_metavar(e)) return false; diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 0911c3cb9..f00487fc9 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -59,6 +59,9 @@ public: */ std::pair d_instantiate_metavars(expr const & e); + /** \brief Instantiate level metavariables in \c l. */ + std::pair instantiate_metavars(level const & l) const; + /** \brief Instantiate metavariables in \c e assigned in the substitution \c s, but does not return a justification object for the new expression. @@ -67,6 +70,9 @@ public: expr d_instantiate_metavars_wo_jst(expr const & e); + /** \brief Instantiate level metavariables in \c l, but does not return justification object. */ + level instantiate_metavars_wo_jst(level const & l) const; + /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */ bool occurs_expr(name const & m, expr const & e) const; /** \brief Return true iff the meta universe parameter \c m occurrs (directly or indirectly) in \c e. */ diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 6e229a12c..6b7342c7d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -12,6 +12,10 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/max_sharing.h" #include "kernel/free_vars.h" +#include "kernel/metavar.h" +#include "kernel/error_msgs.h" +#include "kernel/kernel_exception.h" +#include "kernel/abstract.h" namespace lean { /** \brief Auxiliary functional object used to implement type checker. */ @@ -23,9 +27,13 @@ struct type_checker::imp { bool m_memoize; name_set m_extra_opaque; max_sharing_fn m_sharing; - expr_map m_cache; + expr_map m_infer_type_cache; expr_map m_whnf_core_cache; expr_map m_whnf_cache; + // The following mapping is used to store the relationship + // between temporary expressions created during type checking and the original ones. + // We need that to be able to produce error messages containing position information. + expr_map m_trace; imp(environment const & env, name_generator const & g, constraint_handler & h, optional mod_idx, bool memoize, name_set const & extra_opaque): @@ -42,6 +50,7 @@ struct type_checker::imp { virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); } }; + bool check_memoized(expr const & e) const { return !m_memoize || m_sharing.already_processed(e); } expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; } expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); } expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); } @@ -65,8 +74,35 @@ struct type_checker::imp { return none_expr(); } - bool check_memoized(expr const & e) const { - return !m_memoize || m_sharing.already_processed(e); + /** \brief Add entry new_e -> old_e in the traceability mapping */ + void add_trace(expr const & old_e, expr const & new_e) { + if (!is_eqp(old_e, new_e)) + m_trace.insert(mk_pair(new_e, old_e)); + } + + /** \brief Return the input (sub) expression that corresponds to the (temporary) expression \c e. */ + expr trace_back(expr e) const { + while (true) { + auto it = m_trace.find(e); + if (it != m_trace.end()) + e = it->second; + else + return e; + } + } + + /** \brief Replace free variable \c 0 with \c s in \c e, and trace new sub-expressions created in the process. */ + expr instantiate_with_trace(expr const & e, expr const & s) { + return lean::instantiate(e, s, [&](expr const & old_e, expr const & new_e) { add_trace(old_e, new_e); }); + } + + /** + \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant. + It also returns the fresh local constant. + */ + std::pair open_binder_body(expr const & e) { + expr local = mk_local(m_gen.next() + binder_name(e), binder_domain(e)); + return mk_pair(instantiate_with_trace(binder_body(e), local), local); } /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ @@ -252,9 +288,10 @@ struct type_checker::imp { } /** \brief Put expression \c e in weak head normal form */ - expr whnf(expr const & e) { + expr whnf(expr e) { // check cache if (m_memoize) { + e = max_sharing(e); auto it = m_whnf_cache.find(e); if (it != m_whnf_cache.end()) return it->second; @@ -279,21 +316,24 @@ struct type_checker::imp { m_chandler.add_cnstr(c); } - /** \brief Return the current/latest justification object created by the type checker. */ - justification get_curr_justification() { - // TODO(Leo) - return mk_assumption_justification(0); - } + /** \brief Object to simulate delayed justification creation. */ + class delayed_justification { + optional m_jst; + std::function m_mk; + public: + template delayed_justification(Mk && mk):m_mk(mk) {} + justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } + }; /** \brief Eta-expand \c s and check if it is definitionally equal to \c t. */ - bool try_eta(expr const & t, expr const & s) { + bool try_eta(expr const & t, expr const & s, delayed_justification & jst) { lean_assert(is_lambda(t)); lean_assert(!is_lambda(s)); expr t_s = whnf(infer_type(s)); if (is_pi(t_s)) { // new_s := lambda x : domain(t_s), s x expr new_s = mk_lambda(m_gen.next(), binder_domain(t_s), mk_app(lift_free_vars(s, 1), mk_var(0))); - return is_def_eq(t, new_s); + return is_def_eq(t, new_s, jst); } else { return false; } @@ -318,7 +358,7 @@ struct type_checker::imp { and body(t) is convertible to body(s) */ - bool is_conv_binder(expr t, expr s, bool def_eq) { + bool is_conv_binder(expr t, expr s, bool def_eq, delayed_justification & jst) { lean_assert(t.kind() == s.kind()); lean_assert(is_binder(t)); expr_kind k = t.kind(); @@ -326,13 +366,13 @@ struct type_checker::imp { do { expr var_t_type = instantiate(binder_domain(t), subst.size(), subst.data()); expr var_s_type = instantiate(binder_domain(s), subst.size(), subst.data()); - if (!is_def_eq(var_t_type, var_s_type)) + if (!is_def_eq(var_t_type, var_s_type, jst)) return false; - subst.push_back(mk_local(m_gen.next(), var_s_type)); + subst.push_back(mk_local(m_gen.next() + binder_name(s), var_s_type)); t = binder_body(t); s = binder_body(s); } while (t.kind() == k && s.kind() == k); - return is_conv(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), def_eq); + return is_conv(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), def_eq, jst); } /** @@ -340,30 +380,30 @@ struct type_checker::imp { If \c def_eq is true, then it checks for definitional equality. */ - lbool quick_is_conv(expr const & t, expr const & s, bool def_eq) { + lbool quick_is_conv(expr const & t, expr const & s, bool def_eq, delayed_justification & jst) { if (t == s) return l_true; // t and s are structurally equal if (is_meta(t) || is_meta(s)) { // if t or s is a metavariable (or the application of a metavariable), then add constraint if (def_eq) - add_cnstr(mk_eq_cnstr(t, s, get_curr_justification())); + add_cnstr(mk_eq_cnstr(t, s, jst.get())); else - add_cnstr(mk_conv_cnstr(t, s, get_curr_justification())); + add_cnstr(mk_conv_cnstr(t, s, jst.get())); return l_true; } if (t.kind() == s.kind()) { switch (t.kind()) { case expr_kind::Lambda: - return to_lbool(is_conv_binder(t, s, true)); + return to_lbool(is_conv_binder(t, s, true, jst)); case expr_kind::Pi: - return to_lbool(is_conv_binder(t, s, def_eq)); + return to_lbool(is_conv_binder(t, s, def_eq, jst)); case expr_kind::Sort: // t and s are Sorts if (is_trivial(sort_level(t), sort_level(s)) && (!def_eq || is_trivial(sort_level(s), sort_level(t)))) return l_true; - add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), get_curr_justification())); + add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get())); if (def_eq) - add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), get_curr_justification())); + add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), jst.get())); return l_true; case expr_kind::Meta: lean_unreachable(); // LCOV_EXCL_LINE @@ -380,16 +420,16 @@ struct type_checker::imp { \brief If def_eq is false, then return true iff t is convertible to s. If def_eq is true, then return true iff t is definitionally equal to s. */ - bool is_conv(expr const & t, expr const & s, bool def_eq) { + bool is_conv(expr const & t, expr const & s, bool def_eq, delayed_justification & jst) { check_system("is_convertible"); - lbool r = quick_is_conv(t, s, def_eq); + lbool r = quick_is_conv(t, s, def_eq, jst); if (r != l_undef) return r == l_true; // apply whnf (without using delta-reduction or normalizer extensions) expr t_n = whnf_core(t); expr s_n = whnf_core(s); if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { - r = quick_is_conv(t_n, s_n, def_eq); + r = quick_is_conv(t_n, s_n, def_eq, jst); if (r != l_undef) return r == l_true; } @@ -418,7 +458,7 @@ struct type_checker::imp { t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1)); s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1)); } - r = quick_is_conv(t_n, s_n, def_eq); + r = quick_is_conv(t_n, s_n, def_eq, jst); if (r != l_undef) return r == l_true; } // try normalizer extensions @@ -430,7 +470,7 @@ struct type_checker::imp { t_n = whnf_core(*new_t_n); if (new_s_n) s_n = whnf_core(*new_s_n); - r = quick_is_conv(t_n, s_n, def_eq); + r = quick_is_conv(t_n, s_n, def_eq, jst); if (r != l_undef) return r == l_true; } @@ -439,8 +479,8 @@ struct type_checker::imp { if (m_env.eta()) { lean_assert(!is_lambda(t_n) || !is_lambda(s_n)); // Eta-reduction support - if ((is_lambda(t_n) && try_eta(t_n, s_n)) || - (is_lambda(s_n) && try_eta(s_n, t_n))) + if ((is_lambda(t_n) && try_eta(t_n, s_n, jst)) || + (is_lambda(s_n) && try_eta(s_n, t_n, jst))) return true; } @@ -449,29 +489,34 @@ struct type_checker::imp { expr it2 = s_n; bool ok = true; do { - if (!is_def_eq(app_arg(it1), app_arg(it2))) { + if (!is_def_eq(app_arg(it1), app_arg(it2), jst)) { ok = false; break; } it1 = app_fn(it1); it2 = app_fn(it2); } while (is_app(it1) && is_app(it2)); - if (ok && is_def_eq(it1, it2)) + if (ok && is_def_eq(it1, it2, jst)) return true; } if (m_env.proof_irrel()) { // Proof irrelevance support expr t_type = infer_type(t); - return is_proposition(t_type) && is_def_eq(t_type, infer_type(s)); + return is_proposition(t_type) && is_def_eq(t_type, infer_type(s), jst); } return false; } + /** \brief Return true iff \c t is convertible to s */ + bool is_conv(expr const & t, expr const & s, delayed_justification & jst) { + return is_conv(t, s, false, jst); + } + /** \brief Return true iff \c t and \c s are definitionally equal */ - bool is_def_eq(expr const & t, expr const & s) { - return is_conv(t, s, true); + bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst) { + return is_conv(t, s, true, jst); } /** \brief Return true iff \c e is a proposition */ @@ -479,9 +524,207 @@ struct type_checker::imp { return whnf(infer_type(e)) == Bool; } - expr infer_type(expr const &) { - // TODO(Leo) - return expr(); + /** + \brief Make sure \c e "is" a sort, and return the corresponding sort. + If \c e is not a sort, then the whnf procedure is invoked. Then, there are + two options: the normalize \c e is a sort, or it is a meta. If it is a meta, + a new constraint is created forcing it to be a sort. + + \remark \c s is used to extract position (line number information) when an + error message is produced + */ + expr ensure_sort(expr e, expr const & s) { + if (is_sort(e)) + return e; + e = whnf(e); + if (is_sort(e)) { + return e; + } else if (is_meta(e)) { + expr r = mk_sort(mk_meta_univ(m_gen.next())); + justification j = mk_justification(trace_back(s), + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_type_expected(fmt, o, subst.instantiate_metavars_wo_jst(s)); + }); + add_cnstr(mk_eq_cnstr(e, r, j)); + return r; + } else { + throw_kernel_exception(m_env, trace_back(s), + [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, s); }); + } } + + /** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */ + expr ensure_pi(expr e, expr const & s) { + if (is_pi(e)) + return e; + e = whnf(e); + if (is_pi(e)) { + return e; + } else if (is_meta(e)) { + // TODO(Leo) + return e; + } else { + throw_kernel_exception(m_env, trace_back(s), + [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, o, s); }); + } + } + + /** \brief Create a justification for the level constraint lhs <= rhs associated with constanc \c c. */ + justification mk_lvl_cnstr_jst(expr const & c, level const & lhs, level const & rhs) { + lean_assert(is_constant(c)); + return mk_justification(trace_back(c), + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_def_lvl_cnstrs_satisfied(fmt, o, + subst.instantiate_metavars_wo_jst(c), + subst.instantiate_metavars_wo_jst(lhs), + subst.instantiate_metavars_wo_jst(rhs)); + }); + } + + /** + \brief Create a justification for a application type mismatch, + \c e is the application, \c fn_type and \c arg_type are the function and argument type. + */ + justification mk_app_mismatch_jst(expr const & e, expr const & fn_type, expr const & arg_type) { + lean_assert(is_app(e)); + return mk_justification(trace_back(e), + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_app_type_mismatch(fmt, o, + subst.instantiate_metavars_wo_jst(e), + subst.instantiate_metavars_wo_jst(binder_domain(fn_type)), + subst.instantiate_metavars_wo_jst(arg_type)); + }); + } + + /** + \brief Create a justification for a let definition type mismatch, + \c e is the let expression, and \c val_type is the type inferred for the let value. + */ + justification mk_let_mismatch_jst(expr const & e, expr const & val_type) { + lean_assert(is_let(e)); + return mk_justification(trace_back(e), + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_def_type_mismatch(fmt, o, let_name(e), + subst.instantiate_metavars_wo_jst(let_type(e)), + subst.instantiate_metavars_wo_jst(val_type)); + }); + } + + static constexpr char const * g_macro_error_msg = "failed to type check macro expansion"; + + justification mk_macro_jst(expr const & e) { + return mk_justification(trace_back(e), + [=](formatter const &, options const &, substitution const &) { + return format(g_macro_error_msg); + }); + } + + /** + \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not. + + \pre closed(e) + */ + expr infer_type_core(expr const & e, bool infer_only) { + lean_assert(closed(e)); + check_system("type checker"); + + bool shared = false; + if (m_memoize && is_shared(e)) { + shared = true; + auto it = m_infer_type_cache.find(e); + if (it != m_infer_type_cache.end()) + return it->second; + } + + expr r; + switch (e.kind()) { + case expr_kind::Local: case expr_kind::Meta: + r = mlocal_type(e); + break; + case expr_kind::Var: + throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it"); + case expr_kind::Sort: + r = mk_sort(mk_succ(sort_level(e))); + break; + case expr_kind::Constant: { + definition d = m_env.get(const_name(e)); + auto const & ps = d.get_params(); + auto const & ls = const_level_params(e); + auto const & cs = d.get_level_cnstrs(); + if (!infer_only && !is_nil(cs)) { + // add level constraints associated with the definition + for (auto const & c : cs) { + level lhs = lean::instantiate(c.first, ps, ls); + level rhs = lean::instantiate(c.second, ps, ls); + if (!is_trivial(lhs, rhs)) + add_cnstr(mk_level_cnstr(lhs, rhs, mk_lvl_cnstr_jst(e, lhs, rhs))); + } + } + r = instantiate_params(d.get_type(), ps, ls); + break; + } + case expr_kind::Macro: + r = to_macro(e).get_type(0, 0, 0); + if (!infer_only && to_macro(e).trust_level() <= m_env.trust_lvl()) { + optional m = to_macro(e).expand(0, 0); + if (!m) + throw_kernel_exception(m_env, "failed to expand macro", some_expr(e)); + expr t = infer_type_core(*m, infer_only); + delayed_justification jst([=]() { return mk_macro_jst(e); }); + if (!is_def_eq(r, t, jst)) + throw_kernel_exception(m_env, g_macro_error_msg, some_expr(e)); + } + break; + case expr_kind::Lambda: { + if (!infer_only) { + expr t = infer_type_core(binder_domain(e), infer_only); + ensure_sort(t, binder_domain(e)); + } + auto b = open_binder_body(e); + r = Pi(b.second, binder_domain(e), infer_type_core(b.first, infer_only)); + break; + } + case expr_kind::Pi: { + expr t1 = ensure_sort(infer_type_core(binder_domain(e), infer_only), binder_domain(e)); + auto b = open_binder_body(e); + expr t2 = ensure_sort(infer_type_core(b.first, infer_only), binder_body(e)); + r = mk_sort(mk_imax(sort_level(t1), sort_level(t2))); + break; + } + case expr_kind::App: { + expr f_type = ensure_pi(infer_type_core(app_fn(e), infer_only), app_fn(e)); + if (!infer_only) { + expr a_type = infer_type_core(app_arg(e), infer_only); + delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); }); + if (!is_conv(a_type, binder_domain(f_type), jst)) { + throw_kernel_exception(m_env, trace_back(e), + [=](formatter const & fmt, options const & o) { return pp_app_type_mismatch(fmt, o, e, binder_domain(f_type), a_type); }); + } + } + r = instantiate(binder_body(f_type), app_arg(e)); + break; + } + case expr_kind::Let: + if (!infer_only) { + ensure_sort(infer_type_core(let_type(e), infer_only), let_type(e)); + expr val_type = infer_type_core(let_value(e), infer_only); + delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); + if (!is_conv(val_type, let_type(e), jst)) { + throw_kernel_exception(m_env, trace_back(e), + [=](formatter const & fmt, options const & o) { return pp_def_type_mismatch(fmt, o, let_name(e), let_type(e), val_type); }); + } + } + r = infer_type_core(instantiate_with_trace(let_body(e), let_value(e)), infer_only); + break; + } + + if (m_memoize && shared) + m_infer_type_cache.insert(mk_pair(e, r)); + + return r; + } + + expr infer_type(expr const & e) { return infer_type_core(e, true); } + expr check(expr const & e) { return infer_type_core(e, false); } }; }