From 7176181b42a062bae075d8328249f256b81ebbff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 May 2014 20:43:11 -0700 Subject: [PATCH] refactor(kernel/converter): cleanup and remove universe cumulativity support Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 75 +++++++++++-------------------------- src/kernel/converter.h | 10 ----- src/kernel/type_checker.cpp | 14 +------ 3 files changed, 23 insertions(+), 76 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index de30824b7..34e63881e 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -12,11 +12,6 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" namespace lean { -bool converter::is_conv(expr const & t, expr const & s, context & c) { - delayed_justification j([]() { return justification(); }); - return is_conv(t, s, c, j); -} - bool converter::is_def_eq(expr const & t, expr const & s, context & c) { delayed_justification j([]() { return justification(); }); return is_def_eq(t, s, c, j); @@ -25,7 +20,6 @@ bool converter::is_def_eq(expr const & t, expr const & s, context & c) { /** \brief Do nothing converter */ struct dummy_converter : public converter { virtual expr whnf(expr const & e, context &) { return e; } - virtual bool is_conv(expr const &, expr const &, context &, delayed_justification &) { return true; } virtual bool is_def_eq(expr const &, expr const &, context &, delayed_justification &) { return true; } }; @@ -282,25 +276,15 @@ struct default_converter : public converter { } /** - \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is convertible to \c s. + \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s. - The argument \c def_eq is used to decide whether the body of the binder is checked for - definitional equality or convertability. - - If t and s are lambda expressions, then then t is convertible to 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) - - For Pi expressions, it is slighly different. - If 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) */ - bool is_conv_binder(expr t, expr s, bool def_eq, context & c, delayed_justification & jst) { + bool is_def_eq_binder(expr t, expr s, context & c, delayed_justification & jst) { lean_assert(t.kind() == s.kind()); lean_assert(is_binder(t)); expr_kind k = t.kind(); @@ -314,15 +298,11 @@ struct default_converter : public converter { 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, c, jst); + return is_def_eq(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), c, jst); } - /** - \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, context & c, delayed_justification & jst) { + /** \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, context & c, delayed_justification & jst) { if (t == s) return l_true; // t and s are structurally equal if (is_meta(t) || is_meta(s)) { @@ -332,17 +312,13 @@ struct default_converter : public converter { } if (t.kind() == s.kind()) { switch (t.kind()) { - case expr_kind::Lambda: - return to_lbool(is_conv_binder(t, s, true, c, jst)); - case expr_kind::Pi: - return to_lbool(is_conv_binder(t, s, def_eq, c, jst)); + case expr_kind::Lambda: case expr_kind::Pi: + return to_lbool(is_def_eq_binder(t, s, c, 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)))) + if (is_trivial(sort_level(t), sort_level(s))) return l_true; c.add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get())); - if (def_eq) - c.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 @@ -357,11 +333,9 @@ struct default_converter : public converter { /** \brief Return true if arguments of \c t are definitionally equal to arguments of \c s. - Constraint generation is disabled when performing this test. - This method is used to implement an optimization in the method \c is_conv. + This method is used to implement an optimization in the method \c is_def_eq. */ bool is_def_eq_args(expr t, expr s, context & c, delayed_justification & jst) { - context::disable_cnstrs_scope scope(c); try { while (is_app(t) && is_app(s)) { if (!is_def_eq(app_arg(t), app_arg(s), c, jst)) @@ -375,20 +349,17 @@ struct default_converter : public converter { } } - /** - \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, context & c, delayed_justification & jst) { - check_system("is_convertible"); - lbool r = quick_is_conv(t, s, def_eq, c, jst); + /** Return true iff t is definitionally equal to s. */ + virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & jst) { + check_system("is_definitionally_equal"); + lbool r = quick_is_def_eq(t, s, c, jst); if (r != l_undef) return r == l_true; // 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_conv(t_n, s_n, def_eq, c, jst); + r = quick_is_def_eq(t_n, s_n, c, jst); if (r != l_undef) return r == l_true; } @@ -414,8 +385,12 @@ struct default_converter : public converter { // then 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. + // We only apply the optimization if t_n and s_n do not contain metavariables. + // In this way we don't have to backtrack constraints if the optimization fail. if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s) && // same definition + !has_metavar(t_n) && + !has_metavar(s_n) && !is_opaque(*d_t) && // if d_t is opaque, we don't need to try this optimization d_t->use_conv_opt() && // the flag use_conv_opt() can be used to disable this optimization is_def_eq_args(t_n, s_n, c, jst)) { @@ -424,7 +399,7 @@ struct default_converter : public converter { 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_conv(t_n, s_n, def_eq, c, jst); + r = quick_is_def_eq(t_n, s_n, c, jst); if (r != l_undef) return r == l_true; } // try normalizer extensions @@ -436,7 +411,7 @@ struct default_converter : public converter { t_n = whnf_core(*new_t_n, c); if (new_s_n) s_n = whnf_core(*new_s_n, c); - r = quick_is_conv(t_n, s_n, def_eq, c, jst); + r = quick_is_def_eq(t_n, s_n, c, jst); if (r != l_undef) return r == l_true; } @@ -478,14 +453,6 @@ struct default_converter : public converter { bool is_prop(expr const & e, context & c) { return whnf(c.infer_type(e), c) == Bool; } - - virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & j) { - return is_conv(t, s, true, c, j); - } - - virtual bool is_conv(expr const & t, expr const & s, context & c, delayed_justification & j) { - return is_conv(t, s, false, c, j); - } }; std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 2f0e87525..d8ae68047 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -24,26 +24,16 @@ class converter { public: /** \brief Abstract context that must be provided to a converter object. */ class context { - virtual bool enable_cnstrs(bool flag) = 0; public: virtual name mk_fresh_name() = 0; virtual expr infer_type(expr const & e) = 0; virtual void add_cnstr(constraint const & c) = 0; - class disable_cnstrs_scope { - context & m_ctx; - bool m_old; - public: - disable_cnstrs_scope(context & ctx):m_ctx(ctx), m_old(m_ctx.enable_cnstrs(false)) {} - ~disable_cnstrs_scope() { m_ctx.enable_cnstrs(m_old); } - }; }; virtual ~converter() {} virtual expr whnf(expr const & e, context & c) = 0; - virtual bool is_conv(expr const & t, expr const & s, context & c, delayed_justification & j) = 0; virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & j) = 0; - bool is_conv(expr const & t, expr const & s, context & c); bool is_def_eq(expr const & t, expr const & s, context & c); }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 715ff3be0..2491a5a63 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -36,12 +36,6 @@ struct type_checker::imp { /** \brief Interface type_checker <-> converter */ class converter_context : public converter::context { imp & m_imp; - virtual bool enable_cnstrs(bool flag) { - bool r = m_imp.m_cnstrs_enabled; - m_imp.m_cnstrs_enabled = flag; - return r; - } - public: converter_context(imp & i):m_imp(i) {} virtual name mk_fresh_name() { return m_imp.m_gen.next(); } @@ -74,12 +68,11 @@ struct type_checker::imp { expr_map m_trace; bool m_memoize; // temp flag - bool m_cnstrs_enabled; param_names m_params; imp(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, bool memoize): m_env(env), m_gen(g), m_chandler(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this), - m_memoize(memoize), m_cnstrs_enabled(true) {} + m_memoize(memoize) {} optional expand_macro(expr const & m) { lean_assert(is_macro(m)); @@ -122,10 +115,7 @@ struct type_checker::imp { /** \brief Add given constraint to the constraint handler m_chandler. */ void add_cnstr(constraint const & c) { - if (m_cnstrs_enabled) - m_chandler.add_cnstr(c); - else - throw add_cnstr_exception(); + m_chandler.add_cnstr(c); } /** \brief Return true iff \c t and \c s are definitionally equal */