From e78de448aaf3f77c67820f064ab9ff782b33f8bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Apr 2014 14:26:55 -0700 Subject: [PATCH] feat(kernel/type_checker): add is_convertible predicate (and support for proof irrelevance and eta-reduction) Signed-off-by: Leonardo de Moura --- src/kernel/definition.h | 2 + src/kernel/type_checker.cpp | 219 +++++++++++++++++++++++++++++++++++- src/kernel/type_checker.h | 2 +- 3 files changed, 216 insertions(+), 7 deletions(-) diff --git a/src/kernel/definition.h b/src/kernel/definition.h index b04efbcc5..c1800b7b7 100644 --- a/src/kernel/definition.h +++ b/src/kernel/definition.h @@ -50,6 +50,8 @@ public: definition & operator=(definition const & s); definition & operator=(definition && s); + friend bool is_eqp(definition const & d1, definition const & d2) { return d1.m_ptr == d2.m_ptr; } + bool is_definition() const; bool is_axiom() const; bool is_theorem() const; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index e72e2a689..5c7cf6964 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -5,13 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/interrupt.h" +#include "util/lbool.h" +#include "util/flet.h" #include "kernel/type_checker.h" #include "kernel/expr_maps.h" #include "kernel/instantiate.h" #include "kernel/max_sharing.h" namespace lean { - /** \brief Auxiliary functional object used to implement type checker. */ struct type_checker::imp { environment m_env; @@ -22,7 +23,10 @@ struct type_checker::imp { name_set m_extra_opaque; max_sharing_fn m_sharing; expr_map m_cache; - expr_map m_whnf_cache; + expr_map m_whnf_core_cache; + + // temporary flags + bool m_cnstrs_enabled; // true if constraints can be generated imp(environment const & env, name_generator const & g, constraint_handler & h, optional mod_idx, bool memoize, name_set const & extra_opaque): @@ -47,7 +51,7 @@ struct type_checker::imp { return !m_memoize || m_sharing.already_processed(e); } - /** \brief Weak head normal form core procedure. It does not perform delta reduction nor extensions. */ + /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ expr whnf_core(expr const & e) { check_system("whnf"); lean_assert(check_memoized(e)); @@ -63,8 +67,8 @@ struct type_checker::imp { // check cache if (m_memoize) { - auto it = m_whnf_cache.find(e); - if (it != m_whnf_cache.end()) + auto it = m_whnf_core_cache.find(e); + if (it != m_whnf_core_cache.end()) return it->second; } @@ -113,7 +117,7 @@ struct type_checker::imp { }} if (m_memoize) - m_whnf_cache.insert(mk_pair(e, r)); + m_whnf_core_cache.insert(mk_pair(e, r)); return r; } @@ -185,5 +189,208 @@ struct type_checker::imp { return unfold_name_core(e, w); } } + + /** \brief Auxiliary method for \c is_delta */ + optional is_delta_core(expr const & e) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) + if (d->is_definition() && !is_opaque(*d)) + return d; + } + return none_definition(); + } + + /** + \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) { + if (is_app(e)) { + expr const * it = &e; + while (is_app(*it)) { + it = &(app_fn(*it)); + } + return is_delta_core(*it); + } else { + return is_delta_core(e); + } + } + + /** + \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) { + while (true) { + expr new_e = unfold_names(whnf_core(e), w); + if (is_eqp(e, new_e)) + return e; + e = new_e; + } + } + + void add_cnstr(constraint const & c) { + m_chandler.add_cnstr(c); + } + + justification get_curr_justification() { + // TODO(Leo) + return mk_assumption_justification(0); + } + + /** \brief Cheap test for whnf (weak head normal form) just based on the kind of \c e */ + static bool quick_is_whnf(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: + return true; + case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: + return false; + } + lean_unreachable(); // LCOV_EXCL_LINE + } + + bool try_eta(expr const & t, expr const & s) { + lean_assert(is_lambda(t)); + lean_assert(!is_lambda(s)); + // TODO(Leo): + return false; + } + + /** + \brief This is an auxiliary method for is_conv. It handles the "easy cases". + + 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) { + if (t == s) + return l_true; // t and s are structurally equal + if (is_metavar(t) || is_metavar(s)) { + // if t or s is a metavariable, then add constraint + if (!m_cnstrs_enabled) + return l_false; // constraint creation is disabled, so return error + if (def_eq) + add_cnstr(mk_eq_cnstr(t, s, get_curr_justification())); + else + add_cnstr(mk_conv_cnstr(t, s, get_curr_justification())); + return l_true; + } + if (t.kind() == s.kind()) { + switch (t.kind()) { + case expr_kind::Lambda: + // t and s are lambda expression, then then t is convertible to s + // iff + // domain(t) is definitionally equal to domain(s) + // and + // body(t) is definitionally equal to body(s) + return to_lbool(is_def_eq(binder_domain(t), binder_domain(s)) && is_def_eq(binder_body(t), binder_body(s))); + case expr_kind::Pi: + // t and s are Pi expressions, then then t is convertible to s + // iff + // domain(t) is definitionally equal to domain(s) + // and + // body(t) is convertible to body(s) + return to_lbool(is_def_eq(binder_domain(t), binder_domain(s)) && is_conv(binder_body(t), binder_body(s), def_eq)); + 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; + if (!m_cnstrs_enabled) + return l_false; + add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), get_curr_justification())); + if (def_eq) + add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), get_curr_justification())); + return l_true; + 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: case expr_kind::Let: + // We do not handle these cases in this method. + break; + } + } + return l_undef; // This is not an "easy case" + } + + bool is_conv(expr const & t, expr const & s, bool def_eq) { + check_system("is_convertible"); + lbool r = quick_is_conv(t, s, def_eq); + 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); + if (r != l_undef) return r == l_true; + } + + // lazy delta-reduction + whnf (still not using normalizer extensions) + 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)); + } else if (!d_t && d_s) { + s_n = whnf_core(unfold_names(s_n, 0)); + } else if (d_t->get_weight() > d_s->get_weight()) { + t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1)); + } else if (d_t->get_weight() < d_s->get_weight()) { + s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1)); + } 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)) { + // try backtracking trick to avoild delta-reduction + // TODO(Leo) + } + 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); + if (r != l_undef) return r == l_true; + } + + if (m_env.proof_irrel()) { + // Proof irrelevance support + flet disable_cnstrs(m_cnstrs_enabled, false); // disable constraint generation + auto t_type = infer_type(t); + if (t_type && is_proposition(*t_type)) { + auto s_type = infer_type(s); + if (s_type) + return is_def_eq(*t_type, *s_type); + } + } + + if (m_env.eta()) { + lean_assert(!is_lambda(t) || !is_lambda(s)); + // Eta-reduction support + if ((is_lambda(t) && try_eta(t, s)) || + (is_lambda(s) && try_eta(s, t))) + return true; + } + + return false; + } + + /** \brief Return true iff t and s are definitionally equal */ + bool is_def_eq(expr const & t, expr const & s) { + return is_conv(t, s, true); + } + + bool is_proposition(expr const &) { + // TODO(Leo) + return false; + } + + optional infer_type(expr const &) { + // TODO(Leo) + return none_expr(); + } }; } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 118c0ad05..0aa2d6073 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -16,7 +16,7 @@ namespace lean { class constraint_handler { public: virtual ~constraint_handler(); - void add_constr(constraint const & c); + void add_cnstr(constraint const & c); }; /**