michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/module): efficient inductive_reader

Browse source 
Do not check imported inductive declarations when trust level is greater than 0.
This commit is contained in:
Leonardo de Moura 2015-08-15 14:48:49 -07:00
parent e80d9685e5
commit 7bc8673786
6 changed files with 117 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/environment.h
View file

@ -29,6 +29,7 @@ namespace lean {
class type_checker;
class environment;
class certified_declaration;
namespace inductive { class certified_inductive_decl; }
typedef std::function<bool(name const &)> 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.

38
src/kernel/inductive/inductive.cpp
View file

@ -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<inductive_decl>(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<inductive_decl>(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> 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);
}
};

21
src/kernel/inductive/inductive.h
View file

@ -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<data> 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<expr> const & ets, list<data> 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<expr> const & get_elim_types() const { return m_elim_types; }
list<data> 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. */

92
src/library/kernel_serializer.cpp
View file

@ -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<inductive_decl> 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<intro_rule> 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<intro_rule> 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<certified_inductive_decl::comp_rule>(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<certified_inductive_decl::comp_rule>(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<expr>(s, d.get_elim_types());
write_list<certified_inductive_decl::data>(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<name>(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<expr> ets = read_list<expr>(d, read_expr);
auto ds = read_list<certified_inductive_decl::data>(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() {

5
src/library/kernel_serializer.h
View file

@ -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<level_param_names, unsigned, list<inductive::inductive_decl>> 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();

12
src/library/module.cpp
View file

@ -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<inductive::inductive_decl> const & decls) {
environment new_env = inductive::add_inductive(env, level_params, num_params, decls).first;
pair<environment, certified_inductive_decl> 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<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
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);
});
}