From f371182a6ceaf1525c660251b32158cad531695d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Oct 2015 17:51:25 -0700 Subject: [PATCH] feat(library/type_inference): generic and cheap type inference, unification, whnf --- src/library/CMakeLists.txt | 2 +- src/library/type_inference.cpp | 905 +++++++++++++++++++++++++++++++++ src/library/type_inference.h | 180 +++++++ 3 files changed, 1086 insertions(+), 1 deletion(-) create mode 100644 src/library/type_inference.cpp create mode 100644 src/library/type_inference.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index c4c386deb..1a6bb1578 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -16,4 +16,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp composition_manager.cpp tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp - norm_num.cpp class_instance_resolution.cpp) + norm_num.cpp class_instance_resolution.cpp type_inference.cpp) diff --git a/src/library/type_inference.cpp b/src/library/type_inference.cpp new file mode 100644 index 000000000..0bb5270ee --- /dev/null +++ b/src/library/type_inference.cpp @@ -0,0 +1,905 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/interrupt.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/for_each_fn.h" +#include "library/projection.h" +#include "library/normalize.h" +#include "library/replace_visitor.h" +#include "library/type_inference.h" + +namespace lean { +static name * g_prefix = nullptr; + +struct type_inference::ext_ctx : public extension_context { + type_inference & m_owner; + + ext_ctx(type_inference & o):m_owner(o) {} + + virtual environment const & env() const { return m_owner.m_env; } + + virtual pair whnf(expr const & e) { + return mk_pair(m_owner.whnf(e), constraint_seq()); + } + + virtual pair is_def_eq(expr const & e1, expr const & e2, delayed_justification &) { + return mk_pair(m_owner.is_def_eq(e1, e2), constraint_seq()); + } + + virtual pair check_type(expr const & e, bool) { + return mk_pair(m_owner.infer(e), constraint_seq()); + } + + virtual name mk_fresh_name() { + return m_owner.m_ngen.next(); + } + + virtual optional is_stuck(expr const &) { + return none_expr(); + } +}; + +type_inference::type_inference(environment const & env): + m_env(env), + m_ngen(*g_prefix), + m_ext_ctx(new ext_ctx(*this)), + m_proj_info(get_projection_info_map(env)) { +} + +type_inference::~type_inference() { +} + +bool type_inference::is_opaque(declaration const & d) const { + if (d.is_theorem()) + return true; + name const & n = d.get_name(); + return m_proj_info.contains(n) || is_extra_opaque(n); +} + +optional type_inference::expand_macro(expr const & m) { + lean_assert(is_macro(m)); + return macro_def(m).expand(m, *m_ext_ctx); +} + +optional type_inference::reduce_projection(expr const & e) { + expr const & f = get_app_fn(e); + if (!is_constant(f)) + return none_expr(); + projection_info const * info = m_proj_info.find(const_name(f)); + if (!info) + return none_expr(); + buffer args; + get_app_args(e, args); + if (args.size() <= info->m_nparams) + return none_expr(); + unsigned mkidx = info->m_nparams; + expr const & mk = args[mkidx]; + expr new_mk = whnf(mk); + expr const & new_mk_fn = get_app_fn(new_mk); + if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor) + return none_expr(); + buffer mk_args; + get_app_args(new_mk, mk_args); + unsigned i = info->m_nparams + info->m_i; + if (i >= mk_args.size()) + none_expr(); + expr r = mk_args[i]; + r = mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1); + return some_expr(r); +} + +optional type_inference::norm_ext(expr const & e) { + if (auto r = reduce_projection(e)) { + return r; + } else if (auto r = m_env.norm_ext()(e, *m_ext_ctx)) { + return some_expr(r->first); + } else { + return none_expr(); + } +} + +expr type_inference::whnf_core(expr const & e) { + check_system("whnf"); + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: + return e; + case expr_kind::Macro: + if (auto m = expand_macro(e)) + return whnf_core(*m); + else + return e; + break; + case expr_kind::App: { + buffer args; + expr f0 = get_app_rev_args(e, args); + expr f = whnf_core(f0); + if (is_lambda(f)) { + unsigned m = 1; + unsigned num_args = args.size(); + while (is_lambda(binding_body(f)) && m < num_args) { + f = binding_body(f); + m++; + } + lean_assert(m <= num_args); + return whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), + num_args - m, args.data())); + } else { + return f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data())); + } + }} + lean_unreachable(); +} + +/** \brief Expand \c e if it is non-opaque constant with height >= h */ +expr type_inference::unfold_name_core(expr e, unsigned h) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) { + if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h && + length(const_levels(e)) == d->get_num_univ_params()) + return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h); + } + } + return e; +} + +/** \brief Expand constants and application where the function is a constant. + The unfolding is only performend if the constant corresponds to + a non-opaque definition with height >= h */ +expr type_inference::unfold_names(expr const & e, unsigned h) { + if (is_app(e)) { + expr f0 = get_app_fn(e); + expr f = unfold_name_core(f0, h); + if (is_eqp(f, f0)) { + return e; + } else { + buffer args; + get_app_rev_args(e, args); + return mk_rev_app(f, args); + } + } else { + return unfold_name_core(e, h); + } +} + +/** \brief Return some definition \c d iff \c e is a target for delta-reduction, + and the given definition is the one to be expanded. */ +optional type_inference::is_delta(expr const & e) const { + expr const & f = get_app_fn(e); + if (is_constant(f)) { + if (auto d = m_env.find(const_name(f))) + if (d->is_definition() && !is_opaque(*d)) + return d; + } + return none_declaration(); +} + +/** \brief Weak head normal form core procedure that performs delta reduction + for non-opaque constants with definitional height greater than or equal to \c h. + + This method is based on whnf_core(expr const &) and \c unfold_names. + \remark This method does not use normalization extensions attached in the environment. +*/ +expr type_inference::whnf_core(expr e, unsigned h) { + while (true) { + expr new_e = unfold_names(whnf_core(e), h); + if (is_eqp(e, new_e)) + return e; + e = new_e; + } +} + +/** \brief Put expression \c t in weak head normal form */ +expr type_inference::whnf(expr const & e) { + // Do not cache easy cases + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: + return e; + case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: + break; + } + + expr t = e; + while (true) { + expr t1 = whnf_core(t, 0); + if (auto new_t = norm_ext(t1)) { + t = *new_t; + } else { + return t1; + } + } +} + +bool type_inference::is_def_eq(level const & l1, level const & l2) { + if (is_equivalent(l1, l2)) { + return true; + } + + if (is_uvar(l1)) { + if (auto v = get_assignment(l1)) { + return is_def_eq(*v, l2); + } else { + update_assignment(l1, l2); + return true; + } + } + + if (is_uvar(l2)) { + if (auto v = get_assignment(l2)) { + return is_def_eq(l1, *v); + } else { + update_assignment(l2, l1); + return true; + } + } + + level new_l1 = normalize(l1); + level new_l2 = normalize(l2); + + if (ignore_universe_def_eq(new_l1, new_l2)) + return true; + + if (l1 != new_l1 || l2 != new_l2) + return is_def_eq(new_l1, new_l2); + + if (l1.kind() != l2.kind()) + return false; + + switch (l1.kind()) { + case level_kind::Max: + return + is_def_eq(max_lhs(l1), max_lhs(l2)) && + is_def_eq(max_rhs(l1), max_rhs(l2)); + case level_kind::IMax: + return + is_def_eq(imax_lhs(l1), imax_lhs(l2)) && + is_def_eq(imax_rhs(l1), imax_rhs(l2)); + case level_kind::Succ: + return is_def_eq(succ_of(l1), succ_of(l2)); + case level_kind::Param: + case level_kind::Global: + return false; + case level_kind::Zero: + case level_kind::Meta: + lean_unreachable(); + } + lean_unreachable(); +} + +bool type_inference::is_def_eq(levels const & ls1, levels const & ls2) { + if (is_nil(ls1) && is_nil(ls2)) { + return true; + } else if (!is_nil(ls1) && !is_nil(ls2)) { + return + is_def_eq(head(ls1), head(ls2)) && + is_def_eq(tail(ls1), tail(ls2)); + } else { + return false; + } +} + +/** \brief Given \c e of the form ?m t_1 ... t_n, where + ?m is an assigned mvar, substitute \c ?m with its assignment. */ +expr type_inference::subst_mvar(expr const & e) { + buffer args; + expr const & m = get_app_args(e, args); + lean_assert(is_mvar(m)); + expr const * v = get_assignment(m); + lean_assert(v); + return apply_beta(*v, args.size(), args.data()); +} + +bool type_inference::has_assigned_uvar(level const & l) const { + if (!has_meta(l)) + return false; + bool found = false; + for_each(l, [&](level const & l) { + if (!has_meta(l)) + return false; // stop search + if (found) + return false; // stop search + if (is_uvar(l) && is_assigned(l)) { + found = true; + return false; // stop search + } + return true; // continue search + }); + return found; +} + +bool type_inference::has_assigned_uvar(levels const & ls) const { + for (level const & l : ls) { + if (has_assigned_uvar(l)) + return true; + } + return false; +} + +bool type_inference::has_assigned_uvar_mvar(expr const & e) const { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return false; + bool found = false; + for_each(e, [&](expr const & e, unsigned) { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return false; // stop search + if (found) + return false; // stop search + if ((is_mvar(e) && is_assigned(e)) || + (is_constant(e) && has_assigned_uvar(const_levels(e))) || + (is_sort(e) && has_assigned_uvar(sort_level(e)))) { + found = true; + return false; // stop search + } + return true; // continue search + }); + return found; +} + +level type_inference::instantiate_uvars(level const & l) { + if (!has_assigned_uvar(l)) + return l; + return replace(l, [&](level const & l) { + if (!has_meta(l)) { + return some_level(l); + } else if (is_uvar(l)) { + if (auto v1 = get_assignment(l)) { + level v2 = instantiate_uvars(*v1); + if (*v1 != v2) { + update_assignment(l, v2); + return some_level(v2); + } else { + return some_level(*v1); + } + } + } + return none_level(); + }); +} + +struct instantiate_uvars_mvars_fn : public replace_visitor { + type_inference & m_owner; + + level visit_level(level const & l) { + return m_owner.instantiate_uvars(l); + } + + levels visit_levels(levels const & ls) { + return map_reuse(ls, + [&](level const & l) { return visit_level(l); }, + [](level const & l1, level const & l2) { return is_eqp(l1, l2); }); + } + + virtual expr visit_sort(expr const & s) { + return update_sort(s, visit_level(sort_level(s))); + } + + virtual expr visit_constant(expr const & c) { + return update_constant(c, visit_levels(const_levels(c))); + } + + virtual expr visit_local(expr const & e) { + return update_mlocal(e, visit(mlocal_type(e))); + } + + virtual expr visit_meta(expr const & m) { + if (m_owner.is_mvar(m)) { + if (auto v1 = m_owner.get_assignment(m)) { + if (!has_expr_metavar(*v1)) { + return *v1; + } else { + expr v2 = m_owner.instantiate_uvars_mvars(*v1); + if (v2 != *v1) + m_owner.update_assignment(m, v2); + return v2; + } + } else { + return m; + } + } else { + return m; + } + } + + virtual expr visit_app(expr const & e) { + buffer args; + expr const & f = get_app_rev_args(e, args); + if (m_owner.is_mvar(f)) { + if (auto v = m_owner.get_assignment(f)) { + expr new_app = apply_beta(*v, args.size(), args.data()); + if (has_expr_metavar(new_app)) + return visit(new_app); + else + return new_app; + } + } + expr new_f = visit(f); + buffer new_args; + bool modified = !is_eqp(new_f, f); + for (expr const & arg : args) { + expr new_arg = visit(arg); + if (!is_eqp(arg, new_arg)) + modified = true; + new_args.push_back(new_arg); + } + if (!modified) + return e; + else + return mk_rev_app(new_f, new_args, e.get_tag()); + } + + virtual expr visit_macro(expr const & e) { + lean_assert(is_macro(e)); + buffer new_args; + for (unsigned i = 0; i < macro_num_args(e); i++) + new_args.push_back(visit(macro_arg(e, i))); + return update_macro(e, new_args.size(), new_args.data()); + } + + virtual expr visit(expr const & e) { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return e; + else + return replace_visitor::visit(e); + } + +public: + instantiate_uvars_mvars_fn(type_inference & o):m_owner(o) {} + + expr operator()(expr const & e) { return visit(e); } +}; + +expr type_inference::instantiate_uvars_mvars(expr const & e) { + if (!has_assigned_uvar_mvar(e)) + return e; + else + return instantiate_uvars_mvars_fn(*this)(e); +} + +bool type_inference::is_prop(expr const & e) { + if (m_env.impredicative()) { + expr t = whnf(infer(e)); + return t == mk_Prop(); + } else { + return false; + } +} + +bool type_inference::is_def_eq_binding(expr e1, expr e2) { + lean_assert(e1.kind() == e2.kind()); + lean_assert(is_binding(e1)); + expr_kind k = e1.kind(); + buffer subst; + do { + optional var_e1_type; + if (binding_domain(e1) != binding_domain(e2)) { + var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); + expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data()); + if (!is_def_eq_core(var_e2_type, *var_e1_type)) + return false; + } + if (!closed(binding_body(e1)) || !closed(binding_body(e2))) { + // local is used inside t or s + if (!var_e1_type) + var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); + subst.push_back(mk_tmp_local(*var_e1_type)); + } else { + expr const & dont_care = mk_Prop(); + subst.push_back(dont_care); + } + e1 = binding_body(e1); + e2 = binding_body(e2); + } while (e1.kind() == k && e2.kind() == k); + return is_def_eq_core(instantiate_rev(e1, subst.size(), subst.data()), + instantiate_rev(e2, subst.size(), subst.data())); +} + +bool type_inference::is_def_eq_args(expr t, expr s) { + while (is_app(t) && is_app(s)) { + if (!is_def_eq_core(app_arg(t), app_arg(s))) + return false; + t = app_fn(t); + s = app_fn(s); + } + return !is_app(t) && !is_app(s); +} + +bool type_inference::is_def_eq_eta(expr const & e1, expr const & e2) { + expr new_e1 = try_eta(e1); + expr new_e2 = try_eta(e2); + if (e1 != new_e1 || e2 != new_e2) { + scope s(*this); + if (is_def_eq_core(new_e1, new_e2)) { + s.commit(); + return true; + } + } + return false; +} + +bool type_inference::is_def_eq_proof_irrel(expr const & e1, expr const & e2) { + if (!m_env.prop_proof_irrel()) + return false; + expr e1_type = infer(e1); + expr e2_type = infer(e2); + if (is_prop(e1_type)) { + scope s(*this); + if (is_def_eq_core(e1_type, e2_type)) { + s.commit(); + return true; + } + } + return false; +} + +/** \brief Given \c ma of the form ?m t_1 ... t_n, (try to) assign + ?m to (an abstraction of) v. Return true if success and false otherwise. */ +bool type_inference::assign_mvar(expr const & ma, expr const & v) { + buffer args; + expr const & m = get_app_args(ma, args); + buffer locals; + for (expr const & arg : args) { + if (!is_tmp_local(arg)) + break; // is not local + if (std::any_of(locals.begin(), locals.end(), [&](expr const & local) { + return mlocal_name(local) == mlocal_name(arg); })) + break; // duplicate local + locals.push_back(arg); + } + lean_assert(is_mvar(m)); + expr new_v = instantiate_uvars_mvars(v); + + if (!validate_assignment(m, locals, v)) + return false; + + if (args.empty()) { + // easy case + update_assignment(m, new_v); + return true; + } else if (args.size() == locals.size()) { + update_assignment(m, Fun(locals, new_v)); + return true; + } else { + // This case is imprecise since it is not a higher order pattern. + // That the term \c ma is of the form (?m t_1 ... t_n) and the t_i's are not pairwise + // distinct local constants. + expr m_type = infer_metavar(m); + for (unsigned i = 0; i < args.size(); i++) { + m_type = whnf(m_type); + if (!is_pi(m_type)) + return false; + lean_assert(i <= locals.size()); + if (i == locals.size()) + locals.push_back(mk_tmp_local(binding_domain(m_type))); + lean_assert(i < locals.size()); + m_type = instantiate(binding_body(m_type), locals[i]); + } + lean_assert(locals.size() == args.size()); + update_assignment(m, Fun(locals, new_v)); + return true; + } +} + +/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */ +lbool type_inference::quick_is_def_eq(expr const & e1, expr const & e2) { + if (e1 == e2) + return l_true; + + expr const & f1 = get_app_fn(e1); + if (is_mvar(f1)) { + if (is_assigned(f1)) { + return to_lbool(is_def_eq_core(subst_mvar(e1), e2)); + } else { + return to_lbool(assign_mvar(e1, e2)); + } + } + + expr const & f2 = get_app_fn(e2); + if (is_mvar(f2)) { + if (is_assigned(f2)) { + return to_lbool(is_def_eq_core(e1, subst_mvar(e2))); + } else { + return to_lbool(assign_mvar(e2, e1)); + } + } + + if (e1.kind() == e2.kind()) { + switch (e1.kind()) { + case expr_kind::Lambda: case expr_kind::Pi: + return to_lbool(is_def_eq_binding(e1, e2)); + case expr_kind::Sort: + return to_lbool(is_def_eq(sort_level(e1), sort_level(e2))); + case expr_kind::Meta: case expr_kind::Var: + case expr_kind::Local: case expr_kind::App: + case expr_kind::Constant: case expr_kind::Macro: + // We do not handle these cases in this method. + break; + } + } + return l_undef; // This is not an "easy case" +} + +auto type_inference::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status { + auto d_t = is_delta(t_n); + auto d_s = is_delta(s_n); + if (!d_t && !d_s) { + return reduction_status::DefUnknown; + } else if (d_t && !d_s) { + t_n = whnf_core(unfold_names(t_n, 0)); + } else if (!d_t && d_s) { + s_n = whnf_core(unfold_names(s_n, 0)); + } else if (d_t->get_height() > d_s->get_height()) { + t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1)); + } else if (d_t->get_height() < d_s->get_height()) { + s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1)); + } else { + if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { + if (!is_opaque(*d_t)) { + scope s(*this); + if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) && + is_def_eq_args(t_n, s_n)) { + s.commit(); + return reduction_status::DefEqual; + } + } + } + t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1)); + s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1)); + } + switch (quick_is_def_eq(t_n, s_n)) { + case l_true: return reduction_status::DefEqual; + case l_false: return reduction_status::DefDiff; + case l_undef: return reduction_status::Continue; + } + lean_unreachable(); +} + +lbool type_inference::lazy_delta_reduction(expr & t_n, expr & s_n) { + while (true) { + switch (lazy_delta_reduction_step(t_n, s_n)) { + case reduction_status::Continue: break; + case reduction_status::DefUnknown: return l_undef; + case reduction_status::DefEqual: return l_true; + case reduction_status::DefDiff: return l_false; + } + } +} + +auto type_inference::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status { + auto new_t_n = norm_ext(t_n); + auto new_s_n = norm_ext(s_n); + if (!new_t_n && !new_s_n) + return reduction_status::DefUnknown; + if (new_t_n) + t_n = whnf_core(*new_t_n); + if (new_s_n) + s_n = whnf_core(*new_s_n); + switch (quick_is_def_eq(t_n, s_n)) { + case l_true: return reduction_status::DefEqual; + case l_false: return reduction_status::DefDiff; + case l_undef: return reduction_status::Continue; + } + lean_unreachable(); +} + +// Apply lazy delta-reduction and then normalizer extensions +lbool type_inference::reduce_def_eq(expr & t_n, expr & s_n) { + while (true) { + // first, keep applying lazy delta-reduction while applicable + lbool r = lazy_delta_reduction(t_n, s_n); + if (r != l_undef) return r; + + // try normalizer extensions + switch (ext_reduction_step(t_n, s_n)) { + case reduction_status::Continue: break; + case reduction_status::DefUnknown: return l_undef; + case reduction_status::DefEqual: return l_true; + case reduction_status::DefDiff: return l_false; + } + } +} + +bool type_inference::is_def_eq_core(expr const & t, expr const & s) { + check_system("is_definitionally_equal"); + lbool r = quick_is_def_eq(t, s); + if (r != l_undef) return r == l_true; + + 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_def_eq(t_n, s_n); + if (r != l_undef) return r == l_true; + } + + r = reduce_def_eq(t_n, s_n); + if (r != l_undef) return r == l_true; + + if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n)) { + scope s(*this); + if (is_def_eq(const_levels(t_n), const_levels(s_n))) { + s.commit(); + return true; + } + } + + if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n)) + return true; + + if (is_app(t_n) && is_app(s_n)) { + scope s(*this); + if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) && + is_def_eq_args(t_n, s_n)) { + s.commit(); + return true; + } + } + + if (is_def_eq_eta(t_n, s_n)) + return true; + + if (is_def_eq_proof_irrel(t_n, s_n)) + return true; + + return false; +} + +bool type_inference::is_def_eq(expr const & e1, expr const & e2) { + scope s(*this); + if (is_def_eq_core(e1, e2)) { + s.commit(); + return true; + } + return false; +} + +expr type_inference::infer_constant(expr const & e) { + declaration d = m_env.get(const_name(e)); + auto const & ps = d.get_univ_params(); + auto const & ls = const_levels(e); + if (length(ps) != length(ls)) + throw exception("infer type failed, incorrect number of universe levels"); + return instantiate_type_univ_params(d, ls); +} + +expr type_inference::infer_macro(expr const & e) { + auto def = macro_def(e); + bool infer_only = true; + // Remark: we are ignoring constraints generated by the macro definition. + return def.check_type(e, *m_ext_ctx, infer_only).first; +} + +expr type_inference::infer_lambda(expr e) { + buffer es, ds, ls; + while (is_lambda(e)) { + es.push_back(e); + ds.push_back(binding_domain(e)); + expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); + expr l = mk_tmp_local(d, binding_info(e)); + ls.push_back(l); + e = binding_body(e); + } + expr t = infer(instantiate_rev(e, ls.size(), ls.data())); + expr r = abstract_locals(t, ls.size(), ls.data()); + unsigned i = es.size(); + while (i > 0) { + --i; + r = mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i])); + } + return r; +} + +/** \brief Make sure \c e is a sort, if it is not throw an exception using \c ref as a reference */ +void type_inference::ensure_sort(expr const & e, expr const & /* ref */) { + // Remark: for simplicity reasons, we just fail if \c e is not a sort. + if (!is_sort(e)) + throw exception("infer type failed, sort expected"); +} + +expr type_inference::infer_pi(expr const & e0) { + buffer ls; + buffer us; + expr e = e0; + while (is_pi(e)) { + expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); + expr d_type = whnf(infer(d)); + ensure_sort(d_type, e0); + us.push_back(sort_level(d_type)); + expr l = mk_tmp_local(d, binding_info(e)); + ls.push_back(l); + e = binding_body(e); + } + e = instantiate_rev(e, ls.size(), ls.data()); + expr e_type = whnf(infer(e)); + ensure_sort(e_type, e0); + level r = sort_level(e_type); + unsigned i = ls.size(); + bool imp = m_env.impredicative(); + while (i > 0) { + --i; + r = imp ? mk_imax(us[i], r) : mk_max(us[i], r); + } + return mk_sort(r); +} + +/** \brief Make sure \c e is a Pi-expression, if it is not throw an exception using \c ref as a reference */ +void type_inference::ensure_pi(expr const & e, expr const & /* ref */) { + // Remark: for simplicity reasons, we just fail if \c e is not a Pi. + if (!is_pi(e)) + throw exception("infer type failed, Pi expected"); + // Potential problem: e is of the form (f ...) where f is a constant that is not marked as reducible. + // So, whnf does not reduce it, and we fail to detect that e is can be reduced to a Pi-expression. +} + +expr type_inference::infer_app(expr const & e) { + buffer args; + expr const & f = get_app_args(e, args); + expr f_type = infer(f); + unsigned j = 0; + unsigned nargs = args.size(); + for (unsigned i = 0; i < nargs; i++) { + if (is_pi(f_type)) { + f_type = binding_body(f_type); + } else { + f_type = whnf(instantiate_rev(f_type, i-j, args.data()+j)); + ensure_pi(f_type, e); + f_type = binding_body(f_type); + j = i; + } + } + return instantiate_rev(f_type, nargs-j, args.data()+j); +} + +expr type_inference::infer(expr const & e) { + lean_assert(!is_var(e)); + lean_assert(closed(e)); + check_system("infer_type"); + + expr r; + switch (e.kind()) { + case expr_kind::Local: + r = infer_local(e); + break; + case expr_kind::Meta: + r = infer_metavar(e); + break; + case expr_kind::Var: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Sort: + r = mk_sort(mk_succ(sort_level(e))); + break; + case expr_kind::Constant: + r = infer_constant(e); + break; + case expr_kind::Macro: + r = infer_macro(e); + break; + case expr_kind::Lambda: + r = infer_lambda(e); + break; + case expr_kind::Pi: + r = infer_pi(e); + break; + case expr_kind::App: + r = infer_app(e); + break; + } + // TODO(Leo): cache results if we have performance problems + return r; +} + +void type_inference::clear_cache() { +} + +void initialize_type_inference() { + g_prefix = new name(name::mk_internal_unique_name()); +} + +void finalize_type_inference() { + delete g_prefix; +} +} diff --git a/src/library/type_inference.h b/src/library/type_inference.h new file mode 100644 index 000000000..ee9de4069 --- /dev/null +++ b/src/library/type_inference.h @@ -0,0 +1,180 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "kernel/environment.h" +#include "library/projection.h" + +namespace lean { +/** \brief Light-weight type inference, normalization and definitional equality. + It is simpler and more efficient version of the kernel type checker. + It does not generate unification constraints. + Unification problems are eagerly solved. However, only higher-order patterns + are supported. + + This is a generic class containing several virtual methods that must + be implemeneted by "customers" (e.g., type class resolution procedure, blast tactic). +*/ +class type_inference { + struct ext_ctx; + friend struct ext_ctx; + environment m_env; + name_generator m_ngen; + std::unique_ptr m_ext_ctx; + name_map m_proj_info; + + bool is_opaque(declaration const & d) const; + optional expand_macro(expr const & m); + optional reduce_projection(expr const & e); + optional norm_ext(expr const & e); + expr whnf_core(expr const & e); + expr unfold_name_core(expr e, unsigned h); + expr unfold_names(expr const & e, unsigned h); + optional is_delta(expr const & e) const; + expr whnf_core(expr e, unsigned h); + + bool is_def_eq(level const & l1, level const & l2); + bool is_def_eq(levels const & ls1, levels const & ls2); + + lbool quick_is_def_eq(expr const & e1, expr const & e2); + bool is_def_eq_core(expr const & e1, expr const & e2); + bool is_def_eq_args(expr t, expr s); + bool is_def_eq_binding(expr e1, expr e2); + bool is_def_eq_eta(expr const & e1, expr const & e2); + bool is_def_eq_proof_irrel(expr const & e1, expr const & e2); + + expr subst_mvar(expr const & e); + bool assign_mvar(expr const & ma, expr const & v); + enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff }; + reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n); + lbool lazy_delta_reduction(expr & t_n, expr & s_n); + reduction_status ext_reduction_step(expr & t_n, expr & s_n); + lbool reduce_def_eq(expr & t_n, expr & s_n); + + expr infer_constant(expr const & e); + expr infer_macro(expr const & e); + expr infer_lambda(expr e); + expr infer_pi(expr const & e); + expr infer_app(expr const & e); + void ensure_sort(expr const & e, expr const & ref); + void ensure_pi(expr const & e, expr const & ref); + + struct scope { + type_inference & m_owner; + bool m_keep; + scope(type_inference & o):m_owner(o), m_keep(false) { m_owner.push(); } + ~scope() { if (!m_keep) m_owner.pop(); } + void commit() { m_owner.commit(); m_keep = true; } + }; + +public: + type_inference(environment const & env); + virtual ~type_inference(); + + /** \brief Opaque constants are never unfolded by this procedure. + The is_def_eq method will lazily unfold non-opaque constants. + + \remark This class always treats projections and theorems as opaque. */ + virtual bool is_extra_opaque(name const & n) const = 0; + + /** \brief Create a temporary local constant */ + virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) = 0; + + /** \brief Return true if \c e was created using \c mk_tmp_local */ + virtual bool is_tmp_local(expr const & e) const = 0; + + /** \brief Return true if \c l represents a universe unification variable. + \remark This is supposed to be a subset of is_meta(l). + \remark This method is only invoked when is_meta(l) is true. */ + virtual bool is_uvar(level const & l) const = 0; + + /** \brief This method is invoked by is_def_eq for universe terms. It allows the customer + to ignore a unification sub-problem for universe terms. */ + virtual bool ignore_universe_def_eq(level const &, level const &) const { return false; } + + /** \brief Return true if \c e represents a unification variable. + \remark This is supposed to be a subset of is_metavar(e). + \remark This method is only invoked when is_metavar(l) is true. + This module will only assign a metavariable \c m when is_mvar(m) is true. + This feature allows us to treat some (external) meta-variables as constants. */ + virtual bool is_mvar(expr const & e) const = 0; + + /** \brief Return the assignment for universe unification variable + \c u, and nullptr if it is not assigned. + \pre is_uvar(u) */ + virtual level const * get_assignment(level const & u) const = 0; + + /** \brief Return the assignment for unification variable + \c m, and nullptr if it is not assigned. + \pre is_mvar(u) */ + virtual expr const * get_assignment(expr const & m) const = 0; + + /** \brief Update the assignment for \c u. + \pre is_uvar(u) */ + virtual void update_assignment(level const & u, level const & v) = 0; + /** \brief Update the assignment for \c m. + \pre is_mvar(m) */ + virtual void update_assignment(expr const & m, expr const & v) = 0; + /** \brief Given a metavariable m that takes locals as arguments, this method + should return true if m can be assigned to an abstraction of \c v. + + \remark This method should check at least if m does not occur in v, + and if all tmp locals in v are in locals. */ + virtual bool validate_assignment(expr const & m, buffer const & locals, expr const & v) = 0; + + /** \brief Return the type of a local constant (local or not). + \remark This method allows the customer to store the type of local constants + in a different place. */ + virtual expr infer_local(expr const & e) const = 0; + + /** \brief Return the type of a meta-variable (even if it is not a unification one) */ + virtual expr infer_metavar(expr const & e) const = 0; + + /** \brief Save the current assignment */ + virtual void push() = 0; + /** \brief Retore assignment (inverse for push) */ + virtual void pop() = 0; + /** \brief Keep the changes since last push */ + virtual void commit() = 0; + + bool is_assigned(level const & u) const { return get_assignment(u) != nullptr; } + bool is_assigned(expr const & m) const { return get_assignment(m) != nullptr; } + + bool has_assigned_uvar(level const & l) const; + bool has_assigned_uvar(levels const & ls) const; + bool has_assigned_uvar_mvar(expr const & e) const; + + /** \brief Instantiate assigned universe unification variables occurring in \c l */ + level instantiate_uvars(level const & l); + + /** \brief Instantiate assigned unification variables occurring in \c e */ + expr instantiate_uvars_mvars(expr const & e); + + /** \brief Put the given term in weak-head-normal-form (modulo is_opaque predicate) */ + expr whnf(expr const & e); + + /** \brief Return true if \c e is a proposition */ + bool is_prop(expr const & e); + + /** \brief Infer the type of \c e. */ + expr infer(expr const & e); + + /** \brief Return true if \c e1 and \c e2 are definitionally equal. + When \c e1 and \c e2, this method is not as complete as the one in the kernel. + That is, it may return false even when \c e1 and \c e2 may be definitionally equal. + + It is precise if \c e1 and \c e2 do not contain metavariables. + */ + bool is_def_eq(expr const & e1, expr const & e2); + + /** \brief Clear internal caches used to speedup computation */ + void clear_cache(); +}; + +void initialize_type_inference(); +void finalize_type_inference(); +}