diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index ece3ee913..529bfa6db 100644 --- a/src/kernel/converter.cpp +++ b/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 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 * g_opt_main_module_idx = nullptr; - -optional 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 converter::is_def_eq(expr const & t, expr const & s, type_checker & c) { @@ -72,6 +37,7 @@ struct dummy_converter : public converter { } virtual optional get_module_idx() const { return optional(); } virtual bool is_opaque(declaration const &) const { return false; } + virtual optional is_delta(expr const &) const { return optional(); } }; std::unique_ptr mk_dummy_converter() { @@ -79,12 +45,10 @@ std::unique_ptr mk_dummy_converter() { } void initialize_converter() { - g_opt_main_module_idx = new optional(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; } } diff --git a/src/kernel/converter.h b/src/kernel/converter.h index a69247ae6..ea7c82207 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -22,15 +22,12 @@ public: 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; + virtual optional is_delta(expr const & e) const = 0; pair is_def_eq(expr const & t, expr const & s, type_checker & c); }; std::unique_ptr mk_dummy_converter(); -/** \brief Default procedure for deciding whether a declaration is opaque or not */ -bool is_opaque(declaration const & d, optional const & mod_idx); -optional is_delta(environment const & env, expr const & e); - void initialize_converter(); void finalize_converter(); } diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 3b0e4b314..d1594887a 100644 --- a/src/kernel/default_converter.cpp +++ b/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 default_converter::is_delta(expr const & e) { +optional 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))) diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h index eb7547a08..1dacd6ea0 100644 --- a/src/kernel/default_converter.h +++ b/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 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 mod_idx, bool memoize = true); default_converter(environment const & env, bool relax_main_opaque, bool memoize = true); + virtual optional is_delta(expr const & e) const; virtual bool is_opaque(declaration const & d) const; virtual optional get_module_idx() const { return m_module_idx; } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 531af9795..f5c40d1a8 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -213,6 +213,8 @@ public: /** \brief Return a metavariable that may be stucking the \c e's reduction. */ optional is_stuck(expr const & e); + optional is_delta(expr const & e) const { return m_conv->is_delta(e); } + template typename std::result_of::type with_params(level_param_names const & ps, F && f) { flet updt(m_params, &ps); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 1a933dc84..054ab2dd4 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -775,7 +775,10 @@ struct unifier_fn { lean_unreachable(); // LCOV_EXCL_LINE } - optional is_delta(expr const & e) { return ::lean::is_delta(m_env, e); } + optional 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) {