From ea1bae01436ed009c5c275e411c42be51f1944a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Sep 2014 17:05:13 -0700 Subject: [PATCH] refactor(kernel/converter): replace extra_opaque_set with predicate It gives us more flexibility. --- src/kernel/converter.cpp | 63 +++++++++++++++++++++----------- src/kernel/converter.h | 19 ++++++---- src/kernel/environment.h | 6 ++- src/kernel/type_checker.cpp | 20 +++++++--- src/kernel/type_checker.h | 8 ++-- src/library/kernel_bindings.cpp | 30 ++++++++------- src/library/opaque_hints.cpp | 4 +- src/tests/kernel/environment.cpp | 3 -- 8 files changed, 97 insertions(+), 56 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 5c8b17304..457dd337c 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -23,31 +23,36 @@ 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 an additional set of definition names (m_extra_opaque) that - should be considered opaque. Note that, if \c t type checks when using an extra_opaque set S, then t also type checks - (modulo resource constraints) with the empty set. Again, the purpose of extra_opaque is to mimimize the number + 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 transparent when we are type checking another definition/theorem D' also in M. This rule only applies if - D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field + 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, name_set const & extra_opaque, optional const & mod_idx) { +bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional const & mod_idx) { lean_assert(d.is_definition()); if (d.is_theorem()) return true; // theorems are always opaque - if (extra_opaque.contains(d.get_name())) return true; // extra_opaque set overrides opaque flag + 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; +} + /** \brief Auxiliary method for \c is_delta */ -static optional is_delta_core(environment const & env, expr const & e, name_set const & extra_opaque, +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, extra_opaque, mod_idx)) + if (d->is_definition() && !is_opaque(*d, pred, mod_idx)) return d; } return none_declaration(); @@ -57,15 +62,21 @@ static optional is_delta_core(environment const & env, expr const & \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, name_set const & extra_opaque, optional const & mod_idx) { - return is_delta_core(env, get_app_fn(e), extra_opaque, mod_idx); +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(g_main_module_idx); -optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque) { - return is_delta(env, e, extra_opaque, g_opt_main_module_idx); +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; 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); @@ -95,12 +106,13 @@ struct default_converter : public converter { environment m_env; optional m_module_idx; bool m_memoize; - name_set m_extra_opaque; + extra_opaque_pred m_extra_pred; expr_struct_map m_whnf_core_cache; expr_struct_map> m_whnf_cache; - default_converter(environment const & env, optional mod_idx, bool memoize, name_set const & extra_opaque): - m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) { + default_converter(environment const & env, optional mod_idx, bool memoize, + extra_opaque_pred const & pred): + m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) { } constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { @@ -211,7 +223,7 @@ struct default_converter : public converter { } bool is_opaque(declaration const & d) const { - return ::lean::is_opaque(d, m_extra_opaque, m_module_idx); + return ::lean::is_opaque(d, m_extra_pred, m_module_idx); } /** \brief Expand \c e if it is non-opaque constant with weight >= w */ @@ -252,7 +264,7 @@ struct default_converter : public converter { to be expanded. */ optional is_delta(expr const & e) { - return ::lean::is_delta(m_env, get_app_fn(e), m_extra_opaque, m_module_idx); + return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx); } /** @@ -632,14 +644,21 @@ struct default_converter : public converter { }; std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, - bool memoize, name_set const & extra_opaque) { - return std::unique_ptr(new default_converter(env, mod_idx, memoize, extra_opaque)); + bool memoize, extra_opaque_pred const & pred) { + return std::unique_ptr(new default_converter(env, mod_idx, memoize, pred)); +} +std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, + bool memoize) { + return mk_default_converter(env, mod_idx, memoize, g_always_false); } std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize, - name_set const & extra_opaque) { + extra_opaque_pred const & pred) { if (unfold_opaque_main) - return mk_default_converter(env, optional(0), memoize, extra_opaque); + return mk_default_converter(env, optional(0), memoize, pred); else - return mk_default_converter(env, optional(), memoize, extra_opaque); + return mk_default_converter(env, optional(), memoize, pred); +} +std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize) { + return mk_default_converter(env, unfold_opaque_main, memoize, g_always_false); } } diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 5cbea013a..194d9e2d7 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "kernel/environment.h" namespace lean { @@ -24,13 +25,17 @@ public: }; std::unique_ptr mk_dummy_converter(); -std::unique_ptr mk_default_converter(environment const & env, - optional mod_idx = optional(), - bool memoize = true, name_set const & extra_opaque = name_set()); +std::unique_ptr mk_default_converter(environment const & env, optional mod_idx = optional(), + bool memoize = true); +std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, + bool memoize, extra_opaque_pred const & pred); std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, - bool memoize = true, name_set const & extra_opaque = name_set()); + bool memoize = true); +std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, + bool memoize, extra_opaque_pred const & pred); -bool is_opaque(declaration const & d, name_set const & extra_opaque, optional const & mod_idx); -optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque, optional const & mod_idx); -optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque = name_set()); +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); +optional is_delta(environment const & env, expr const & e); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 8dea9ab08..39678fe1f 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -29,6 +29,9 @@ class type_checker; class environment; class certified_declaration; +typedef std::function extra_opaque_pred; +extra_opaque_pred const & no_extra_opaque(); + /** \brief The header of an environment is created when we create the empty environment. Moreover if environment B is an extension of environment A, then A and B share the same header. @@ -223,7 +226,8 @@ class name_generator; Only the type_checker class can create certified declarations. */ class certified_declaration { - friend certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize); + friend certified_declaration check(environment const & env, declaration const & d, + name_generator const & g, extra_opaque_pred const & extra_opaque); environment_id m_id; declaration m_declaration; certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {} diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 481cc1006..f7f76be9c 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -453,20 +453,22 @@ static void check_duplicated_params(environment const & env, declaration const & } } -certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) { +certified_declaration check(environment const & env, declaration const & d, name_generator const & g, + extra_opaque_pred const & pred) { if (d.is_definition()) check_no_mlocal(env, d.get_name(), d.get_value(), false); check_no_mlocal(env, d.get_name(), d.get_type(), true); check_name(env, d.get_name()); check_duplicated_params(env, d); - type_checker checker1(env, g, mk_default_converter(env, optional(), memoize, extra_opaque)); + bool memoize = true; + type_checker checker1(env, g, mk_default_converter(env, optional(), memoize, pred)); expr sort = checker1.check(d.get_type(), d.get_univ_params()).first; checker1.ensure_sort(sort, d.get_type()); if (d.is_definition()) { optional midx; if (d.is_opaque()) midx = optional(d.get_module_idx()); - type_checker checker2(env, g, mk_default_converter(env, midx, memoize, extra_opaque)); + type_checker checker2(env, g, mk_default_converter(env, midx, memoize, pred)); expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first; if (!checker2.is_def_eq(val_type, d.get_type()).first) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) { @@ -477,7 +479,15 @@ certified_declaration check(environment const & env, declaration const & d, name return certified_declaration(env.get_id(), d); } -certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque, bool memoize) { - return check(env, d, name_generator(g_tmp_prefix), extra_opaque, memoize); +certified_declaration check(environment const & env, declaration const & d, name_generator const & g) { + return check(env, d, g, no_extra_opaque()); +} + +certified_declaration check(environment const & env, declaration const & d, extra_opaque_pred const & pred) { + return check(env, d, name_generator(g_tmp_prefix), pred); +} + +certified_declaration check(environment const & env, declaration const & d) { + return check(env, d, no_extra_opaque()); } } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 2a8e78b08..20e847a35 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -209,9 +209,11 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b \brief Type check the given declaration, and return a certified declaration if it is type correct. Throw an exception if the declaration is type incorrect. */ -certified_declaration check(environment const & env, declaration const & d, - name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true); -certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque = name_set(), bool memoize = true); +certified_declaration check(environment const & env, declaration const & d, name_generator const & g, + extra_opaque_pred const & pred); +certified_declaration check(environment const & env, declaration const & d, name_generator const & g); +certified_declaration check(environment const & env, declaration const & d, extra_opaque_pred const & pred); +certified_declaration check(environment const & env, declaration const & d); /** \brief Create a justification for an application \c e where the expected type must be \c d_type and diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 9a971d009..2b9166e34 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1842,9 +1842,10 @@ static int mk_type_checker(lua_State * L) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); } else { optional mod_idx; bool memoize; name_set extra_opaque; + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque); auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), - mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque), + mk_default_converter(to_environment(L, 1), mod_idx, memoize, pred), memoize); return push_type_checker_ref(L, t); } @@ -1905,28 +1906,29 @@ static const struct luaL_Reg type_checker_ref_m[] = { // type_check procedure static int type_check(lua_State * L) { int nargs = lua_gettop(L); - if (nargs == 2) + if (nargs == 2) { return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2))); - else if (nargs == 3) + } else if (nargs == 3) { return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3))); - else if (nargs == 4) - return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4))); - else - return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), - lua_toboolean(L, 5))); + } else { + name_set extra_opaque = to_name_set(L, 4); + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); + return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), pred)); + } } static int add_declaration(lua_State * L) { int nargs = lua_gettop(L); optional d; - if (nargs == 2) + if (nargs == 2) { d = check(to_environment(L, 1), to_declaration(L, 2)); - else if (nargs == 3) + } else if (nargs == 3) { d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3)); - else if (nargs == 4) - d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4)); - else - d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5)); + } else { + name_set extra_opaque = to_name_set(L, 4); + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); + d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), pred); + } return push_environment(L, module::add(to_environment(L, 1), *d)); } diff --git a/src/library/opaque_hints.cpp b/src/library/opaque_hints.cpp index 6c33f4bf6..de9eef19a 100644 --- a/src/library/opaque_hints.cpp +++ b/src/library/opaque_hints.cpp @@ -56,8 +56,10 @@ bool get_hide_main_opaque(environment const & env) { std::unique_ptr mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque) { auto const & ext = get_extension(env); + name_set extra_opaque = ext.m_extra_opaque; + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); return std::unique_ptr(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module && relax_main_opaque, - true, ext.m_extra_opaque))); + true, pred))); } } diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 24dbe99fb..c06a054f0 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -106,9 +106,6 @@ static void tst2() { lean_assert(checker.is_def_eq(f98(c1, id(Prop, id(Prop, c2))), f97(f97(c1, id(Prop, c2)), f97(c2, c1))).first); name_set s; s.insert(name(base, 96)); - type_checker checker2(env, name_generator("tmp"), mk_default_converter(env, optional(), true, s)); - lean_assert_eq(checker2.whnf(f98(c1, c2)).first, - f96(f96(f97(c1, c2), f97(c2, c1)), f96(f97(c2, c1), f97(c1, c2)))); } class normalizer_extension_tst : public normalizer_extension {