feat(library/module): add inductive decls to .olean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
49e1f78a33
commit
eca906b074
5 changed files with 44 additions and 14 deletions
|
@ -727,11 +727,6 @@ environment add_inductive(environment env,
|
|||
return add_inductive_fn(env, level_params, num_params, decls)();
|
||||
}
|
||||
|
||||
environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params,
|
||||
unsigned num_params, expr const & type, list<intro_rule> const & intro_rules) {
|
||||
return add_inductive(env, level_params, num_params, list<inductive_decl>(inductive_decl(ind_name, type, intro_rules)));
|
||||
}
|
||||
|
||||
optional<expr> inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const {
|
||||
// Reduce terms \c e of the form
|
||||
// elim_k A C e p[A,b] (intro_k_i A b u)
|
||||
|
|
|
@ -40,13 +40,5 @@ environment add_inductive(environment env,
|
|||
level_param_names const & level_params,
|
||||
unsigned num_params,
|
||||
list<inductive_decl> const & decls);
|
||||
|
||||
/** \brief Declare a single inductive datatype. */
|
||||
environment add_inductive(environment const & env,
|
||||
name const & ind_name, // name of new inductive datatype
|
||||
level_param_names const & level_params, // level parameters
|
||||
unsigned num_params, // number of params
|
||||
expr const & type, // type of the form: params -> indices -> Type
|
||||
list<intro_rule> const & intro_rules); // introduction rules
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1926,7 +1926,7 @@ static int add_inductivek(lua_State * L) {
|
|||
}
|
||||
if (decls.empty())
|
||||
throw exception("invalid add_inductive, at least one inductive type must be defined");
|
||||
return push_environment(L, add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end())));
|
||||
return push_environment(L, ::lean::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end())));
|
||||
}
|
||||
static int add_inductive(lua_State * L) {
|
||||
if (is_name(L, 2) || lua_isstring(L, 2))
|
||||
|
|
|
@ -138,6 +138,34 @@ environment add(environment const & env, declaration const & d) {
|
|||
return add(new_env, g_decl, [=](serializer & s) { s << d; });
|
||||
}
|
||||
|
||||
static std::string g_inductive("ind");
|
||||
|
||||
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);
|
||||
return add(new_env, g_inductive, [=](serializer & s) {
|
||||
s << inductive_decls(level_params, num_params, decls);
|
||||
});
|
||||
}
|
||||
|
||||
environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params,
|
||||
unsigned num_params, expr const & type, list<inductive::intro_rule> const & intro_rules) {
|
||||
return add_inductive(env, level_params, num_params, list<inductive::inductive_decl>(inductive::inductive_decl(ind_name, type, intro_rules)));
|
||||
}
|
||||
|
||||
static void inductive_reader(deserializer & d, module_idx, shared_environment & senv,
|
||||
std::function<void(asynch_update_fn const &)> &,
|
||||
std::function<void(delayed_update_fn const &)> &) {
|
||||
inductive_decls ds = read_inductive_decls(d);
|
||||
senv.update([&](environment const & env) {
|
||||
return inductive::add_inductive(env, std::get<0>(ds), std::get<1>(ds), std::get<2>(ds));
|
||||
});
|
||||
}
|
||||
|
||||
static register_module_object_reader_fn g_reg_ind_reader(g_inductive, inductive_reader);
|
||||
|
||||
struct import_modules_fn {
|
||||
typedef std::tuple<module_idx, unsigned, delayed_update_fn> delayed_update;
|
||||
shared_environment m_senv;
|
||||
|
|
|
@ -8,6 +8,7 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include <iostream>
|
||||
#include "util/serializer.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "library/shared_environment.h"
|
||||
#include "library/io_state.h"
|
||||
|
||||
|
@ -77,4 +78,18 @@ environment add(environment const & env, certified_declaration const & d);
|
|||
This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
|
||||
*/
|
||||
environment add(environment const & env, declaration const & d);
|
||||
|
||||
/** \brief Add the given inductive declaration to the environment, and mark it to be exported. */
|
||||
environment add_inductive(environment env,
|
||||
level_param_names const & level_params,
|
||||
unsigned num_params,
|
||||
list<inductive::inductive_decl> const & decls);
|
||||
|
||||
/** \brief Declare a single inductive datatype. */
|
||||
environment add_inductive(environment const & env,
|
||||
name const & ind_name, // name of new inductive datatype
|
||||
level_param_names const & level_params, // level parameters
|
||||
unsigned num_params, // number of params
|
||||
expr const & type, // type of the form: params -> indices -> Type
|
||||
list<inductive::intro_rule> const & intro_rules); // introduction rules
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue