From 7bc8673786a86d6e4d637ff0a7cd6330202bb929 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Aug 2015 14:48:49 -0700 Subject: [PATCH] feat(library/module): efficient inductive_reader Do not check imported inductive declarations when trust level is greater than 0. --- src/kernel/environment.h | 2 + src/kernel/inductive/inductive.cpp | 38 ++++++++---- src/kernel/inductive/inductive.h | 21 ++++--- src/library/kernel_serializer.cpp | 92 +++++++++++++++++++++--------- src/library/kernel_serializer.h | 5 +- src/library/module.cpp | 12 ++-- 6 files changed, 117 insertions(+), 53 deletions(-) diff --git a/src/kernel/environment.h b/src/kernel/environment.h index a4d0899aa0..af99629106 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -29,6 +29,7 @@ namespace lean { class type_checker; class environment; class certified_declaration; +namespace inductive { class certified_inductive_decl; } typedef std::function extra_opaque_pred; // NOLINT extra_opaque_pred const & no_extra_opaque(); @@ -116,6 +117,7 @@ class environment { environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext); friend class shared_environment; + friend class inductive::certified_inductive_decl; /** \brief Adds a declaration that was not type checked. diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index e0c94e6882..aeb76f757e 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -190,7 +190,14 @@ name get_elim_name(name const & n) { return n + name("rec"); } -environment certified_inductive_decl::add(environment const & env) { +environment certified_inductive_decl::add_constant(environment const & env, name const & n, level_param_names const & ls, expr const & t) const { + if (env.trust_lvl() == 0) + return env.add(check(env, mk_constant_assumption(n, ls, t))); + else + return env.add(mk_constant_assumption(n, ls, t)); +} + +environment certified_inductive_decl::add_core(environment const & env, bool update_ext_only) const { lean_assert(m_data); lean_assert(length(m_data) == length(m_elim_types)); environment new_env = env; @@ -198,23 +205,19 @@ environment certified_inductive_decl::add(environment const & env) { level_param_names levels = m_levels; if (!m_elim_prop) levels = tail(levels); - // declarate inductive types, introduction/elimination rules if they have not been declared yet - bool declare = !new_env.find(inductive_decl_name(head(m_decl_data).m_decl)); - if (declare && env.trust_lvl() == 0) - throw_kernel_exception(env, "environment trust level does not allow users to add inductive declarations that were not type checked"); // declare inductive types for (data const & dt : m_decl_data) { inductive_decl const & d = dt.m_decl; - if (declare) - new_env = new_env.add(check(new_env, mk_constant_assumption(inductive_decl_name(d), levels, inductive_decl_type(d)))); + if (!update_ext_only) + new_env = add_constant(new_env, inductive_decl_name(d), levels, inductive_decl_type(d)); ext.add_inductive_info(levels, m_num_params, map2(m_decl_data, [](data const & d) { return d.m_decl; })); } // declare introduction rules for (data const & dt : m_decl_data) { inductive_decl const & d = dt.m_decl; for (auto ir : inductive_decl_intros(d)) { - if (declare) - new_env = new_env.add(check(new_env, mk_constant_assumption(intro_rule_name(ir), levels, intro_rule_type(ir)))); + if (!update_ext_only) + new_env = add_constant(new_env, intro_rule_name(ir), levels, intro_rule_type(ir)); ext.add_intro_info(intro_rule_name(ir), inductive_decl_name(d)); } } @@ -223,8 +226,8 @@ environment certified_inductive_decl::add(environment const & env) { for (data const & dt : m_decl_data) { inductive_decl const & d = dt.m_decl; name elim_name = get_elim_name(inductive_decl_name(d)); - if (declare) - new_env = new_env.add(check(new_env, mk_constant_assumption(elim_name, m_levels, head(types)))); + if (!update_ext_only) + new_env = add_constant(new_env, elim_name, m_levels, head(types)); ext.add_elim(elim_name, inductive_decl_name(d), m_levels, m_num_params, m_num_ACe, dt.m_num_indices, dt.m_K_target, m_dep_elim); lean_assert(length(inductive_decl_intros(d)) == length(dt.m_comp_rules)); @@ -239,6 +242,17 @@ environment certified_inductive_decl::add(environment const & env) { return update(new_env, ext); } +environment certified_inductive_decl::add(environment const & env) const { + if (env.trust_lvl() == 0) { + level_param_names levels = m_levels; + if (!m_elim_prop) + levels = tail(levels); + return add_inductive(env, levels, m_num_params, map2(m_decl_data, [](data const & d) { return d.m_decl; })).first; + } else { + return add_core(env, false); + } +} + /** \brief Helper functional object for processing inductive datatype declarations. */ struct add_inductive_fn { typedef std::unique_ptr type_checker_ptr; @@ -853,7 +867,7 @@ struct add_inductive_fn { check_intro_rules(); declare_intro_rules(); certified_inductive_decl c = mk_certified_decl(declare_elim_rules()); - m_env = c.add(m_env); + m_env = c.add_core(m_env, true); return mk_pair(m_env, c); } }; diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 0aa62094ce..8cbf9f65d2 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { +class read_certified_inductive_decl_fn; namespace inductive { /** \brief Normalizer extension for applying inductive datatype computational rules. */ class inductive_normalizer_extension : public normalizer_extension { @@ -70,24 +71,28 @@ private: list m_decl_data; friend struct add_inductive_fn; + friend class ::lean::read_certified_inductive_decl_fn; + + environment add_core(environment const & env, bool update_ext_only) const; + environment add_constant(environment const & env, name const & n, level_param_names const & ls, expr const & t) const; certified_inductive_decl(level_param_names const & ps, unsigned num_params, unsigned num_ACe, bool elim_prop, bool dep_delim, list const & ets, list const & d): m_levels(ps), m_num_params(num_params), m_num_ACe(num_ACe), m_elim_prop(elim_prop), m_dep_elim(dep_delim), m_elim_types(ets), m_decl_data(d) {} - - /** \brief Update the environment with this "certified declaration" - \remark This method throws an exception if trust level is 0. - \remark This method is used to import modules efficiently. - */ - environment add(environment const & env); - public: - level_param_names const & get_univ_param() const { return m_levels; } + level_param_names const & get_univ_params() const { return m_levels; } unsigned get_num_params() const { return m_num_params; } unsigned get_num_ACe() const { return m_num_ACe; } + bool elim_prop_only() const { return m_elim_prop; } bool has_dep_elim() const { return m_dep_elim; } + list const & get_elim_types() const { return m_elim_types; } list const & get_decl_data() const { return m_decl_data; } + + /** \brief Update the environment with this "certified declaration" + \remark If trust_level is 0, then declaration is rechecked. + */ + environment add(environment const & env) const; }; /** \brief Declare a finite set of mutually dependent inductive datatypes. */ diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index b95d69ad45..c64e0386ee 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -317,6 +317,7 @@ declaration read_declaration(deserializer & d) { } } +using inductive::certified_inductive_decl; using inductive::inductive_decl; using inductive::intro_rule; using inductive::inductive_decl_name; @@ -325,36 +326,75 @@ using inductive::inductive_decl_intros; using inductive::intro_rule_name; using inductive::intro_rule_type; -serializer & operator<<(serializer & s, inductive_decls const & ds) { - s << std::get<0>(ds) << std::get<1>(ds); - auto const & ls = std::get<2>(ds); - s << length(ls); - for (inductive_decl const & d : ls) { - s << inductive_decl_name(d) << inductive_decl_type(d) << length(inductive_decl_intros(d)); - for (intro_rule const & r : inductive_decl_intros(d)) - s << intro_rule_name(r) << intro_rule_type(r); - } +serializer & operator<<(serializer & s, certified_inductive_decl::comp_rule const & r) { + s << r.m_num_bu << r.m_comp_rhs; return s; } -inductive_decls read_inductive_decls(deserializer & d) { - level_param_names ps = read_level_params(d); - unsigned num_params, num_decls; - d >> num_params >> num_decls; - buffer decls; - for (unsigned i = 0; i < num_decls; i++) { - name d_name = read_name(d); - expr d_type = read_expr(d); - unsigned num_intros = d.read_unsigned(); - buffer rules; - for (unsigned j = 0; j < num_intros; j++) { - name r_name = read_name(d); - expr r_type = read_expr(d); - rules.push_back(intro_rule(r_name, r_type)); - } - decls.push_back(inductive_decl(d_name, d_type, to_list(rules.begin(), rules.end()))); +certified_inductive_decl::comp_rule read_comp_rule(deserializer & d) { + unsigned n; expr e; + d >> n >> e; + return certified_inductive_decl::comp_rule(n, e); +} + +serializer & operator<<(serializer & s, inductive_decl const & d) { + s << inductive_decl_name(d) << inductive_decl_type(d) << length(inductive_decl_intros(d)); + for (intro_rule const & r : inductive_decl_intros(d)) + s << intro_rule_name(r) << intro_rule_type(r); + return s; +} + +inductive_decl read_inductive_decl(deserializer & d) { + name d_name = read_name(d); + expr d_type = read_expr(d); + unsigned num_intros = d.read_unsigned(); + buffer rules; + for (unsigned j = 0; j < num_intros; j++) { + name r_name = read_name(d); + expr r_type = read_expr(d); + rules.push_back(intro_rule(r_name, r_type)); } - return inductive_decls(ps, num_params, to_list(decls.begin(), decls.end())); + return inductive_decl(d_name, d_type, to_list(rules.begin(), rules.end())); +} + +serializer & operator<<(serializer & s, certified_inductive_decl::data const & d) { + s << d.m_decl << d.m_K_target << d.m_num_indices; + write_list(s, d.m_comp_rules); + return s; +} + +certified_inductive_decl::data read_certified_inductive_decl_data(deserializer & d) { + inductive_decl decl = read_inductive_decl(d); + bool K = d.read_bool(); + unsigned nind = d.read_unsigned(); + auto rs = read_list(d, read_comp_rule); + return certified_inductive_decl::data(decl, K, nind, rs); +} + +serializer & operator<<(serializer & s, certified_inductive_decl const & d) { + s << d.get_univ_params() << d.get_num_params() << d.get_num_ACe() + << d.elim_prop_only() << d.has_dep_elim(); + write_list(s, d.get_elim_types()); + write_list(s, d.get_decl_data()); + return s; +} + +class read_certified_inductive_decl_fn { +public: + certified_inductive_decl operator()(deserializer & d) { + level_param_names ls = read_list(d, read_name); + unsigned nparams = d.read_unsigned(); + unsigned nACe = d.read_unsigned(); + bool elim_prop = d.read_bool(); + bool dep_elim = d.read_bool(); + list ets = read_list(d, read_expr); + auto ds = read_list(d, read_certified_inductive_decl_data); + return certified_inductive_decl(ls, nparams, nACe, elim_prop, dep_elim, ets, ds); + } +}; + +certified_inductive_decl read_certified_inductive_decl(deserializer & d) { + return read_certified_inductive_decl_fn()(d); } void initialize_kernel_serializer() { diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h index 9111016cd4..ebe4462d95 100644 --- a/src/library/kernel_serializer.h +++ b/src/library/kernel_serializer.h @@ -29,9 +29,8 @@ inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); serializer & operator<<(serializer & s, declaration const & d); declaration read_declaration(deserializer & d); -typedef std::tuple> inductive_decls; -serializer & operator<<(serializer & s, inductive_decls const & ds); -inductive_decls read_inductive_decls(deserializer & d); +serializer & operator<<(serializer & s, inductive::certified_inductive_decl const & d); +inductive::certified_inductive_decl read_certified_inductive_decl(deserializer & d); void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd); void initialize_kernel_serializer(); diff --git a/src/library/module.cpp b/src/library/module.cpp index 5d5a269a94..93769e280e 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -256,25 +256,29 @@ static void hits_reader(deserializer &, shared_environment & senv, }); } +using inductive::certified_inductive_decl; + environment add_inductive(environment env, level_param_names const & level_params, unsigned num_params, list const & decls) { - environment new_env = inductive::add_inductive(env, level_params, num_params, decls).first; + pair r = inductive::add_inductive(env, level_params, num_params, decls); + environment new_env = r.first; + certified_inductive_decl cdecl = r.second; module_ext ext = get_extension(env); ext.m_module_decls = cons(inductive::inductive_decl_name(head(decls)), ext.m_module_decls); new_env = update(new_env, ext); return add(new_env, *g_inductive, [=](environment const &, serializer & s) { - s << inductive_decls(level_params, num_params, decls); + s << cdecl; }); } static void inductive_reader(deserializer & d, shared_environment & senv, std::function &, std::function &) { - inductive_decls ds = read_inductive_decls(d); + certified_inductive_decl cdecl = read_certified_inductive_decl(d); senv.update([&](environment const & env) { - return inductive::add_inductive(env, std::get<0>(ds), std::get<1>(ds), std::get<2>(ds)).first; + return cdecl.add(env); }); }