From 3f06f7b6fd373972dc64034e05f7498d3a7095f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Feb 2015 11:33:37 -0800 Subject: [PATCH] refactor(kernel): move default_converter to its own module --- src/kernel/CMakeLists.txt | 3 +- src/kernel/converter.cpp | 511 +------------------------------ src/kernel/default_converter.cpp | 508 ++++++++++++++++++++++++++++++ src/kernel/default_converter.h | 74 +++++ src/kernel/init_module.cpp | 3 + 5 files changed, 588 insertions(+), 511 deletions(-) create mode 100644 src/kernel/default_converter.cpp create mode 100644 src/kernel/default_converter.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 766c3f9be..6f46e2e02 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -3,6 +3,7 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp formatter.cpp declaration.cpp environment.cpp justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp -normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp) +normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp +default_converter.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 97d2b6018..50b528bcc 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/free_vars.h" #include "kernel/type_checker.h" +#include "kernel/default_converter.h" namespace lean { // Temporary hack for ignoring opaque annotations in the kernel @@ -112,514 +113,6 @@ std::unique_ptr mk_dummy_converter() { name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); } pair converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); } extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); } -static expr * g_dont_care = nullptr; - -struct default_converter : public converter { - environment m_env; - optional m_module_idx; - bool m_memoize; - extra_opaque_pred m_extra_pred; - expr_struct_map m_whnf_core_cache; - expr_struct_map> m_whnf_cache; - - default_converter(environment const & env, optional mod_idx, bool memoize, - extra_opaque_pred const & pred): - m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) { - } - - constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { - return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast(m_module_idx)); - } - - optional expand_macro(expr const & m, type_checker & c) { - lean_assert(is_macro(m)); - return macro_def(m).expand(m, get_extension(c)); - } - - /** \brief Apply normalizer extensions to \c e. */ - optional> norm_ext(expr const & e, type_checker & c) { - return m_env.norm_ext()(e, get_extension(c)); - } - - optional d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs) { - if (auto r = norm_ext(e, c)) { - cs = cs + r->second; - return some_expr(r->first); - } else { - return none_expr(); - } - } - - /** \brief Return true if \c e may be reduced later after metavariables are instantiated. */ - bool may_reduce_later(expr const & e, type_checker & c) { - return static_cast(m_env.norm_ext().may_reduce_later(e, get_extension(c))); - } - - /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ - expr whnf_core(expr const & e, type_checker & c) { - check_system("whnf"); - - // handle 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: case expr_kind::Constant: case expr_kind::Lambda: - return e; - case expr_kind::Macro: case expr_kind::App: - break; - } - - // check cache - if (m_memoize) { - auto it = m_whnf_core_cache.find(e); - if (it != m_whnf_core_cache.end()) - return it->second; - } - - // do the actual work - expr r; - 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: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Macro: - if (auto m = expand_macro(e, c)) - r = whnf_core(*m, c); - else - r = e; - break; - case expr_kind::App: { - buffer args; - expr f0 = get_app_rev_args(e, args); - expr f = whnf_core(f0, c); - 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); - r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c); - } else { - r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()), c); - } - break; - }} - - if (m_memoize) - m_whnf_core_cache.insert(mk_pair(e, r)); - return r; - } - - bool is_opaque_core(declaration const & d) const { - return ::lean::is_opaque(d, m_extra_pred, m_module_idx); - } - - virtual bool is_opaque(declaration const & d) const { - return is_opaque_core(d); - } - - /** \brief Expand \c e if it is non-opaque constant with weight >= w */ - expr unfold_name_core(expr e, unsigned w) { - if (is_constant(e)) { - if (auto d = m_env.find(const_name(e))) { - if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w) - return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w); - } - } - 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 weight >= w. - */ - expr unfold_names(expr const & e, unsigned w) { - if (is_app(e)) { - expr f0 = get_app_fn(e); - expr f = unfold_name_core(f0, w); - 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, w); - } - } - - /** - \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 is_delta(expr const & e) { - return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx); - } - - /** - \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with - weight greater than or equal to \c w. - - 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 whnf_core(expr e, unsigned w, type_checker & c) { - while (true) { - expr new_e = unfold_names(whnf_core(e, c), w); - if (is_eqp(e, new_e)) - return e; - e = new_e; - } - } - - /** \brief Put expression \c t in weak head normal form */ - virtual pair whnf(expr const & e_prime, type_checker & c) { - // Do not cache easy cases - switch (e_prime.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: - return to_ecs(e_prime); - case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: - break; - } - - expr e = e_prime; - // check cache - if (m_memoize) { - auto it = m_whnf_cache.find(e); - if (it != m_whnf_cache.end()) - return it->second; - } - - expr t = e; - constraint_seq cs; - while (true) { - expr t1 = whnf_core(t, 0, c); - if (auto new_t = d_norm_ext(t1, c, cs)) { - t = *new_t; - } else { - auto r = mk_pair(t1, cs); - if (m_memoize) - m_whnf_cache.insert(mk_pair(e, r)); - return r; - } - } - } - - expr whnf(expr const & e_prime, type_checker & c, constraint_seq & cs) { - auto r = whnf(e_prime, c); - cs = cs + r.second; - return r.first; - } - - pair to_bcs(bool b) { return mk_pair(b, constraint_seq()); } - pair to_bcs(bool b, constraint const & c) { return mk_pair(b, constraint_seq(c)); } - pair to_bcs(bool b, constraint_seq const & cs) { return mk_pair(b, cs); } - - /** - \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s. - - t and s are definitionally equal - iff - domain(t) is definitionally equal to domain(s) - and - body(t) is definitionally equal to body(s) - */ - bool is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - lean_assert(t.kind() == s.kind()); - lean_assert(is_binding(t)); - expr_kind k = t.kind(); - buffer subst; - do { - optional var_s_type; - if (binding_domain(t) != binding_domain(s)) { - var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data()); - expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data()); - if (!is_def_eq(var_t_type, *var_s_type, c, jst, cs)) - return false; - } - if (!closed(binding_body(t)) || !closed(binding_body(s))) { - // local is used inside t or s - if (!var_s_type) - var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data()); - subst.push_back(mk_local(mk_fresh_name(c), binding_name(s), *var_s_type, binding_info(s))); - } else { - subst.push_back(*g_dont_care); // don't care - } - t = binding_body(t); - s = binding_body(s); - } while (t.kind() == k && s.kind() == k); - return is_def_eq(instantiate_rev(t, subst.size(), subst.data()), - instantiate_rev(s, subst.size(), subst.data()), c, jst, cs); - } - - bool is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs) { - if (is_equivalent(l1, l2)) { - return true; - } else if (has_meta(l1) || has_meta(l2)) { - cs = cs + constraint_seq(mk_level_eq_cnstr(l1, l2, jst.get())); - return true; - } else { - return false; - } - } - - bool is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - 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), jst, cs) && - is_def_eq(tail(ls1), tail(ls2), c, jst, cs); - } else { - return false; - } - } - - static pair to_lbcs(lbool l) { return mk_pair(l, constraint_seq()); } - static pair to_lbcs(lbool l, constraint const & c) { return mk_pair(l, constraint_seq(c)); } - static pair to_lbcs(pair const & bcs) { - return mk_pair(to_lbool(bcs.first), bcs.second); - } - - /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */ - lbool quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - 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 - cs = cs + constraint_seq(mk_eq_cnstr(t, s, jst.get())); - return l_true; - } - if (t.kind() == s.kind()) { - switch (t.kind()) { - case expr_kind::Lambda: case expr_kind::Pi: - return to_lbool(is_def_eq_binding(t, s, c, jst, cs)); - case expr_kind::Sort: - return to_lbool(is_def_eq(sort_level(t), sort_level(s), c, jst, cs)); - case expr_kind::Meta: - lean_unreachable(); // LCOV_EXCL_LINE - 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" - } - - /** - \brief Return true if arguments of \c t are definitionally equal to arguments of \c s. - This method is used to implement an optimization in the method \c is_def_eq. - */ - bool is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - while (is_app(t) && is_app(s)) { - if (!is_def_eq(app_arg(t), app_arg(s), c, jst, cs)) - return false; - t = app_fn(t); - s = app_fn(s); - } - return !is_app(t) && !is_app(s); - } - - /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */ - bool is_app_of(expr t, name const & f_name) { - t = get_app_fn(t); - return is_constant(t) && const_name(t) == f_name; - } - - /** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */ - bool try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - if (is_lambda(t) && !is_lambda(s)) { - auto tcs = infer_type(c, s); - auto wcs = whnf(tcs.first, c); - expr s_type = wcs.first; - if (!is_pi(s_type)) - return false; - expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type)); - auto dcs = is_def_eq(t, new_s, c, jst); - if (!dcs.first) - return false; - cs = cs + dcs.second + wcs.second + tcs.second; - return true; - } else { - return false; - } - } - - bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { - auto bcs = is_def_eq(t, s, c, jst); - if (bcs.first) { - cs = cs + bcs.second; - return true; - } else { - return false; - } - } - - /** Return true iff t is definitionally equal to s. */ - virtual pair is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) { - check_system("is_definitionally_equal"); - constraint_seq cs; - lbool r = quick_is_def_eq(t, s, c, jst, cs); - if (r != l_undef) return to_bcs(r == l_true, cs); - - // apply whnf (without using delta-reduction or normalizer extensions) - expr t_n = whnf_core(t, c); - expr s_n = whnf_core(s, c); - - if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { - r = quick_is_def_eq(t_n, s_n, c, jst, cs); - if (r != l_undef) return to_bcs(r == l_true, cs); - } - - // lazy delta-reduction and then normalizer extensions - while (true) { - // first, keep applying lazy delta-reduction while applicable - while (true) { - auto d_t = is_delta(t_n); - auto d_s = is_delta(s_n); - if (!d_t && !d_s) { - break; - } else if (d_t && !d_s) { - t_n = whnf_core(unfold_names(t_n, 0), c); - } else if (!d_t && d_s) { - s_n = whnf_core(unfold_names(s_n, 0), c); - } else if (d_t->get_weight() > d_s->get_weight()) { - t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c); - } else if (d_t->get_weight() < d_s->get_weight()) { - s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c); - } else { - lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); - if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { - // If t_n and s_n are both applications of the same (non-opaque) definition, - if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { - // We let the unifier deal with cases such as - // (f ...) =?= (f ...) - // when t_n or s_n contains metavariables - break; - } else { - // Optimization: - // We try to check if their arguments are definitionally equal. - // If they are, then t_n and s_n must be definitionally equal, and we can - // skip the delta-reduction step. - // If the flag use_conv_opt() is not true, then we skip this optimization - if (!is_opaque_core(*d_t) && d_t->use_conv_opt() && - is_def_eq_args(t_n, s_n, c, jst, cs)) - return to_bcs(true, cs); - } - } - t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c); - s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c); - } - r = quick_is_def_eq(t_n, s_n, c, jst, cs); - if (r != l_undef) return to_bcs(r == l_true, cs); - } - // try normalizer extensions - auto new_t_n = d_norm_ext(t_n, c, cs); - auto new_s_n = d_norm_ext(s_n, c, cs); - if (!new_t_n && !new_s_n) - break; // t_n and s_n are in weak head normal form - if (new_t_n) - t_n = whnf_core(*new_t_n, c); - if (new_s_n) - s_n = whnf_core(*new_s_n, c); - r = quick_is_def_eq(t_n, s_n, c, jst, cs); - if (r != l_undef) return to_bcs(r == l_true, cs); - } - - if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) && - is_def_eq(const_levels(t_n), const_levels(s_n), c, jst, cs)) - return to_bcs(true, cs); - - if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n)) - return to_bcs(true, cs); - - optional d_t, d_s; - bool delay_check = false; - if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { - d_t = is_delta(t_n); - d_s = is_delta(s_n); - if (d_t && d_s && is_eqp(*d_t, *d_s)) - delay_check = true; - else if (may_reduce_later(t_n, c) && may_reduce_later(s_n, c)) - delay_check = true; - } - - // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance) - if (!delay_check && is_app(t_n) && is_app(s_n)) { - buffer t_args; - buffer s_args; - expr t_fn = get_app_args(t_n, t_args); - expr s_fn = get_app_args(s_n, s_args); - constraint_seq cs_prime = cs; - if (is_def_eq(t_fn, s_fn, c, jst, cs_prime) && t_args.size() == s_args.size()) { - unsigned i = 0; - for (; i < t_args.size(); i++) { - if (!is_def_eq(t_args[i], s_args[i], c, jst, cs_prime)) - break; - } - if (i == t_args.size()) { - return to_bcs(true, cs_prime); - } - } - } - - if (try_eta_expansion(t_n, s_n, c, jst, cs) || - try_eta_expansion(s_n, t_n, c, jst, cs)) - return to_bcs(true, cs); - - if (m_env.prop_proof_irrel()) { - // Proof irrelevance support for Prop (aka Type.{0}) - auto tcs = infer_type(c, t); - auto scs = infer_type(c, s); - expr t_type = tcs.first; - expr s_type = scs.first; - // remark: is_prop returns true only if t_type reducible to Prop. - // If t_type contains metavariables, then reduction can get stuck, and is_prop will return false. - auto pcs = is_prop(t_type, c); - if (pcs.first) { - auto dcs = is_def_eq(t_type, s_type, c, jst); - if (dcs.first) - return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second); - } else { - // If we can't stablish whether t_type is Prop, we try s_type. - pcs = is_prop(s_type, c); - if (pcs.first) { - auto dcs = is_def_eq(t_type, s_type, c, jst); - if (dcs.first) - return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second); - } - // This procedure will miss the case where s_type and t_type cannot be reduced to Prop - // because they contain metavariables. - } - } - - if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c) || delay_check) { - cs = cs + constraint_seq(mk_eq_cnstr(t_n, s_n, jst.get())); - return to_bcs(true, cs); - } - - return to_bcs(false); - } - - pair is_prop(expr const & e, type_checker & c) { - auto tcs = infer_type(c, e); - auto wcs = whnf(tcs.first, c); - if (wcs.first == mk_Prop()) - return to_bcs(true, wcs.second + tcs.second); - else - return to_bcs(false); - } - - virtual optional get_module_idx() const { - return m_module_idx; - } -}; std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, bool memoize, extra_opaque_pred const & pred) { @@ -643,12 +136,10 @@ std::unique_ptr mk_default_converter(environment const & env, bool un void initialize_converter() { g_opt_main_module_idx = new optional(g_main_module_idx); g_no_delayed_jst = new no_delayed_justification(); - g_dont_care = new expr(Const("dontcare")); } void finalize_converter() { delete g_opt_main_module_idx; delete g_no_delayed_jst; - delete g_dont_care; } } diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp new file mode 100644 index 000000000..fbf368ace --- /dev/null +++ b/src/kernel/default_converter.cpp @@ -0,0 +1,508 @@ +/* +Copyright (c) 2014-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/default_converter.h" +#include "kernel/instantiate.h" +#include "kernel/free_vars.h" +#include "kernel/type_checker.h" + +namespace lean { +static expr * g_dont_care = nullptr; + +default_converter::default_converter(environment const & env, optional mod_idx, bool memoize, + extra_opaque_pred const & pred): + m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) { +} + +constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { + return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast(m_module_idx)); +} + +optional default_converter::expand_macro(expr const & m, type_checker & c) { + lean_assert(is_macro(m)); + return macro_def(m).expand(m, get_extension(c)); +} + +/** \brief Apply normalizer extensions to \c e. */ +optional> default_converter::norm_ext(expr const & e, type_checker & c) { + return m_env.norm_ext()(e, get_extension(c)); +} + +optional default_converter::d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs) { + if (auto r = norm_ext(e, c)) { + cs = cs + r->second; + return some_expr(r->first); + } else { + return none_expr(); + } +} + +/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */ +bool default_converter::may_reduce_later(expr const & e, type_checker & c) { + return static_cast(m_env.norm_ext().may_reduce_later(e, get_extension(c))); +} + +/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ +expr default_converter::whnf_core(expr const & e, type_checker & c) { + check_system("whnf"); + + // handle 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: case expr_kind::Constant: case expr_kind::Lambda: + return e; + case expr_kind::Macro: case expr_kind::App: + break; + } + + // check cache + if (m_memoize) { + auto it = m_whnf_core_cache.find(e); + if (it != m_whnf_core_cache.end()) + return it->second; + } + + // do the actual work + expr r; + 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: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Macro: + if (auto m = expand_macro(e, c)) + r = whnf_core(*m, c); + else + r = e; + break; + case expr_kind::App: { + buffer args; + expr f0 = get_app_rev_args(e, args); + expr f = whnf_core(f0, c); + 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); + r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c); + } else { + r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()), c); + } + break; + }} + + if (m_memoize) + m_whnf_core_cache.insert(mk_pair(e, r)); + return r; +} + +bool default_converter::is_opaque_core(declaration const & d) const { + return ::lean::is_opaque(d, m_extra_pred, m_module_idx); +} + +bool default_converter::is_opaque(declaration const & d) const { + return is_opaque_core(d); +} + +/** \brief Expand \c e if it is non-opaque constant with weight >= w */ +expr default_converter::unfold_name_core(expr e, unsigned w) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) { + if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w) + return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w); + } + } + 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 weight >= w. +*/ +expr default_converter::unfold_names(expr const & e, unsigned w) { + if (is_app(e)) { + expr f0 = get_app_fn(e); + expr f = unfold_name_core(f0, w); + 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, w); + } +} + +/** + \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 default_converter::is_delta(expr const & e) { + return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx); +} + +/** + \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with + weight greater than or equal to \c w. + + 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 default_converter::whnf_core(expr e, unsigned w, type_checker & c) { + while (true) { + expr new_e = unfold_names(whnf_core(e, c), w); + if (is_eqp(e, new_e)) + return e; + e = new_e; + } +} + +/** \brief Put expression \c t in weak head normal form */ +pair default_converter::whnf(expr const & e_prime, type_checker & c) { + // Do not cache easy cases + switch (e_prime.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: + return to_ecs(e_prime); + case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: + break; + } + + expr e = e_prime; + // check cache + if (m_memoize) { + auto it = m_whnf_cache.find(e); + if (it != m_whnf_cache.end()) + return it->second; + } + + expr t = e; + constraint_seq cs; + while (true) { + expr t1 = whnf_core(t, 0, c); + if (auto new_t = d_norm_ext(t1, c, cs)) { + t = *new_t; + } else { + auto r = mk_pair(t1, cs); + if (m_memoize) + m_whnf_cache.insert(mk_pair(e, r)); + return r; + } + } +} + +expr default_converter::whnf(expr const & e_prime, type_checker & c, constraint_seq & cs) { + auto r = whnf(e_prime, c); + cs = cs + r.second; + return r.first; +} + + +/** + \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s. + + t and s are definitionally equal + iff + domain(t) is definitionally equal to domain(s) + and + body(t) is definitionally equal to body(s) +*/ +bool default_converter::is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + lean_assert(t.kind() == s.kind()); + lean_assert(is_binding(t)); + expr_kind k = t.kind(); + buffer subst; + do { + optional var_s_type; + if (binding_domain(t) != binding_domain(s)) { + var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data()); + expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data()); + if (!is_def_eq(var_t_type, *var_s_type, c, jst, cs)) + return false; + } + if (!closed(binding_body(t)) || !closed(binding_body(s))) { + // local is used inside t or s + if (!var_s_type) + var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data()); + subst.push_back(mk_local(mk_fresh_name(c), binding_name(s), *var_s_type, binding_info(s))); + } else { + subst.push_back(*g_dont_care); // don't care + } + t = binding_body(t); + s = binding_body(s); + } while (t.kind() == k && s.kind() == k); + return is_def_eq(instantiate_rev(t, subst.size(), subst.data()), + instantiate_rev(s, subst.size(), subst.data()), c, jst, cs); +} + +bool default_converter::is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs) { + if (is_equivalent(l1, l2)) { + return true; + } else if (has_meta(l1) || has_meta(l2)) { + cs = cs + constraint_seq(mk_level_eq_cnstr(l1, l2, jst.get())); + return true; + } else { + return false; + } +} + +bool default_converter::is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + 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), jst, cs) && + is_def_eq(tail(ls1), tail(ls2), c, jst, cs); + } else { + return false; + } +} + +/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */ +lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + 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 + cs = cs + constraint_seq(mk_eq_cnstr(t, s, jst.get())); + return l_true; + } + if (t.kind() == s.kind()) { + switch (t.kind()) { + case expr_kind::Lambda: case expr_kind::Pi: + return to_lbool(is_def_eq_binding(t, s, c, jst, cs)); + case expr_kind::Sort: + return to_lbool(is_def_eq(sort_level(t), sort_level(s), c, jst, cs)); + case expr_kind::Meta: + lean_unreachable(); // LCOV_EXCL_LINE + 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" +} + +/** + \brief Return true if arguments of \c t are definitionally equal to arguments of \c s. + This method is used to implement an optimization in the method \c is_def_eq. +*/ +bool default_converter::is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + while (is_app(t) && is_app(s)) { + if (!is_def_eq(app_arg(t), app_arg(s), c, jst, cs)) + return false; + t = app_fn(t); + s = app_fn(s); + } + return !is_app(t) && !is_app(s); +} + +/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */ +bool default_converter::is_app_of(expr t, name const & f_name) { + t = get_app_fn(t); + return is_constant(t) && const_name(t) == f_name; +} + +/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */ +bool default_converter::try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + if (is_lambda(t) && !is_lambda(s)) { + auto tcs = infer_type(c, s); + auto wcs = whnf(tcs.first, c); + expr s_type = wcs.first; + if (!is_pi(s_type)) + return false; + expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type)); + auto dcs = is_def_eq(t, new_s, c, jst); + if (!dcs.first) + return false; + cs = cs + dcs.second + wcs.second + tcs.second; + return true; + } else { + return false; + } +} + +bool default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) { + auto bcs = is_def_eq(t, s, c, jst); + if (bcs.first) { + cs = cs + bcs.second; + return true; + } else { + return false; + } +} + +/** Return true iff t is definitionally equal to s. */ +pair default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) { + check_system("is_definitionally_equal"); + constraint_seq cs; + lbool r = quick_is_def_eq(t, s, c, jst, cs); + if (r != l_undef) return to_bcs(r == l_true, cs); + + // apply whnf (without using delta-reduction or normalizer extensions) + expr t_n = whnf_core(t, c); + expr s_n = whnf_core(s, c); + + if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { + r = quick_is_def_eq(t_n, s_n, c, jst, cs); + if (r != l_undef) return to_bcs(r == l_true, cs); + } + + // lazy delta-reduction and then normalizer extensions + while (true) { + // first, keep applying lazy delta-reduction while applicable + while (true) { + auto d_t = is_delta(t_n); + auto d_s = is_delta(s_n); + if (!d_t && !d_s) { + break; + } else if (d_t && !d_s) { + t_n = whnf_core(unfold_names(t_n, 0), c); + } else if (!d_t && d_s) { + s_n = whnf_core(unfold_names(s_n, 0), c); + } else if (d_t->get_weight() > d_s->get_weight()) { + t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c); + } else if (d_t->get_weight() < d_s->get_weight()) { + s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c); + } else { + lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); + if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { + // If t_n and s_n are both applications of the same (non-opaque) definition, + if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { + // We let the unifier deal with cases such as + // (f ...) =?= (f ...) + // when t_n or s_n contains metavariables + break; + } else { + // Optimization: + // We try to check if their arguments are definitionally equal. + // If they are, then t_n and s_n must be definitionally equal, and we can + // skip the delta-reduction step. + // If the flag use_conv_opt() is not true, then we skip this optimization + if (!is_opaque_core(*d_t) && d_t->use_conv_opt() && + is_def_eq_args(t_n, s_n, c, jst, cs)) + return to_bcs(true, cs); + } + } + t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c); + s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c); + } + r = quick_is_def_eq(t_n, s_n, c, jst, cs); + if (r != l_undef) return to_bcs(r == l_true, cs); + } + // try normalizer extensions + auto new_t_n = d_norm_ext(t_n, c, cs); + auto new_s_n = d_norm_ext(s_n, c, cs); + if (!new_t_n && !new_s_n) + break; // t_n and s_n are in weak head normal form + if (new_t_n) + t_n = whnf_core(*new_t_n, c); + if (new_s_n) + s_n = whnf_core(*new_s_n, c); + r = quick_is_def_eq(t_n, s_n, c, jst, cs); + if (r != l_undef) return to_bcs(r == l_true, cs); + } + + if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) && + is_def_eq(const_levels(t_n), const_levels(s_n), c, jst, cs)) + return to_bcs(true, cs); + + if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n)) + return to_bcs(true, cs); + + optional d_t, d_s; + bool delay_check = false; + if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { + d_t = is_delta(t_n); + d_s = is_delta(s_n); + if (d_t && d_s && is_eqp(*d_t, *d_s)) + delay_check = true; + else if (may_reduce_later(t_n, c) && may_reduce_later(s_n, c)) + delay_check = true; + } + + // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance) + if (!delay_check && is_app(t_n) && is_app(s_n)) { + buffer t_args; + buffer s_args; + expr t_fn = get_app_args(t_n, t_args); + expr s_fn = get_app_args(s_n, s_args); + constraint_seq cs_prime = cs; + if (is_def_eq(t_fn, s_fn, c, jst, cs_prime) && t_args.size() == s_args.size()) { + unsigned i = 0; + for (; i < t_args.size(); i++) { + if (!is_def_eq(t_args[i], s_args[i], c, jst, cs_prime)) + break; + } + if (i == t_args.size()) { + return to_bcs(true, cs_prime); + } + } + } + + if (try_eta_expansion(t_n, s_n, c, jst, cs) || + try_eta_expansion(s_n, t_n, c, jst, cs)) + return to_bcs(true, cs); + + if (m_env.prop_proof_irrel()) { + // Proof irrelevance support for Prop (aka Type.{0}) + auto tcs = infer_type(c, t); + auto scs = infer_type(c, s); + expr t_type = tcs.first; + expr s_type = scs.first; + // remark: is_prop returns true only if t_type reducible to Prop. + // If t_type contains metavariables, then reduction can get stuck, and is_prop will return false. + auto pcs = is_prop(t_type, c); + if (pcs.first) { + auto dcs = is_def_eq(t_type, s_type, c, jst); + if (dcs.first) + return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second); + } else { + // If we can't stablish whether t_type is Prop, we try s_type. + pcs = is_prop(s_type, c); + if (pcs.first) { + auto dcs = is_def_eq(t_type, s_type, c, jst); + if (dcs.first) + return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second); + } + // This procedure will miss the case where s_type and t_type cannot be reduced to Prop + // because they contain metavariables. + } + } + + if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c) || delay_check) { + cs = cs + constraint_seq(mk_eq_cnstr(t_n, s_n, jst.get())); + return to_bcs(true, cs); + } + + return to_bcs(false); +} + +pair default_converter::is_prop(expr const & e, type_checker & c) { + auto tcs = infer_type(c, e); + auto wcs = whnf(tcs.first, c); + if (wcs.first == mk_Prop()) + return to_bcs(true, wcs.second + tcs.second); + else + return to_bcs(false); +} + +void initialize_default_converter() { + g_dont_care = new expr(Const("dontcare")); +} + +void finalize_default_converter() { + delete g_dont_care; +} +} diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h new file mode 100644 index 000000000..f9817597d --- /dev/null +++ b/src/kernel/default_converter.h @@ -0,0 +1,74 @@ +/* +Copyright (c) 2014-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 "util/lbool.h" +#include "kernel/justification.h" +#include "kernel/environment.h" +#include "kernel/converter.h" +#include "kernel/expr_maps.h" + +namespace lean { +/** \breif Converter used in the kernel */ +class default_converter : public converter { +protected: + environment m_env; + optional m_module_idx; + bool m_memoize; + extra_opaque_pred m_extra_pred; + expr_struct_map m_whnf_core_cache; + expr_struct_map> m_whnf_cache; + + virtual bool may_reduce_later(expr const & e, type_checker & c); + + constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j); + optional expand_macro(expr const & m, type_checker & c); + optional> norm_ext(expr const & e, type_checker & c); + optional d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs); + expr whnf_core(expr const & e, type_checker & c); + bool is_opaque_core(declaration const & d) const; + expr unfold_name_core(expr e, unsigned w); + expr unfold_names(expr const & e, unsigned w); + optional is_delta(expr const & e); + expr whnf_core(expr e, unsigned w, type_checker & c); + + expr whnf(expr const & e_prime, type_checker & c, constraint_seq & cs); + + pair to_bcs(bool b) { return mk_pair(b, constraint_seq()); } + pair to_bcs(bool b, constraint const & c) { return mk_pair(b, constraint_seq(c)); } + pair to_bcs(bool b, constraint_seq const & cs) { return mk_pair(b, cs); } + + bool is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs); + bool is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs); + bool is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs); + + static pair to_lbcs(lbool l) { return mk_pair(l, constraint_seq()); } + static pair to_lbcs(lbool l, constraint const & c) { return mk_pair(l, constraint_seq(c)); } + static pair to_lbcs(pair const & bcs) { + return mk_pair(to_lbool(bcs.first), bcs.second); + } + + lbool quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs); + bool is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs); + bool is_app_of(expr t, name const & f_name); + bool try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs); + bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs); + + pair is_prop(expr const & e, type_checker & c); + +public: + default_converter(environment const & env, optional mod_idx, bool memoize, + extra_opaque_pred const & pred); + + virtual bool is_opaque(declaration const & d) const; + virtual pair whnf(expr const & e_prime, type_checker & c); + virtual optional get_module_idx() const { return m_module_idx; } + virtual pair is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst); +}; + +void initialize_default_converter(); +void finalize_default_converter(); +} diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp index 728ecfd1d..cbfd9db52 100644 --- a/src/kernel/init_module.cpp +++ b/src/kernel/init_module.cpp @@ -11,12 +11,14 @@ Author: Leonardo de Moura #include "kernel/formatter.h" #include "kernel/level.h" #include "kernel/declaration.h" +#include "kernel/default_converter.h" namespace lean { void initialize_kernel_module() { initialize_level(); initialize_expr(); initialize_declaration(); + initialize_default_converter(); initialize_converter(); initialize_type_checker(); initialize_environment(); @@ -27,6 +29,7 @@ void finalize_kernel_module() { finalize_environment(); finalize_type_checker(); finalize_converter(); + finalize_default_converter(); finalize_declaration(); finalize_expr(); finalize_level();