diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index ee0366ac6..ece3ee913 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -24,65 +24,44 @@ namespace lean { 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) Whenever type checking an expression, the user can provide a predicate that is true for for additional definitions that - should be considered opaque. Note that, if \c t type checks when using predicate P, then t also type checks - (modulo resource constraints) without it. Again, the purpose of the predicate is to mimimize the number - of delta-reduction steps. - - 3) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as + 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, extra_opaque_pred const & pred, optional const & mod_idx) { +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 (pred(d.get_name())) return true; // extra_opaque predicate overrides opaque flag 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 } -extra_opaque_pred g_always_false([](name const &) { return false; }); -extra_opaque_pred const & no_extra_opaque() { - return g_always_false; -} +static optional * g_opt_main_module_idx = nullptr; -/** \brief Auxiliary method for \c is_delta */ -static optional is_delta_core(environment const & env, expr const & e, extra_opaque_pred const & pred, - optional const & mod_idx) { - if (is_constant(e)) { - if (auto d = env.find(const_name(e))) - if (d->is_definition() && !is_opaque(*d, pred, mod_idx)) +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(); } -/** - \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 is_delta(environment const & env, expr const & e, - extra_opaque_pred const & pred, optional const & mod_idx) { - return is_delta_core(env, get_app_fn(e), pred, mod_idx); -} - -static optional * g_opt_main_module_idx = nullptr; -optional is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred) { - return is_delta(env, e, pred, *g_opt_main_module_idx); -} - -optional is_delta(environment const & env, expr const & e) { - return is_delta(env, e, g_always_false); -} - - static no_delayed_justification * g_no_delayed_jst = nullptr; + pair converter::is_def_eq(expr const & t, expr const & s, type_checker & c) { return is_def_eq(t, s, c, *g_no_delayed_jst); } +name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); } + +pair converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); } + +extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); } + + /** \brief Do nothing converter */ struct dummy_converter : public converter { virtual pair whnf(expr const & e, type_checker &) { @@ -99,10 +78,6 @@ std::unique_ptr mk_dummy_converter() { return std::unique_ptr(new dummy_converter()); } -name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); } -pair converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); } -extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); } - void initialize_converter() { g_opt_main_module_idx = new optional(g_main_module_idx); g_no_delayed_jst = new no_delayed_justification(); diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 39fbdadfb..a69247ae6 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -27,9 +27,8 @@ public: std::unique_ptr mk_dummy_converter(); -bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional const & mod_idx); -optional is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred, optional const & mod_idx); -optional is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred); +/** \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(); diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index b3b8efd1f..3b0e4b314 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -108,11 +108,7 @@ expr default_converter::whnf_core(expr const & e) { } bool default_converter::is_opaque(declaration const & d) const { - 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 + return ::lean::is_opaque(d, m_module_idx); } /** \brief Expand \c e if it is non-opaque constant with weight >= w */