feat(kernel/type_checker): expose is_opaque

src/kernel/converter.cpp

@@ -91,6 +91,7 @@ struct dummy_converter : public converter {
         return mk_pair(true, constraint_seq());
     }
     virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
+    virtual bool is_opaque(declaration const &) const { return false; }
 };
 
 std::unique_ptr<converter> 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);
                         }

src/kernel/converter.h

@@ -21,6 +21,7 @@ public:
     virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
     virtual optional<module_idx> get_module_idx() const = 0;
+    virtual bool is_opaque(declaration const & d) const = 0;
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 

src/kernel/type_checker.cpp

@@ -407,6 +407,18 @@ pair<expr, constraint_seq> 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<converter> && conv, bool memoize):
     m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this),
     m_memoize(memoize), m_params(nullptr) {

src/kernel/type_checker.h

@@ -199,6 +199,11 @@ public:
     }
 
     optional<expr> 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> type_checker_ref;