refactor(kernel): remove unnecessary procedures

src/kernel/converter.cpp

@@ -14,41 +14,6 @@ Author: Leonardo de Moura
 #include "kernel/default_converter.h"
 
 namespace lean {
-/**
-   \brief Predicate for deciding whether \c d is an opaque definition or not.
-
-   Here is the basic idea:
-
-   1) Each definition has an opaque flag. This flag cannot be modified after a definition is added to the environment.
-   The opaque flag affects the convertability check. The idea is to minimize the number of delta-reduction steps.
-   We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined.
-   We should view non-opaque definitions as "inline definitions" used in programming languages such as C++.
-
-   2) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as
-   transparent when we are type checking another definition/theorem D' also in M. This rule only applies if
-   D is not a theorem, nor pred(D) is true. To implement this feature, this class has a field
-   m_module_idx that is not none when this rule should be applied.
-*/
-bool is_opaque(declaration const & d, optional<module_idx> const & mod_idx) {
-    lean_assert(d.is_definition());
-    if (d.is_theorem()) return true;                               // theorems are always opaque
-    if (!d.is_opaque()) return false;                              // d is a transparent definition
-    if (mod_idx && d.get_module_idx() == *mod_idx) return false;   // the opaque definitions in mod_idx are considered transparent
-    return true;                                                   // d is opaque
-}
-
-static optional<module_idx> * g_opt_main_module_idx = nullptr;
-
-optional<declaration> is_delta(environment const & env, expr const & e) {
-    expr const & f = get_app_fn(e);
-    if (is_constant(f)) {
-        if (auto d = env.find(const_name(f)))
-            if (d->is_definition() && !is_opaque(*d, *g_opt_main_module_idx))
-                return d;
-    }
-    return none_declaration();
-}
-
 static no_delayed_justification * g_no_delayed_jst = nullptr;
 
 pair<bool, constraint_seq> converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
@@ -72,6 +37,7 @@ struct dummy_converter : public converter {
     }
     virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
     virtual bool is_opaque(declaration const &) const { return false; }
+    virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {
@@ -79,12 +45,10 @@ std::unique_ptr<converter> mk_dummy_converter() {
 }
 
 void initialize_converter() {
-    g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx);
     g_no_delayed_jst      = new no_delayed_justification();
 }
 
 void finalize_converter() {
-    delete g_opt_main_module_idx;
     delete g_no_delayed_jst;
 }
 }

src/kernel/converter.h

@@ -22,15 +22,12 @@ public:
     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;
+    virtual optional<declaration> is_delta(expr const & e) const = 0;
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
 std::unique_ptr<converter> mk_dummy_converter();
 
-/** \brief Default procedure for deciding whether a declaration is opaque or not */
-bool is_opaque(declaration const & d, optional<module_idx> const & mod_idx);
-optional<declaration> is_delta(environment const & env, expr const & e);
-
 void initialize_converter();
 void finalize_converter();
 }

src/kernel/default_converter.cpp

@@ -108,7 +108,11 @@ expr default_converter::whnf_core(expr const & e) {
 }
 
 bool default_converter::is_opaque(declaration const & d) const {
-    return ::lean::is_opaque(d, m_module_idx);
+    lean_assert(d.is_definition());
+    if (d.is_theorem()) return true;                               // theorems are always opaque
+    if (!d.is_opaque()) return false;                              // d is a transparent definition
+    if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
+    return true;                                                   // d is opaque
 }
 
 /** \brief Expand \c e if it is non-opaque constant with weight >= w */
@@ -148,7 +152,7 @@ expr default_converter::unfold_names(expr const & e, unsigned 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<declaration> default_converter::is_delta(expr const & e) {
+optional<declaration> default_converter::is_delta(expr const & e) const {
     expr const & f = get_app_fn(e);
     if (is_constant(f)) {
         if (auto d = m_env.find(const_name(f)))

src/kernel/default_converter.h

@@ -36,7 +36,6 @@ protected:
     expr whnf_core(expr const & e);
     expr unfold_name_core(expr e, unsigned w);
     expr unfold_names(expr const & e, unsigned w);
-    optional<declaration> is_delta(expr const & e);
     expr whnf_core(expr e, unsigned w);
 
     expr whnf(expr const & e_prime, constraint_seq & cs);
@@ -74,6 +73,7 @@ public:
     default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
     default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);
 
+    virtual optional<declaration> is_delta(expr const & e) const;
     virtual bool is_opaque(declaration const & d) const;
     virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
 

src/kernel/type_checker.h

@@ -213,6 +213,8 @@ public:
     /** \brief Return a metavariable that may be stucking the \c e's reduction. */
     optional<expr> is_stuck(expr const & e);
 
+    optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
+
     template<typename F>
     typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
         flet<level_param_names const *> updt(m_params, &ps);

src/library/unifier.cpp

@@ -775,7 +775,10 @@ struct unifier_fn {
         lean_unreachable(); // LCOV_EXCL_LINE
     }
 
-    optional<declaration> is_delta(expr const & e) { return ::lean::is_delta(m_env, e); }
+    optional<declaration> is_delta(expr const & e) {
+        bool relax_opaque = true;
+        return m_tc[relax_opaque]->is_delta(e);
+    }
 
     /** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */
     bool is_eq_deltas(expr const & lhs, expr const & rhs) {