From d4236e40b4fe4f8238329f94441e985708e125ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 11:19:54 -0700 Subject: [PATCH] feat(kernel/type_checker): expose is_opaque --- src/kernel/converter.cpp | 11 ++++++++--- src/kernel/converter.h | 1 + src/kernel/type_checker.cpp | 12 ++++++++++++ src/kernel/type_checker.h | 5 +++++ 4 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index a3bbd90b4..384794326 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -91,6 +91,7 @@ struct dummy_converter : public converter { return mk_pair(true, constraint_seq()); } virtual optional get_module_idx() const { return optional(); } + virtual bool is_opaque(declaration const &) const { return false; } }; std::unique_ptr mk_dummy_converter() { @@ -222,15 +223,19 @@ struct default_converter : public converter { return r; } - bool is_opaque(declaration const & d) const { + 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(*d) && d->get_weight() >= w) + 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); } } @@ -515,7 +520,7 @@ struct default_converter : public converter { // 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(*d_t) && d_t->use_conv_opt() && + 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); } diff --git a/src/kernel/converter.h b/src/kernel/converter.h index c02515f91..4d59a0189 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -21,6 +21,7 @@ public: virtual pair whnf(expr const & e, type_checker & c) = 0; virtual pair is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0; virtual optional get_module_idx() const = 0; + virtual bool is_opaque(declaration const & d) const = 0; pair is_def_eq(expr const & t, expr const & s, type_checker & c); }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 50270c4fc..ccdd2eebb 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -407,6 +407,18 @@ pair type_checker::whnf(expr const & t) { return m_conv->whnf(t, *this); } +bool type_checker::is_opaque(declaration const & d) const { + return m_conv->is_opaque(d); +} + +bool type_checker::is_opaque(expr const & c) const { + lean_assert(is_constant(c)); + if (auto d = m_env.find(const_name(c))) + return is_opaque(*d); + else + return true; +} + type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize): m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this), m_memoize(memoize), m_params(nullptr) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index bc56ac9ee..a07358eac 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -199,6 +199,11 @@ public: } optional expand_macro(expr const & m); + + /** \brief Return true iff \c d is opaque with respect to this type checker. */ + bool is_opaque(declaration const & d) const; + /** \brief Return true iff the constant \c c is opaque with respect to this type checker. */ + bool is_opaque(expr const & c) const; }; typedef std::shared_ptr type_checker_ref;