max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/module): intermediary data structure for environment modifications

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-19 13:39:26 -05:00 • committed by Leonardo de Moura
parent 23be9bc0c2
commit a26e2c9108
29 changed files with 769 additions and 593 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/module.cpp
View file

@ -31,8 +31,9 @@ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, le
lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex) {
LEAN_TRY;
check_nonnull(env);
auto lm = export_module(to_env_ref(env), fname);
std::ofstream out(fname, std::ofstream::binary);
export_module(out, to_env_ref(env));
write_module(lm, out);
LEAN_CATCH;
}

36
src/frontends/lean/builtin_cmds.cpp
View file

@ -485,18 +485,31 @@ static environment vm_eval_cmd(parser & p) {
return p.env();
}
static std::string * g_declare_trace_key = nullptr;
struct declare_trace_modification : public modification {
LEAN_MODIFICATION("decl_trace")
name m_cls;
declare_trace_modification(name const & cls) : m_cls(cls) {}
declare_trace_modification() {}
void perform(environment &) const override {
// TODO(gabriel): this is just fundamentally wrong
register_trace_class(m_cls);
}
void serialize(serializer & s) const override {
s << m_cls;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<declare_trace_modification>(read_name(d));
}
};
environment declare_trace_cmd(parser & p) {
name cls = p.check_id_next("invalid declare_trace command, identifier expected");
register_trace_class(cls);
return module::add(p.env(), *g_declare_trace_key, [=](environment const &, serializer & s) { s << cls; });
}
static void declare_trace_reader(deserializer & d, environment &) {
name cls;
d >> cls;
register_trace_class(cls);
return module::add_and_perform(p.env(), std::make_shared<declare_trace_modification>(cls));
}
environment add_key_equivalence_cmd(parser & p) {
@ -558,12 +571,11 @@ cmd_table get_builtin_cmds() {
void initialize_builtin_cmds() {
g_cmds = new cmd_table();
init_cmd_table(*g_cmds);
g_declare_trace_key = new std::string("decl_trace");
register_module_object_reader(*g_declare_trace_key, declare_trace_reader);
declare_trace_modification::init();
}
void finalize_builtin_cmds() {
declare_trace_modification::finalize();
delete g_cmds;
delete g_declare_trace_key;
}
}

16
src/frontends/lean/parser_config.cpp
View file

@ -80,7 +80,6 @@ struct token_config {
typedef token_state state;
typedef token_entry entry;
static name * g_class_name;
static std::string * g_key;
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
@ -88,9 +87,7 @@ struct token_config {
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "TK"; }
static void write_entry(serializer & s, entry const & e) {
s << e.m_token.c_str() << e.m_prec;
}
@ -104,7 +101,6 @@ struct token_config {
}
};
name * token_config::g_class_name = nullptr;
std::string * token_config::g_key = nullptr;
template class scoped_ext<token_config>;
typedef scoped_ext<token_config> token_ext;
@ -239,7 +235,6 @@ struct notation_config {
typedef notation_state state;
typedef notation_entry entry;
static name * g_class_name;
static std::string * g_key;
static void updt_inv_map(state & s, head_index const & idx, entry const & e) {
if (!e.parse_only())
@ -281,9 +276,7 @@ struct notation_config {
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static char const * get_serialization_key() { return "NOTA"; }
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.kind()) << e.overload() << e.parse_only() << e.get_expr();
if (e.is_numeral()) {
@ -321,7 +314,6 @@ struct notation_config {
}
};
name * notation_config::g_class_name = nullptr;
std::string * notation_config::g_key = nullptr;
template class scoped_ext<notation_config>;
typedef scoped_ext<notation_config> notation_ext;
@ -386,20 +378,16 @@ cmd_table const & get_cmd_table(environment const & env) {
void initialize_parser_config() {
token_config::g_class_name = new name("notation");
token_config::g_key = new std::string("TK");
token_ext::initialize();
notation_config::g_class_name = new name("notation");
notation_config::g_key = new std::string("NOTA");
notation_ext::initialize();
g_ext = new cmd_ext_reg();
}
void finalize_parser_config() {
delete g_ext;
notation_ext::finalize();
delete notation_config::g_key;
delete notation_config::g_class_name;
token_ext::finalize();
delete token_config::g_key;
delete token_config::g_class_name;
}
}

1
src/frontends/lean/parser_config.h
View file

@ -16,6 +16,7 @@ struct token_entry {
std::string m_token;
unsigned m_prec;
token_entry(std::string const & tk, unsigned prec): m_token(tk), m_prec(prec) {}
token_entry() : m_prec(0) {}
};
inline token_entry mk_token_entry(std::string const & tk, unsigned prec) { return token_entry(tk, prec); }

8
src/library/attribute_manager.cpp
View file

@ -32,8 +32,6 @@ void set_user_attribute_ext(std::unique_ptr<user_attribute_ext> ext) {
static std::vector<pair<name, name>> * g_incomp = nullptr;
static std::string * g_key = nullptr;
bool is_system_attribute(name const & attr) {
return g_system_attributes->contains(attr);
}
@ -122,9 +120,7 @@ struct attr_config {
s.insert(e.m_attr, mk_pair(m, h));
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "ATTR"; }
static void write_entry(serializer & s, entry const & e) {
s << e.m_attr << e.m_prio << e.m_record.m_decl << e.m_record.deleted();
@ -276,13 +272,11 @@ void initialize_attribute_manager() {
g_system_attributes = new name_map<attribute_ptr>();
g_user_attribute_ext = new user_attribute_ext();
g_incomp = new std::vector<pair<name, name>>();
g_key = new std::string("ATTR");
attribute_ext::initialize();
}
void finalize_attribute_manager() {
attribute_ext::finalize();
delete g_key;
delete g_incomp;
delete g_user_attribute_ext;
delete g_system_attributes;

83
src/library/aux_recursors.cpp
View file

@ -29,21 +29,58 @@ static environment update(environment const & env, aux_recursor_ext const & ext)
return env.update(g_ext->m_ext_id, std::make_shared<aux_recursor_ext>(ext));
}
static std::string * g_auxrec_key = nullptr;
static std::string * g_no_confusion_key = nullptr;
struct auxrec_modification : public modification {
LEAN_MODIFICATION("auxrec")
name m_decl;
auxrec_modification() {}
auxrec_modification(name const & decl) : m_decl(decl) {}
void perform(environment & env) const override {
aux_recursor_ext ext = get_extension(env);
ext.m_aux_recursor_set.insert(m_decl);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_decl;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<auxrec_modification>(read_name(d));
}
};
struct no_conf_modification : public modification {
LEAN_MODIFICATION("no_conf")
name m_decl;
no_conf_modification() {}
no_conf_modification(name const & decl) : m_decl(decl) {}
void perform(environment & env) const override {
aux_recursor_ext ext = get_extension(env);
ext.m_no_confusion_set.insert(m_decl);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_decl;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<no_conf_modification>(read_name(d));
}
};
environment add_aux_recursor(environment const & env, name const & r) {
aux_recursor_ext ext = get_extension(env);
ext.m_aux_recursor_set.insert(r);
environment new_env = update(env, ext);
return module::add(new_env, *g_auxrec_key, [=](environment const &, serializer & s) { s << r; });
return module::add_and_perform(env, std::make_shared<auxrec_modification>(r));
}
environment add_no_confusion(environment const & env, name const & r) {
aux_recursor_ext ext = get_extension(env);
ext.m_no_confusion_set.insert(r);
environment new_env = update(env, ext);
return module::add(new_env, *g_no_confusion_key, [=](environment const &, serializer & s) { s << r; });
return module::add_and_perform(env, std::make_shared<no_conf_modification>(r));
}
bool is_aux_recursor(environment const & env, name const & r) {
@ -54,33 +91,15 @@ bool is_no_confusion(environment const & env, name const & r) {
return get_extension(env).m_no_confusion_set.contains(r);
}
static void aux_recursor_reader(deserializer & d, environment & env) {
name r;
d >> r;
aux_recursor_ext ext = get_extension(env);
ext.m_aux_recursor_set.insert(r);
env = update(env, ext);
}
static void no_confusion_reader(deserializer & d, environment & env) {
name r;
d >> r;
aux_recursor_ext ext = get_extension(env);
ext.m_no_confusion_set.insert(r);
env = update(env, ext);
}
void initialize_aux_recursors() {
g_ext = new aux_recursor_ext_reg();
g_auxrec_key = new std::string("auxrec");
g_no_confusion_key = new std::string("no_conf");
register_module_object_reader(*g_auxrec_key, aux_recursor_reader);
register_module_object_reader(*g_no_confusion_key, no_confusion_reader);
auxrec_modification::init();
no_conf_modification::init();
}
void finalize_aux_recursors() {
delete g_auxrec_key;
delete g_no_confusion_key;
auxrec_modification::finalize();
no_conf_modification::finalize();
delete g_ext;
}
}

7
src/library/class.cpp
View file

@ -76,7 +76,6 @@ struct class_state {
};
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
struct class_config {
typedef class_state state;
@ -94,9 +93,7 @@ struct class_config {
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "class"; }
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.m_kind);
switch (e.m_kind) {
@ -246,7 +243,6 @@ void initialize_class() {
g_class_attr_name = new name("class");
g_instance_attr_name = new name("instance");
g_class_name = new name("class");
g_key = new std::string("class");
class_ext::initialize();
register_system_attribute(basic_attribute(*g_class_attr_name, "type class",
@ -264,7 +260,6 @@ void initialize_class() {
void finalize_class() {
class_ext::finalize();
delete g_key;
delete g_class_name;
delete g_class_attr_name;
delete g_instance_attr_name;

45
src/library/documentation.cpp
View file

@ -32,8 +32,31 @@ static environment update(environment const & env, documentation_ext const & ext
return env.update(g_ext->m_ext_id, std::make_shared<documentation_ext>(ext));
}
static name * g_documentation = nullptr;
static std::string * g_doc_key = nullptr;
struct doc_modification : public modification {
LEAN_MODIFICATION("doc")
name m_decl;
std::string m_doc;
doc_modification() {}
doc_modification(name const & decl, std::string const & doc) : m_decl(decl), m_doc(doc) {}
void perform(environment & env) const override {
auto ext = get_extension(env);
ext.m_doc_string_map.insert(m_decl, m_doc);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_decl << m_doc;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name decl; std::string doc;
d >> decl >> doc;
return std::make_shared<doc_modification>(decl, doc);
}
};
static void remove_blank_lines_begin(std::string & s) {
optional<std::string::iterator> found;
@ -144,7 +167,8 @@ environment add_doc_string(environment const & env, name const & n, std::string
ext.m_doc_string_map.insert(n, doc);
ext.m_module_doc = cons(doc_entry(n, doc), ext.m_module_doc);
auto new_env = update(env, ext);
return module::add(new_env, *g_doc_key, [=](environment const &, serializer & s) { s << n << doc; });
// TODO(gabriel,leo): why does this not update the module documentation?
return module::add(new_env, std::make_shared<doc_modification>(n, doc));
}
optional<std::string> get_doc_string(environment const & env, name const & n) {
@ -161,24 +185,13 @@ void get_module_doc_strings(environment const & env, buffer<doc_entry> & result)
std::reverse(result.begin(), result.end());
}
static void documentation_reader(deserializer & d, environment & env) {
name n; std::string doc;
d >> n >> doc;
auto ext = get_extension(env);
ext.m_doc_string_map.insert(n, doc);
env = update(env, ext);
}
void initialize_documentation() {
g_ext = new documentation_ext_reg();
g_documentation = new name("documentation");
g_doc_key = new std::string("doc");
register_module_object_reader(*g_doc_key, documentation_reader);
doc_modification::init();
}
void finalize_documentation() {
delete g_doc_key;
delete g_documentation;
doc_modification::finalize();
delete g_ext;
}
}

54
src/library/export_decl.cpp
View file

@ -10,8 +10,6 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
namespace lean {
static std::string * g_export_decl_key = nullptr;
static std::string * g_active_export_decls_key = nullptr;
static void write_pair_name(serializer & s, pair<name, name> const & p) {
s << p.first << p.second;
@ -66,14 +64,35 @@ static environment update(environment const & env, export_decl_env_ext const & e
return env.update(g_ext->m_ext_id, std::make_shared<export_decl_env_ext>(ext));
}
static void read_export_decls(deserializer & d, environment & env) {
name in_ns;
export_decl e;
d >> in_ns >> e.m_ns >> e.m_as >> e.m_had_explicit;
e.m_except_names = read_list<name>(d, read_name);
e.m_renames = read_list<pair<name, name>>(d, read_pair_name);
env = add_export_decl(env, in_ns, e);
}
struct export_decl_modification : public modification {
LEAN_MODIFICATION("export_decl")
name m_in_ns;
export_decl m_export_decl;
export_decl_modification() {}
export_decl_modification(name const & in_ns, export_decl const & e) :
m_in_ns(in_ns), m_export_decl(e) {}
void perform(environment & env) const override {
env = add_export_decl(env, m_in_ns, m_export_decl);
}
void serialize(serializer & s) const override {
s << m_in_ns << m_export_decl.m_ns << m_export_decl.m_as << m_export_decl.m_had_explicit;
write_list<name>(s, m_export_decl.m_except_names);
write_list<pair<name, name>>(s, m_export_decl.m_renames);
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
auto m = std::make_shared<export_decl_modification>();
auto & e = m->m_export_decl;
d >> m->m_in_ns >> e.m_ns >> e.m_as >> e.m_had_explicit;
e.m_except_names = read_list<name>(d, read_name);
e.m_renames = read_list<pair<name, name>>(d, read_pair_name);
return m;
}
};
environment add_export_decl(environment const & env, name const & in_ns, export_decl const & e) {
auto ns_map = get_export_decl_extension(env).m_ns_map;
@ -85,11 +104,7 @@ environment add_export_decl(environment const & env, name const & in_ns, export_
return env;
auto new_env = update(env, export_decl_env_ext(insert(ns_map, in_ns, cons(e, decls))));
return module::add(new_env, *g_export_decl_key, [=](environment const &, serializer & s) {
s << in_ns << e.m_ns << e.m_as << e.m_had_explicit;
write_list<name>(s, e.m_except_names);
write_list<pair<name, name>>(s, e.m_renames);
});
return module::add(new_env, std::make_shared<export_decl_modification>(in_ns, e));
}
environment add_export_decl(environment const & env, export_decl const & entry) {
return add_export_decl(env, get_namespace(env), entry);
@ -109,7 +124,7 @@ struct active_export_decls_config {
}
// uses local scope only
static std::string const & get_serialization_key() { return *g_active_export_decls_key; }
static const char * get_serialization_key() { return "active_export_decls"; }
static void write_entry(serializer &, entry const &) { lean_unreachable(); }
static entry read_entry(deserializer &) { lean_unreachable(); }
};
@ -136,17 +151,14 @@ list<export_decl> get_active_export_decls(environment const & env) {
}
void initialize_export_decl() {
g_export_decl_key = new std::string("export_decl");
g_active_export_decls_key = new std::string("active_export_decls"); // unused
g_ext = new export_decl_env_ext_reg();
register_module_object_reader(*g_export_decl_key, read_export_decls);
export_decl_modification::init();
active_export_decls_ext::initialize();
}
void finalize_export_decl() {
active_export_decls_ext::finalize();
delete g_active_export_decls_key;
delete g_export_decl_key;
export_decl_modification::finalize();
delete g_ext;
}
}

50
src/library/inductive_compiler/ginductive.cpp
View file

@ -70,9 +70,6 @@ inline deserializer & operator>>(deserializer & d, ginductive_entry & entry) {
return d;
}
static name * g_ginductive_extension = nullptr;
static std::string * g_ginductive_key = nullptr;
struct ginductive_env_ext : public environment_extension {
list<name> m_all_nested_inds;
list<name> m_all_mutual_inds;
@ -163,9 +160,32 @@ static environment update(environment const & env, ginductive_env_ext const & ex
return env.update(g_ext->m_ext_id, std::make_shared<ginductive_env_ext>(ext));
}
environment register_ginductive_decl(environment const & env, ginductive_decl const & decl, ginductive_kind k) {
ginductive_env_ext ext(get_extension(env));
struct ginductive_modification : public modification {
LEAN_MODIFICATION("gind")
ginductive_entry m_entry;
ginductive_modification() {}
ginductive_modification(ginductive_entry const & entry) : m_entry(entry) {}
void perform(environment & env) const override {
auto ext = get_extension(env);
ext.register_ginductive_entry(m_entry);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_entry;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
ginductive_entry entry;
d >> entry;
return std::make_shared<ginductive_modification>(entry);
}
};
environment register_ginductive_decl(environment const & env, ginductive_decl const & decl, ginductive_kind k) {
ginductive_entry entry;
entry.m_kind = k;
entry.m_num_params = decl.get_num_params();
@ -185,9 +205,7 @@ environment register_ginductive_decl(environment const & env, ginductive_decl co
}
entry.m_intro_rules = to_list(intro_rules);
ext.register_ginductive_entry(entry);
environment new_env = update(env, ext);
return module::add(new_env, *g_ginductive_key, [=](environment const &, serializer & s) { s << entry; });
return module::add_and_perform(env, std::make_shared<ginductive_modification>(entry));
}
optional<ginductive_kind> is_ginductive(environment const & env, name const & ind_name) {
@ -218,25 +236,13 @@ list<name> get_ginductive_all_nested_inds(environment const & env) {
return get_extension(env).get_all_nested_inds();
}
static void ginductive_reader(deserializer & d, environment & env) {
ginductive_entry entry;
d >> entry;
ginductive_env_ext ext = get_extension(env);
ext.register_ginductive_entry(entry);
env = update(env, ext);
}
void initialize_inductive_compiler_ginductive() {
g_ginductive_extension = new name("ginductive_extension");
g_ginductive_key = new std::string("gind");
ginductive_modification::init();
g_ext = new ginductive_env_ext_reg();
register_module_object_reader(*g_ginductive_key, ginductive_reader);
}
void finalize_inductive_compiler_ginductive() {
delete g_ginductive_extension;
delete g_ginductive_key;
ginductive_modification::finalize();
delete g_ext;
}
}

7
src/library/inverse.cpp
View file

@ -31,7 +31,6 @@ struct inverse_state {
};
static name * g_inverse_name = nullptr;
static std::string * g_key = nullptr;
struct inverse_config {
typedef inverse_state state;
@ -42,8 +41,8 @@ struct inverse_config {
static name const & get_class_name() {
return *g_inverse_name;
}
static std::string const & get_serialization_key() {
return *g_key;
static const char * get_serialization_key() {
return "inverse";
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_fn << e.m_info.m_arity << e.m_info.m_inv << e.m_info.m_inv_arity << e.m_info.m_lemma;
@ -107,7 +106,6 @@ environment add_inverse_lemma(environment const & env, name const & lemma, bool
void initialize_inverse() {
g_inverse_name = new name("inverse");
g_key = new std::string("inverse");
inverse_ext::initialize();
register_system_attribute(basic_attribute("inverse", "attribute for marking inverse lemmas "
@ -120,7 +118,6 @@ void initialize_inverse() {
void finalize_inverse() {
inverse_ext::finalize();
delete g_key;
delete g_inverse_name;
}
}

359
src/library/module.cpp
View file

@ -40,11 +40,9 @@ corrupted_file_exception::corrupted_file_exception(std::string const & fname):
exception(sstream() << "failed to import '" << fname << "', file is corrupted, please regenerate the file from sources") {
}
typedef pair<std::string, std::function<void(environment const &, serializer &)>> writer;
struct module_ext : public environment_extension {
list<module_name> m_direct_imports;
list<writer> m_writers;
list<std::shared_ptr<modification const>> m_modifications;
list<name> m_module_univs;
list<name> m_module_decls;
name_set m_module_defs;
@ -103,7 +101,6 @@ optional<std::string> get_decl_olean(environment const & env, name const & decl_
return optional<std::string>();
}
static std::string * g_pos_info_key = nullptr;
LEAN_THREAD_VALUE(bool, g_has_pos, false);
LEAN_THREAD_VALUE(unsigned, g_curr_line, 0);
LEAN_THREAD_VALUE(unsigned, g_curr_column, 0);
@ -118,17 +115,36 @@ module::scope_pos_info::~scope_pos_info() {
g_has_pos = false;
}
struct pos_info_mod : public modification {
LEAN_MODIFICATION("PInfo")
name m_decl_name;
pos_info m_pos_info;
pos_info_mod(name const & decl_name, pos_info const & pos) :
m_decl_name(decl_name), m_pos_info(pos) {}
void perform(environment & env) const override {
auto ext = get_extension(env);
ext.m_decl2pos_info.insert(m_decl_name, m_pos_info);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_decl_name << m_pos_info.first << m_pos_info.second;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name decl_name; unsigned line, column;
d >> decl_name >> line >> column;
return std::make_shared<pos_info_mod>(decl_name, pos_info {line, column});
}
};
static environment add_decl_pos_info(environment const & env, name const & decl_name) {
if (!g_has_pos)
return env;
module_ext ext = get_extension(env);
unsigned line = g_curr_line;
unsigned column = g_curr_column;
ext.m_decl2pos_info.insert(decl_name, mk_pair(line, column));
environment new_env = update(env, ext);
return module::add(new_env, *g_pos_info_key, [=](environment const &, serializer & s) {
s << decl_name << line << column;
});
return module::add_and_perform(env, std::make_shared<pos_info_mod>(decl_name, pos_info {g_curr_line, g_curr_column}));
}
optional<pos_info> get_decl_pos_info(environment const & env, name const & decl_name) {
@ -152,13 +168,6 @@ environment add_transient_decl_pos_info(environment const & env, name const & de
return update(env, ext);
}
static void pos_info_reader(deserializer & d, environment & env) {
name decl_name;
unsigned line, column;
d >> decl_name >> line >> column;
env = add_transient_decl_pos_info(env, decl_name, pos_info(line, column));
}
static char const * g_olean_end_file = "EndFile";
static char const * g_olean_header = "oleanfile";
@ -182,38 +191,14 @@ deserializer & operator>>(deserializer & d, module_name & r) {
return d;
}
LEAN_THREAD_PTR(std::vector<task_result<expr>>, g_export_delayed_proofs);
class scoped_delayed_proofs {
std::vector<task_result<expr>> * m_old;
public:
scoped_delayed_proofs(std::vector<task_result<expr>> & r) {
m_old = g_export_delayed_proofs;
g_export_delayed_proofs = &r;
}
~scoped_delayed_proofs() {
g_export_delayed_proofs = m_old;
}
};
void export_module(std::ostream & out, environment const & env) {
module_ext const & ext = get_extension(env);
buffer<module_name> imports;
to_buffer(ext.m_direct_imports, imports);
std::reverse(imports.begin(), imports.end());
buffer<writer const *> writers;
for (writer const & w : ext.m_writers)
writers.push_back(&w);
std::reverse(writers.begin(), writers.end());
void write_module(loaded_module const & mod, std::ostream & out) {
std::ostringstream out1(std::ios_base::binary);
serializer s1(out1);
// store objects
for (auto p : writers) {
s1 << p->first;
p->second(env, s1);
for (auto p : mod.m_modifications) {
s1 << std::string(p->get_key());
p->serialize(s1);
}
s1 << g_olean_end_file;
@ -223,8 +208,8 @@ void export_module(std::ostream & out, environment const & env) {
s2 << g_olean_header << LEAN_VERSION_MAJOR << LEAN_VERSION_MINOR << LEAN_VERSION_PATCH;
s2 << h;
// store imported files
s2 << imports.size();
for (auto m : imports)
s2 << static_cast<unsigned>(mod.m_imports.size());
for (auto m : mod.m_imports)
s2 << m;
// store object code
s2.write_unsigned(r.size());
@ -232,41 +217,144 @@ void export_module(std::ostream & out, environment const & env) {
s2.write_char(r[i]);
}
std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env) {
std::vector<task_result<expr>> delayed_proofs;
scoped_delayed_proofs _(delayed_proofs);
export_module(out, env);
return delayed_proofs;
loaded_module export_module(environment const & env, std::string const & mod_name) {
loaded_module out;
out.m_module_name = mod_name;
module_ext const & ext = get_extension(env);
for (auto & i : ext.m_direct_imports)
out.m_imports.push_back(i);
std::reverse(out.m_imports.begin(), out.m_imports.end());
for (auto & w : ext.m_modifications)
out.m_modifications.push_back(w);
std::reverse(out.m_modifications.begin(), out.m_modifications.end());
return out;
}
typedef std::unordered_map<std::string, module_object_reader> object_readers;
typedef std::unordered_map<std::string, module_modification_reader> object_readers;
static object_readers * g_object_readers = nullptr;
static object_readers & get_object_readers() { return *g_object_readers; }
void register_module_object_reader(std::string const & k, module_object_reader r) {
void register_module_object_reader(std::string const & k, module_modification_reader && r) {
object_readers & readers = get_object_readers();
lean_assert(readers.find(k) == readers.end());
readers[k] = r;
}
static std::string * g_glvl_key = nullptr;
static std::string * g_decl_key = nullptr;
static std::string * g_inductive = nullptr;
static std::string * g_quotient = nullptr;
struct import_helper {
static environment add_unchecked(environment const & env, declaration const & decl) {
return env.add(certify_or_check(env, decl));
}
static certified_declaration certify_or_check(environment const & env, declaration const & decl) {
return certify_unchecked::certify_or_check(env, decl);
}
};
struct glvl_modification : public modification {
LEAN_MODIFICATION("glvl")
name m_name;
glvl_modification() {}
glvl_modification(name const & name) : m_name(name) {}
void perform(environment & env) const override {
env = env.add_universe(m_name);
}
void serialize(serializer & s) const override {
s << m_name;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<glvl_modification>(read_name(d));
}
};
struct decl_modification : public modification {
LEAN_MODIFICATION("decl")
declaration m_decl;
decl_modification() {}
decl_modification(declaration const & decl) : m_decl(decl) {}
void perform(environment & env) const override {
auto decl = m_decl;
decl = unfold_untrusted_macros(env, decl);
if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
// ignore double sorrys
return;
}
// TODO(gabriel): this might be a bit more unsafe here than before
env = import_helper::add_unchecked(env, decl);
}
void serialize(serializer & s) const override {
s << m_decl;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<decl_modification>(read_declaration(d));
}
};
struct inductive_modification : public modification {
LEAN_MODIFICATION("ind")
inductive::certified_inductive_decl m_decl;
inductive_modification(inductive::certified_inductive_decl const & decl) : m_decl(decl) {}
void perform(environment & env) const override {
env = m_decl.add(env);
}
void serialize(serializer & s) const override {
s << m_decl;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<inductive_modification>(read_certified_inductive_decl(d));
}
};
struct quot_modification : public modification {
LEAN_MODIFICATION("quot")
void perform(environment & env) const override {
env = ::lean::declare_quotient(env);
}
void serialize(serializer &) const override {}
static std::shared_ptr<modification const> deserialize(deserializer &) {
return std::make_shared<quot_modification>();
}
};
namespace module {
environment add(environment const & env, std::string const & k, std::function<void(environment const &, serializer &)> const & wr) {
environment add(environment const & env, std::shared_ptr<modification const> const & modf) {
module_ext ext = get_extension(env);
ext.m_writers = cons(writer(k, wr), ext.m_writers);
ext.m_modifications = cons(modf, ext.m_modifications);
return update(env, ext);
}
environment add_and_perform(environment const & env, std::shared_ptr<modification const> const & modf) {
auto new_env = env;
modf->perform(new_env);
module_ext ext = get_extension(new_env);
ext.m_modifications = cons(modf, ext.m_modifications);
return update(new_env, ext);
}
environment add_universe(environment const & env, name const & l) {
environment new_env = env.add_universe(l);
module_ext ext = get_extension(env);
ext.m_module_univs = cons(l, ext.m_module_univs);
new_env = update(new_env, ext);
return add(new_env, *g_glvl_key, [=](environment const &, serializer & s) { s << l; });
return add_and_perform(update(env, ext), std::make_shared<glvl_modification>(l));
}
environment update_module_defs(environment const & env, declaration const & d) {
@ -282,30 +370,13 @@ environment update_module_defs(environment const & env, declaration const & d) {
}
}
static declaration theorem2axiom(declaration const & decl) {
lean_assert(decl.is_theorem());
return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
}
static environment export_decl(environment const & env, declaration const & d) {
name n = d.get_name();
return add(env, *g_decl_key, [=](environment const & env, serializer & s) {
auto d = env.get(n);
if (g_export_delayed_proofs && d.is_theorem()) {
s << true << theorem2axiom(d) << static_cast<unsigned>(g_export_delayed_proofs->size());
g_export_delayed_proofs->push_back(d.get_value_task());
} else {
s << false << d;
}
});
}
environment add(environment const & env, certified_declaration const & d) {
environment new_env = env.add(d);
declaration _d = d.get_declaration();
if (!check_computable(new_env, _d.get_name()))
new_env = mark_noncomputable(new_env, _d.get_name());
new_env = export_decl(update_module_defs(new_env, _d), _d);
new_env = update_module_defs(new_env, _d);
new_env = add(new_env, std::make_shared<decl_modification>(_d));
return add_decl_pos_info(new_env, _d.get_name());
}
@ -315,12 +386,7 @@ bool is_definition(environment const & env, name const & n) {
}
environment declare_quotient(environment const & env) {
environment new_env = ::lean::declare_quotient(env);
return add(new_env, *g_quotient, [=](environment const &, serializer &) {});
}
static void quotient_reader(deserializer &, environment & env) {
env = ::lean::declare_quotient(env);
return add_and_perform(env, std::make_shared<quot_modification>());
}
using inductive::certified_inductive_decl;
@ -335,9 +401,7 @@ environment add_inductive(environment env,
ext.m_module_decls = cons(decl.m_name, ext.m_module_decls);
new_env = update(new_env, ext);
new_env = add_decl_pos_info(new_env, decl.m_name);
return add(new_env, *g_inductive, [=](environment const &, serializer & s) {
s << cdecl;
});
return add(new_env, std::make_shared<inductive_modification>(cdecl));
}
} // end of namespace module
@ -376,28 +440,17 @@ std::pair<std::vector<module_name>, std::vector<char>> parse_olean(std::istream
return { imports, code };
}
struct import_helper {
static environment add_unchecked(environment const & env, declaration const & decl) {
return env.add(certify_or_check(env, decl));
}
static certified_declaration certify_or_check(environment const & env, declaration const & decl) {
return certify_unchecked::certify_or_check(env, decl);
}
};
static void import_module(environment & env, std::string const & module_file_name, module_name const & ref,
module_loader const & mod_ldr) {
auto res = mod_ldr(module_file_name, ref);
if (get_extension(env).m_imported.contains(res.m_module_name)) return;
std::istringstream in(res.m_obj_code, std::ios_base::binary);
auto olean = parse_olean(in, res.m_module_name, false);
for (auto & dep : olean.first) {
for (auto & dep : res.m_imports) {
import_module(env, res.m_module_name, dep, mod_ldr);
}
auto ext = get_extension(env);
ext.m_imported.insert(res.m_module_name);
env = update(env, ext);
import_module(olean.second, res.m_module_name, env, res.m_delayed_proofs);
import_module(res.m_modifications, res.m_module_name, env);
}
environment import_module(environment const & env0, std::string const & module_file_name,
@ -411,68 +464,52 @@ environment import_module(environment const & env0, std::string const & module_f
return env;
}
static optional<name> import_decl(deserializer & d, environment & env,
std::vector<task_result<expr>> const & delayed_proofs) {
bool is_delayed; d >> is_delayed;
declaration decl = read_declaration(d);
decl = unfold_untrusted_macros(env, decl);
if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
// TODO(gabriel): not sure why this is here
return optional<name>();
}
if (is_delayed) {
unsigned i; d >> i;
auto delayed_proof = delayed_proofs.at(i);
decl = mk_theorem(decl.get_name(), decl.get_univ_params(), decl.get_type(), delayed_proof);
}
env = import_helper::add_unchecked(env, decl);
return optional<name>(decl.get_name());
}
static void import_universe(deserializer & d, environment & env) {
name const l = read_name(d);
env = env.add_universe(l);
}
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
std::vector<task_result<expr>> const & delayed_proofs) {
// TODO(gabriel): update extension
modification_list parse_olean_modifications(std::vector<char> const & olean_code, std::string const & file_name) {
modification_list ms;
std::string s(olean_code.data(), olean_code.size());
std::istringstream in(s, std::ios_base::binary);
scoped_expr_caching enable_caching(true);
scoped_expr_caching enable_caching(false);
deserializer d(in, optional<std::string>(file_name));
object_readers & readers = get_object_readers();
unsigned obj_counter = 0;
while (true) {
std::string k;
d >> k;
if (k == g_olean_end_file) {
break;
} else if (k == *g_decl_key) {
if (auto decl_name = import_decl(d, env, delayed_proofs))
env = add_decl_olean(env, *decl_name, file_name);
} else if (k == *g_glvl_key) {
import_universe(d, env);
} else if (k == *g_inductive) {
inductive::certified_inductive_decl cdecl = read_certified_inductive_decl(d);
env = cdecl.add(env);
env = add_decl_olean(env, cdecl.get_decl().m_name, file_name);
} else {
object_readers & readers = get_object_readers();
auto it = readers.find(k);
if (it == readers.end())
throw exception(sstream() << "file '" << file_name << "' has been corrupted, unknown object: " << k);
it->second(d, env);
}
auto it = readers.find(k);
if (it == readers.end())
throw exception(sstream() << "file '" << file_name << "' has been corrupted, unknown object: " << k);
ms.emplace_back(it->second(d));
obj_counter++;
}
return ms;
}
void import_module(modification_list const & modifications, std::string const & file_name, environment & env) {
for (auto & m : modifications) {
m->perform(env);
if (auto dm = dynamic_cast<decl_modification const *>(m.get())) {
env = add_decl_olean(env, dm->m_decl.get_name(), file_name);
} else if (auto im = dynamic_cast<inductive_modification const *>(m.get())) {
env = add_decl_olean(env, im->m_decl.get_decl().m_name, file_name);
}
}
}
module_loader mk_olean_loader() {
bool check_hash = false;
return[=] (std::string const & module_fn, module_name const & ref) {
auto base_dir = dirname(module_fn.c_str());
auto fn = find_file(base_dir, ref.m_relative, ref.m_name, ".olean");
auto contents = read_file(fn, std::ios_base::binary);
return loaded_module { fn, contents, {} };
std::ifstream in(fn, std::ios_base::binary);
auto parsed = parse_olean(in, fn, check_hash);
auto modifs = parse_olean_modifications(parsed.second, fn);
return loaded_module { fn, parsed.first, modifs };
};
}
@ -485,22 +522,20 @@ module_loader mk_dummy_loader() {
void initialize_module() {
g_ext = new module_ext_reg();
g_object_readers = new object_readers();
g_glvl_key = new std::string("glvl");
g_decl_key = new std::string("decl");
g_inductive = new std::string("ind");
g_quotient = new std::string("quot");
g_pos_info_key = new std::string("PInfo");
register_module_object_reader(*g_quotient, module::quotient_reader);
register_module_object_reader(*g_pos_info_key, pos_info_reader);
glvl_modification::init();
decl_modification::init();
inductive_modification::init();
quot_modification::init();
pos_info_mod::init();
}
void finalize_module() {
delete g_inductive;
delete g_quotient;
delete g_decl_key;
delete g_glvl_key;
quot_modification::finalize();
pos_info_mod::finalize();
inductive_modification::finalize();
decl_modification::finalize();
glvl_modification::finalize();
delete g_object_readers;
delete g_ext;
delete g_pos_info_key;
}
}

43
src/library/module.h
View file

@ -27,10 +27,13 @@ struct module_name {
optional<unsigned> m_relative;
};
struct modification;
using modification_list = std::vector<std::shared_ptr<modification const>>;
struct loaded_module {
std::string m_module_name;
std::string m_obj_code;
std::vector<task_result<expr>> m_delayed_proofs;
std::vector<module_name> m_imports;
modification_list m_modifications;
};
using module_loader = std::function<loaded_module(std::string const &, module_name const &)>;
module_loader mk_olean_loader();
@ -66,25 +69,36 @@ optional<pos_info> get_decl_pos_info(environment const & env, name const & decl_
.olean files. We use this function for attaching position information to temporary functions. */
environment add_transient_decl_pos_info(environment const & env, name const & decl_name, pos_info const & pos);
/** \brief Store/Export module using \c env to the output stream \c out. */
void export_module(std::ostream & out, environment const & env);
std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env);
/** \brief Store/Export module using \c env. */
loaded_module export_module(environment const & env, std::string const & mod_name);
void write_module(loaded_module const & mod, std::ostream & out);
std::pair<std::vector<module_name>, std::vector<char>> parse_olean(
std::istream & in, std::string const & file_name, bool check_hash = true);
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
std::vector<task_result<expr>> const & delayed_proofs);
modification_list parse_olean_modifications(std::vector<char> const & olean_code, std::string const & file_name);
void import_module(modification_list const & modifications, std::string const & file_name, environment & env);
/** \brief A reader for importing data from a stream using deserializer \c d.
There is one way to update the environment being constructed.
1- Direct update it using \c env.
*/
typedef void (*module_object_reader)(deserializer & d, environment & env);
struct modification {
public:
virtual ~modification() {}
virtual const char * get_key() const = 0;
virtual void perform(environment &) const = 0;
virtual void serialize(serializer &) const = 0;
};
#define LEAN_MODIFICATION(k) \
static void init() { \
register_module_object_reader(k, module_modification_reader(deserialize)); \
} \
static void finalize() {} \
const char * get_key() const override { return k; }
using module_modification_reader = std::function<std::shared_ptr<modification const>(deserializer &)>;
/** \brief Register a module object reader. The key \c k is used to identify the class of objects
that can be read by the given reader.
*/
void register_module_object_reader(std::string const & k, module_object_reader r);
void register_module_object_reader(std::string const & k, module_modification_reader && r);
namespace module {
/** \brief Add a function that should be invoked when the environment is exported.
@ -93,7 +107,8 @@ namespace module {
\see module_object_reader
*/
environment add(environment const & env, std::string const & k, std::function<void(environment const &, serializer &)> const & writer);
environment add(environment const & env, std::shared_ptr<modification const> const & modif);
environment add_and_perform(environment const & env, std::shared_ptr<modification const> const & modif);
/** \brief Add the global universe declaration to the environment, and mark it to be exported. */
environment add_universe(environment const & env, name const & l);

23
src/library/module_mgr.cpp
View file

@ -65,12 +65,7 @@ public:
std::get<1>(d).m_name == import.m_name &&
std::get<1>(d).m_relative == import.m_relative) {
auto & mod_info = std::get<2>(d);
return loaded_module {
mod_info->m_mod,
mod_info->m_result.get().m_obj_code,
mod_info->m_result.get().m_obj_code_delayed_proofs,
};
return mod_info->m_result.get().m_loaded_module;
}
}
throw exception(sstream() << "could not resolve import: " << import.m_name);
@ -88,12 +83,7 @@ public:
mod.m_snapshots = std::move(m_snapshots);
{
std::ostringstream obj_code_buf(std::ios_base::binary);
mod.m_obj_code_delayed_proofs =
export_module_delayed(obj_code_buf, p.env());
mod.m_obj_code = obj_code_buf.str();
}
mod.m_loaded_module = export_module(p.env(), get_module_id());
mod.m_env = optional<environment>(p.env());
@ -132,15 +122,13 @@ public:
if (m_mod->m_source != module_src::LEAN)
throw exception("cannot build olean from olean");
auto res = m_mod->m_result.get();
auto env = *res.m_env;
if (!res.m_ok)
throw exception("not creating olean file because of errors");
auto olean_fn = olean_of_lean(m_mod->m_mod);
exclusive_file_lock output_lock(olean_fn);
std::ofstream out(olean_fn, std::ios_base::binary);
export_module(out, env);
write_module(res.m_loaded_module, out);
return {};
}
};
@ -181,7 +169,8 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
std::istringstream in2(obj_code, std::ios_base::binary);
auto olean_fn = olean_of_lean(id);
auto parsed_olean = parse_olean(in2, olean_fn);
bool check_hash = false;
auto parsed_olean = parse_olean(in2, olean_fn, check_hash);
auto mod = std::make_shared<module_info>();
@ -204,7 +193,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
return build_module(id, false, orig_module_stack);
module_info::parse_result res;
res.m_obj_code = obj_code;
res.m_loaded_module = { id, parsed_olean.first, parse_olean_modifications(parsed_olean.second, id) };
res.m_ok = true;
mod->m_result = mk_pure_task_result(res, "Loading " + olean_fn);

3
src/library/module_mgr.h
View file

@ -42,8 +42,7 @@ struct module_info {
options m_opts;
bool m_ok = false;
std::string m_obj_code;
std::vector<task_result<expr>> m_obj_code_delayed_proofs;
loaded_module m_loaded_module;
snapshot_vector m_snapshots;
};

46
src/library/native_compiler/native_compiler.cpp
View file

@ -471,29 +471,30 @@ void native_compile_module(environment const & env) {
native_compile_module(env, decls);
}
// Setup for the storage of native modules to .olean files.
static std::string *g_native_module_key = nullptr;
struct native_module_path_modification : public modification {
LEAN_MODIFICATION("native_module_path")
static void native_module_reader(
deserializer & d,
environment & /* env */) {
name fn;
d >> fn;
std::cout << "reading native module from meta-data: " << fn << std::endl;
// senv.update([&](environment const & env) -> environment {
// vm_decls ext = get_extension(env);
// // ext.update(fn, code_sz, code.data());
// // return update(env, ext);
// return
// });
}
name m_native_module_path;
native_module_path_modification() {}
native_module_path_modification(name const & fn) : m_native_module_path(fn) {}
void perform(environment &) const override {
// TODO(gabriel,jared): I have no idea what this is supposed to do.
// ???
}
void serialize(serializer & s) const override {
s << m_native_module_path;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<native_module_path_modification>(read_name(d));
}
};
environment set_native_module_path(environment & env, name const & n) {
return module::add(env, *g_native_module_key, [=] (environment const & e, serializer & s) {
std::cout << "writing out" << n << std::endl;
s << n;
native_compile_module(e);
});
return module::add(env, std::make_shared<native_module_path_modification>(n));
}
void initialize_native_compiler() {
@ -502,13 +503,12 @@ void initialize_native_compiler() {
register_trace_class({"compiler", "native"});
register_trace_class({"compiler", "native", "preprocess"});
register_trace_class({"compiler", "native", "cpp_compiler"});
g_native_module_key = new std::string("native_module_path");
register_module_object_reader(*g_native_module_key, native_module_reader);
native_module_path_modification::init();
}
void finalize_native_compiler() {
native::finalize_options();
delete g_native_module_key;
delete g_lean_install_path;
native_module_path_modification::finalize();
}
}

39
src/library/noncomputable.cpp
View file

@ -35,16 +35,28 @@ static environment update(environment const & env, noncomputable_ext const & ext
return env.update(g_ext->m_ext_id, std::make_shared<noncomputable_ext>(ext));
}
static name * g_noncomputable = nullptr;
static std::string * g_key = nullptr;
struct noncomputable_modification : public modification {
LEAN_MODIFICATION("ncomp")
static void noncomputable_reader(deserializer & d, environment & env) {
name n;
d >> n;
noncomputable_ext ext = get_extension(env);
ext.m_noncomputable.insert(n);
env = update(env, ext);
}
name m_decl;
noncomputable_modification() {}
noncomputable_modification(name const & decl) : m_decl(decl) {}
void perform(environment & env) const override {
noncomputable_ext ext = get_extension(env);
ext.m_noncomputable.insert(m_decl);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_decl;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<noncomputable_modification>(read_name(d));
}
};
static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) {
environment const & env = tc.env();
@ -77,7 +89,7 @@ environment mark_noncomputable(environment const & env, name const & n) {
auto ext = get_extension(env);
ext.m_noncomputable.insert(n);
environment new_env = update(env, ext);
return module::add(new_env, *g_key, [=](environment const &, serializer & s) { s << n; });
return module::add(new_env, std::make_shared<noncomputable_modification>(n));
}
optional<name> get_noncomputable_reason(environment const & env, name const & n) {
@ -105,14 +117,11 @@ bool check_computable(environment const & env, name const & n) {
void initialize_noncomputable() {
g_ext = new noncomputable_ext_reg();
g_noncomputable = new name("noncomputable");
g_key = new std::string("ncomp");
register_module_object_reader(*g_key, noncomputable_reader);
noncomputable_modification::init();
}
void finalize_noncomputable() {
delete g_key;
delete g_noncomputable;
noncomputable_modification::finalize();
delete g_ext;
}
}

45
src/library/private.cpp
View file

@ -32,12 +32,38 @@ static environment update(environment const & env, private_ext const & ext) {
}
static name * g_private = nullptr;
static std::string * g_prv_key = nullptr;
struct private_modification : public modification {
LEAN_MODIFICATION("prv")
name m_name, m_real;
private_modification() {}
private_modification(name const & n, name const & h) : m_name(n), m_real(h) {}
void perform(environment & env) const override {
private_ext ext = get_extension(env);
// we restore only the mapping hidden-name -> user-name (for pretty printing purposes)
ext.m_inv_map.insert(m_real, m_name);
ext.m_counter++;
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_name << m_real;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name n, h;
d >> n >> h;
return std::make_shared<private_modification>(n, h);
}
};
// Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
// export .olean files.
static environment preserve_private_data(environment const & env, name const & r, name const & n) {
return module::add(env, *g_prv_key, [=](environment const &, serializer & s) { s << n << r; });
return module::add(env, std::make_shared<private_modification>(n, r));
}
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
@ -56,16 +82,6 @@ pair<environment, name> add_private_name(environment const & env, name const & n
return mk_pair(new_env, r);
}
static void private_reader(deserializer & d, environment & env) {
name n, h;
d >> n >> h;
private_ext ext = get_extension(env);
// we restore only the mapping hidden-name -> user-name (for pretty printing purposes)
ext.m_inv_map.insert(h, n);
ext.m_counter++;
env = update(env, ext);
}
optional<name> hidden_to_user_name(environment const & env, name const & n) {
auto it = get_extension(env).m_inv_map.find(n);
return it ? optional<name>(*it) : optional<name>();
@ -78,12 +94,11 @@ bool is_private(environment const & env, name const & n) {
void initialize_private() {
g_ext = new private_ext_reg();
g_private = new name("private");
g_prv_key = new std::string("prv");
register_module_object_reader(*g_prv_key, private_reader);
private_modification::init();
}
void finalize_private() {
delete g_prv_key;
private_modification::finalize();
delete g_private;
delete g_ext;
}

48
src/library/projection.cpp
View file

@ -38,20 +38,35 @@ static environment update(environment const & env, projection_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<projection_ext>(ext));
}
static std::string * g_proj_key = nullptr;
struct proj_modification : public modification {
LEAN_MODIFICATION("proj")
static environment save_projection_info_core(environment const & env, name const & p, name const & mk, unsigned nparams,
unsigned i, bool inst_implicit) {
projection_ext ext = get_extension(env);
ext.m_info.insert(p, projection_info(mk, nparams, i, inst_implicit));
return update(env, ext);
}
name m_proj;
projection_info m_info;
proj_modification() {}
proj_modification(name const & proj, projection_info const & info) : m_proj(proj), m_info(info) {}
void perform(environment & env) const override {
projection_ext ext = get_extension(env);
ext.m_info.insert(m_proj, m_info);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_proj << m_info.m_constructor << m_info.m_nparams << m_info.m_i << m_info.m_inst_implicit;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name p, mk; unsigned nparams, i; bool inst_implicit;
d >> p >> mk >> nparams >> i >> inst_implicit;
return std::make_shared<proj_modification>(p, projection_info(mk, nparams, i, inst_implicit));
}
};
environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) {
environment new_env = save_projection_info_core(env, p, mk, nparams, i, inst_implicit);
return module::add(new_env, *g_proj_key, [=](environment const &, serializer & s) {
s << p << mk << nparams << i << inst_implicit;
});
return module::add_and_perform(env, std::make_shared<proj_modification>(
p, projection_info(mk, nparams, i, inst_implicit)));
}
projection_info const * get_projection_info(environment const & env, name const & p) {
@ -63,12 +78,6 @@ name_map<projection_info> const & get_projection_info_map(environment const & en
return get_extension(env).m_info;
}
static void projection_info_reader(deserializer & d, environment & env) {
name p, mk; unsigned nparams, i; bool inst_implicit;
d >> p >> mk >> nparams >> i >> inst_implicit;
env = save_projection_info_core(env, p, mk, nparams, i, inst_implicit);
}
/** \brief Return true iff the type named \c S can be viewed as
a structure in the given environment.
@ -82,12 +91,11 @@ bool is_structure_like(environment const & env, name const & S) {
void initialize_projection() {
g_ext = new projection_ext_reg();
g_proj_key = new std::string("proj");
register_module_object_reader(*g_proj_key, projection_info_reader);
proj_modification::init();
}
void finalize_projection() {
delete g_proj_key;
proj_modification::finalize();
delete g_ext;
}
}

41
src/library/protected.cpp
View file

@ -28,21 +28,31 @@ static environment update(environment const & env, protected_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<protected_ext>(ext));
}
static std::string * g_prt_key = nullptr;
struct protected_modification : public modification {
LEAN_MODIFICATION("prt")
name m_name;
protected_modification() {}
protected_modification(name const & n) : m_name(n) {}
void perform(environment & env) const override {
protected_ext ext = get_extension(env);
ext.m_protected.insert(m_name);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_name;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<protected_modification>(read_name(d));
}
};
environment add_protected(environment const & env, name const & n) {
protected_ext ext = get_extension(env);
ext.m_protected.insert(n);
environment new_env = update(env, ext);
return module::add(new_env, *g_prt_key, [=](environment const &, serializer & s) { s << n; });
}
static void protected_reader(deserializer & d, environment & env) {
name n;
d >> n;
protected_ext ext = get_extension(env);
ext.m_protected.insert(n);
env = update(env, ext);
return module::add_and_perform(env, std::make_shared<protected_modification>(n));
}
bool is_protected(environment const & env, name const & n) {
@ -60,12 +70,11 @@ name get_protected_shortest_name(name const & n) {
void initialize_protected() {
g_ext = new protected_ext_reg();
g_prt_key = new std::string("prt");
register_module_object_reader(*g_prt_key, protected_reader);
protected_modification::init();
}
void finalize_protected() {
delete g_prt_key;
protected_modification::finalize();
delete g_ext;
}
}

8
src/library/relation_manager.cpp
View file

@ -147,8 +147,6 @@ struct rel_state {
}
};
static std::string * g_key = nullptr;
struct rel_config {
typedef rel_state state;
typedef rel_entry entry;
@ -161,9 +159,7 @@ struct rel_config {
case op_kind::Symm: s.add_symm(env, e.m_name); break;
}
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "REL"; }
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.m_kind) << e.m_name;
}
@ -323,7 +319,6 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
}
void initialize_relation_manager() {
g_key = new std::string("REL");
rel_ext::initialize();
register_system_attribute(basic_attribute("refl", "reflexive relation",
[](environment const & env, io_state const &, name const & d, unsigned,
@ -352,6 +347,5 @@ void initialize_relation_manager() {
void finalize_relation_manager() {
rel_ext::finalize();
delete g_key;
}
}

42
src/library/scoped_ext.cpp
View file

@ -77,14 +77,37 @@ optional<name> to_valid_namespace_name(environment const & env, name const & n)
return optional<name>();
}
static std::string * g_new_namespace_key = nullptr;
struct new_namespace_modification : public modification {
LEAN_MODIFICATION("nspace")
name m_ns;
new_namespace_modification(name const & ns) : m_ns(ns) {}
new_namespace_modification() {}
void perform(environment & env) const override {
scope_mng_ext ext = get_extension(env);
ext.m_namespace_set.insert(m_ns);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_ns;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name n;
d >> n;
return std::make_shared<new_namespace_modification>(n);
}
};
environment add_namespace(environment const & env, name const & ns) {
scope_mng_ext ext = get_extension(env);
if (!ext.m_namespace_set.contains(ns)) {
ext.m_namespace_set.insert(ns);
environment r = update(env, ext);
r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
r = module::add(r, std::make_shared<new_namespace_modification>(ns));
if (ns.is_atomic())
return r;
else
@ -114,18 +137,10 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
r = std::get<0>(t)(r, ios, k);
}
if (save_ns)
r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << new_n; });
r = module::add(r, std::make_shared<new_namespace_modification>(new_n));
return r;
}
static void namespace_reader(deserializer & d, environment & env) {
name n;
d >> n;
scope_mng_ext ext = get_extension(env);
ext.m_namespace_set.insert(n);
env = update(env, ext);
}
environment pop_scope_core(environment const & env, io_state const & ios) {
scope_mng_ext ext = get_extension(env);
if (is_nil(ext.m_namespaces))
@ -159,12 +174,11 @@ bool has_open_scopes(environment const & env) {
void initialize_scoped_ext() {
g_exts = new scoped_exts();
g_ext = new scope_mng_ext_reg();
g_new_namespace_key = new std::string("nspace");
register_module_object_reader(*g_new_namespace_key, namespace_reader);
new_namespace_modification::init();
}
void finalize_scoped_ext() {
delete g_new_namespace_key;
new_namespace_modification::finalize();
delete g_exts;
delete g_ext;
}

36
src/library/scoped_ext.h
View file

@ -75,7 +75,7 @@ class scoped_ext : public environment_extension {
}
static void write_entry(serializer & s, entry const & e) { Config::write_entry(s, e); }
static entry read_entry(deserializer & d) { return Config::read_entry(d); }
static std::string const & get_serialization_key() { return Config::get_serialization_key(); }
static const char * get_serialization_key() { return Config::get_serialization_key(); }
static optional<unsigned> get_fingerprint(entry const & e) {
return Config::get_fingerprint(e);
}
@ -128,13 +128,37 @@ public:
return r;
}
struct modification : public lean::modification {
LEAN_MODIFICATION(get_serialization_key())
entry m_entry;
modification() {}
modification(entry const & e) : m_entry(e) {}
void perform(environment & env) const override {
env = register_entry(env, get_global_ios(), m_entry);
}
void serialize(serializer & s) const override {
write_entry(s, m_entry);
}
static std::shared_ptr<lean::modification const> deserialize(deserializer & d) {
return std::make_shared<modification>(read_entry(d));
}
};
struct reg {
unsigned m_ext_id;
reg() {
register_scoped_ext(push_fn, pop_fn);
register_module_object_reader(get_serialization_key(), reader);
modification::init();
m_ext_id = environment::register_extension(std::make_shared<scoped_ext>());
}
~reg() {
modification::finalize();
}
};
static reg * g_ext;
@ -166,17 +190,11 @@ public:
return update(env, get(env)._add_tmp_entry(env, ios, e));
} else {
name n = get_namespace(env);
env = module::add(env, get_serialization_key(), [=](environment const &, serializer & s) {
write_entry(s, e);
});
env = module::add(env, std::make_shared<modification>(e));
return update(env, get(env)._register_entry(env, ios, e));
}
}
static void reader(deserializer & d, environment & env) {
entry e = read_entry(d);
env = register_entry(env, get_global_ios(), e);
}
static state const & get_state(environment const & env) {
return get(env).m_state;
}

40
src/library/tactic/eqn_lemmas.cpp
View file

@ -32,9 +32,6 @@ static environment update(environment const & env, eqn_lemmas_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<eqn_lemmas_ext>(ext));
}
static name * g_eqn_lemmas = nullptr;
static std::string * g_eqn_lemmas_key = nullptr;
environment add_eqn_lemma_core(environment const & env, name const & eqn_lemma) {
type_context ctx(env, transparency_mode::None);
simp_lemmas lemmas = add(ctx, simp_lemmas(), eqn_lemma, LEAN_DEFAULT_PRIORITY);
@ -61,9 +58,29 @@ environment add_eqn_lemma_core(environment const & env, name const & eqn_lemma)
return update(env, ext);
}
struct eqn_lemmas_modification : public modification {
LEAN_MODIFICATION("EqnL")
name m_lemma;
eqn_lemmas_modification() {}
eqn_lemmas_modification(name const & lemma) : m_lemma(lemma) {}
void perform(environment & env) const override {
env = add_eqn_lemma_core(env, m_lemma);
}
void serialize(serializer & s) const override {
s << m_lemma;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<eqn_lemmas_modification>(read_name(d));
}
};
environment add_eqn_lemma(environment const & env, name const & eqn_lemma) {
environment new_env = add_eqn_lemma_core(env, eqn_lemma);
return module::add(new_env, *g_eqn_lemmas_key, [=](environment const &, serializer & s) { s << eqn_lemma; });
return module::add_and_perform(env, std::make_shared<eqn_lemmas_modification>(eqn_lemma));
}
void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer<simp_lemma> & result) {
@ -81,22 +98,13 @@ bool has_eqn_lemmas(environment const & env, name const & cname) {
return ext.m_lemmas.contains(cname);
}
static void eqn_lemmas_reader(deserializer & d, environment & env) {
name lemma;
d >> lemma;
env = add_eqn_lemma_core(env, lemma);
}
void initialize_eqn_lemmas() {
g_ext = new eqn_lemmas_ext_reg();
g_eqn_lemmas = new name("eqn_lemmas");
g_eqn_lemmas_key = new std::string("EqnL");
register_module_object_reader(*g_eqn_lemmas_key, eqn_lemmas_reader);
eqn_lemmas_modification::init();
}
void finalize_eqn_lemmas() {
eqn_lemmas_modification::finalize();
delete g_ext;
delete g_eqn_lemmas;
delete g_eqn_lemmas_key;
}
}

43
src/library/tactic/kabstract.cpp
View file

@ -100,13 +100,33 @@ static environment update(environment const & env, key_equivalence_ext const & e
return env.update(g_ext->m_ext_id, std::make_shared<key_equivalence_ext>(ext));
}
static std::string * g_key_equivalence_key = nullptr;
struct key_equivalence_modification : public modification {
LEAN_MODIFICATION("key_eqv")
name m_n1, m_n2;
key_equivalence_modification() {}
key_equivalence_modification(name const & n1, name const & n2) : m_n1(n1), m_n2(n2) {}
void perform(environment & env) const override {
key_equivalence_ext ext = get_extension(env);
ext.add_alias(m_n1, m_n2);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_n1 << m_n2;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name n1, n2;
d >> n1 >> n2;
return std::make_shared<key_equivalence_modification>(n1, n2);
}
};
environment add_key_equivalence(environment const & env, name const & n1, name const & n2) {
key_equivalence_ext ext = get_extension(env);
ext.add_alias(n1, n2);
environment new_env = update(env, ext);
return module::add(new_env, *g_key_equivalence_key, [=](environment const &, serializer & s) { s << n1 << n2; });
return module::add_and_perform(env, std::make_shared<key_equivalence_modification>(n1, n2));
}
bool is_key_equivalent(environment const & env, name const & n1, name const & n2) {
@ -130,14 +150,6 @@ void for_each_key_equivalence(environment const & env, std::function<void(buffer
});
}
static void key_equivalence_reader(deserializer & d, environment & env) {
name n1, n2;
d >> n1 >> n2;
key_equivalence_ext ext = get_extension(env);
ext.add_alias(n1, n2);
env = update(env, ext);
}
expr kabstract(type_context & ctx, expr const & e, expr const & t, occurrences const & occs) {
lean_assert(closed(e));
head_index idx1(t);
@ -165,12 +177,11 @@ expr kabstract(type_context & ctx, expr const & e, expr const & t, occurrences c
void initialize_kabstract() {
g_ext = new key_equivalence_ext_reg();
g_key_equivalence_key = new std::string("keyeqv");
register_module_object_reader(*g_key_equivalence_key, key_equivalence_reader);
key_equivalence_modification::init();
}
void finalize_kabstract() {
delete g_key_equivalence_key;
key_equivalence_modification::finalize();
delete g_ext;
}
}

37
src/library/tactic/user_attribute.cpp
View file

@ -25,8 +25,6 @@ Author: Sebastian Ullrich
namespace lean {
/* typed_attribute */
static std::string * g_key = nullptr;
struct user_attr_data : public attr_data {
// to be filled
@ -80,13 +78,6 @@ static environment add_user_attr(environment const & env, name const & d) {
return update(env, ext);
}
static void user_attr_reader(deserializer & d, environment & env) {
name n;
d >> n;
env = add_user_attr(env, n);
}
/* Integration into attribute_manager */
class actual_user_attribute_ext : public user_attribute_ext {
public:
@ -95,6 +86,26 @@ public:
}
};
struct user_attr_modification : public modification {
LEAN_MODIFICATION("USR_ATTR")
name m_name;
user_attr_modification() {}
user_attr_modification(name const & name) : m_name(name) {}
void perform(environment & env) const override {
env = add_user_attr(env, m_name);
}
void serialize(serializer & s) const override {
s << m_name;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<user_attr_modification>(read_name(d));
}
};
/* VM builtins */
vm_obj attribute_get_instances(vm_obj const & vm_n, vm_obj const & vm_s) {
@ -111,8 +122,7 @@ vm_obj attribute_register(vm_obj const & vm_n, vm_obj const & vm_s) {
auto const & s = to_tactic_state(vm_s);
auto const & n = to_name(vm_n);
LEAN_TACTIC_TRY;
auto env = add_user_attr(s.env(), n);
env = module::add(env, *g_key, [=](environment const &, serializer & s) { s << n; });
auto env = module::add_and_perform(s.env(), std::make_shared<user_attr_modification>(n));
return mk_tactic_success(set_env(s, env));
LEAN_TACTIC_CATCH(s);
}
@ -251,12 +261,11 @@ void initialize_user_attribute() {
register_trace_class("user_attributes_cache");
g_ext = new user_attr_ext_reg();
g_key = new std::string("USR_ATTR");
register_module_object_reader(*g_key, user_attr_reader);
user_attr_modification::init();
set_user_attribute_ext(std::unique_ptr<user_attribute_ext>(new actual_user_attribute_ext));
}
void finalize_user_attribute() {
delete g_key;
user_attr_modification::finalize();
delete g_ext;
}
}

9
src/library/unification_hint.cpp
View file

@ -40,8 +40,6 @@ int unification_hint_cmp::operator()(unification_hint const & uh1, unification_h
/* Environment extension */
static std::string * g_key = nullptr;
struct unification_hint_state {
unification_hints m_hints;
name_map<unsigned> m_decl_names_to_prio; // Note: redundant but convenient
@ -127,9 +125,7 @@ struct unification_hint_config {
// TODO(dhs): the downside to this approach is that a [unify] tag on an actual axiom will be silently ignored.
if (decl.is_definition()) s.register_hint(e.m_decl_name, decl.get_value(), e.m_priority);
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "UNIFICATION_HINT"; }
static void write_entry(serializer & s, entry const & e) {
s << e.m_decl_name << e.m_priority;
}
@ -200,8 +196,6 @@ format pp_unification_hints(unification_hints const & hints, formatter const & f
}
void initialize_unification_hint() {
g_key = new std::string("UNIFICATION_HINT");
unification_hint_ext::initialize();
register_system_attribute(basic_attribute("unify", "unification hint", add_unification_hint));
@ -209,6 +203,5 @@ void initialize_unification_hint() {
void finalize_unification_hint() {
unification_hint_ext::finalize();
delete g_key;
}
}

8
src/library/user_recursors.cpp
View file

@ -298,8 +298,6 @@ struct recursor_state {
}
};
static std::string * g_key = nullptr;
struct recursor_config {
typedef recursor_state state;
typedef recursor_info entry;
@ -307,9 +305,7 @@ struct recursor_config {
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
s.insert(e);
}
static std::string const & get_serialization_key() {
return *g_key;
}
static const char * get_serialization_key() { return "UREC"; }
static void write_entry(serializer & s, entry const & e) {
e.write(s);
}
@ -357,7 +353,6 @@ static indices_attribute const & get_recursor_attribute() {
}
void initialize_user_recursors() {
g_key = new std::string("UREC");
recursor_ext::initialize();
register_system_attribute(indices_attribute("recursor", "user defined recursor",
[](environment const & env, io_state const &, name const & n, unsigned,
@ -372,6 +367,5 @@ void initialize_user_recursors() {
void finalize_user_recursors() {
recursor_ext::finalize();
delete g_key;
}
}

182
src/library/vm/vm.cpp
View file

@ -932,13 +932,10 @@ struct vm_decls : public environment_extension {
return idx;
}
void update(name const & n, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> const & pos,
optional<std::string> const & olean = optional<std::string>()) {
unsigned idx = get_vm_index(n);
vm_decl const * d = m_decls.find(idx);
lean_assert(d);
m_decls.insert(idx, vm_decl(n, idx, d->get_expr(), code_sz, code, args_info, pos, olean));
void update(vm_decl const & new_decl) {
lean_assert(new_decl.get_idx() == get_vm_index(new_decl.get_name()));
lean_assert(m_decls.contains(new_decl.get_idx()));
m_decls.insert(new_decl.get_idx(), new_decl);
}
};
@ -1028,59 +1025,100 @@ optional<unsigned> get_vm_builtin_idx(name const & n) {
return optional<unsigned>();
}
static std::string * g_vm_reserve_key = nullptr;
static std::string * g_vm_code_key = nullptr;
struct vm_reserve_modification : public modification {
LEAN_MODIFICATION("VMR")
name m_fn;
expr m_e;
vm_reserve_modification(name const & fn, expr const & e) : m_fn(fn), m_e(e) {}
void perform(environment & env) const override {
vm_decls ext = get_extension(env);
ext.reserve(m_fn, m_e);
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_fn << m_e;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name fn; expr e;
d >> fn >> e;
return std::make_shared<vm_reserve_modification>(fn, e);
}
};
struct vm_code_modification : public modification {
LEAN_MODIFICATION("VMC")
vm_decl m_decl;
vm_code_modification(vm_decl const & decl) : m_decl(decl) {}
vm_code_modification() {}
void perform(environment & env) const override {
vm_decls ext = get_extension(env);
ext.update(m_decl);
env = update(env, ext);
}
void serialize(serializer & s) const override {
unsigned code_sz = m_decl.get_code_size();
s << m_decl.get_name() << m_decl.get_expr() << code_sz << m_decl.get_pos_info();
write_list(s, m_decl.get_args_info());
auto c = m_decl.get_code();
for (unsigned i = 0; i < code_sz; i++)
c[i].serialize(s, get_vm_name);
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
name fn; unsigned code_sz; expr e; optional<pos_info> pos;
d >> fn >> e >> code_sz >> pos;
auto args_info = read_list<vm_local_info>(d);
buffer<vm_instr> code;
for (unsigned i = 0; i < code_sz; i++)
code.emplace_back(read_vm_instr(d));
optional<std::string> file_name; // TODO(gabriel)
return std::make_shared<vm_code_modification>(
vm_decl(fn, get_vm_index(fn), e, code_sz, code.data(), args_info, pos, file_name));
}
};
struct vm_monitor_modification : public modification {
LEAN_MODIFICATION("VMMonitor")
name m_monitor;
vm_monitor_modification() {}
vm_monitor_modification(name const & n) : m_monitor(n) {}
void perform(environment & env) const override {
vm_decls ext = get_extension(env);
ext.m_monitor = m_monitor;
env = update(env, ext);
}
void serialize(serializer & s) const override {
s << m_monitor;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
auto m = std::make_shared<vm_monitor_modification>();
d >> m->m_monitor;
return m;
}
};
environment reserve_vm_index(environment const & env, name const & fn, expr const & e) {
vm_decls ext = get_extension(env);
ext.reserve(fn, e);
environment new_env = update(env, ext);
return module::add(new_env, *g_vm_reserve_key, [=](environment const &, serializer & s) {
s << fn << e;
});
}
static void reserve_reader(deserializer & d, environment & env) {
name fn; expr e;
d >> fn >> e;
vm_decls ext = get_extension(env);
ext.reserve(fn, e);
env = update(env, ext);
}
void serialize_code(serializer & s, unsigned fidx, unsigned_map<vm_decl> const & decls) {
vm_decl const * d = decls.find(fidx);
s << d->get_name() << d->get_code_size() << d->get_pos_info();
write_list(s, d->get_args_info());
vm_instr const * code = d->get_code();
auto fn = [&](unsigned idx) { return decls.find(idx)->get_name(); };
for (unsigned i = 0; i < d->get_code_size(); i++) {
code[i].serialize(s, fn);
}
}
static void code_reader(deserializer & d, environment & env) {
name fn; unsigned code_sz; list<vm_local_info> args_info; optional<pos_info> pos;
d >> fn >> code_sz >> pos;
args_info = read_list<vm_local_info>(d);
vm_decls ext = get_extension(env);
buffer<vm_instr> code;
for (unsigned i = 0; i < code_sz; i++) {
code.push_back(read_vm_instr(d));
}
ext.update(fn, code_sz, code.data(), args_info, pos, d.get_fname());
env = update(env, ext);
return module::add_and_perform(env, std::make_shared<vm_reserve_modification>(fn, e));
}
environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> const & pos) {
vm_decls ext = get_extension(env);
ext.update(fn, code_sz, code, args_info, pos);
environment new_env = update(env, ext);
unsigned fidx = get_vm_index(fn);
return module::add(new_env, *g_vm_code_key, [=](environment const & env, serializer & s) {
serialize_code(s, fidx, get_extension(env).m_decls);
});
vm_decl decl(fn, get_vm_index(fn), get_vm_decl(env, fn)->get_expr(), code_sz, code, args_info, pos);
return module::add_and_perform(env, std::make_shared<vm_code_modification>(decl));
}
environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code,
@ -3181,20 +3219,11 @@ void* get_extern_symbol(std::string library_name, std::string extern_name) {
return library.symbol(extern_name);
}
static std::string * g_vm_monitor_key = nullptr;
static environment vm_monitor_register_core(environment const & env, name const & d) {
environment vm_monitor_register(environment const & env, name const & d) {
expr const & type = env.get(d).get_type();
if (!is_app_of(type, get_vm_monitor_name(), 1))
throw exception("invalid vm_monitor.register argument, must be name of a definition of type (vm_monitor ?s) ");
auto ext = get_extension(env);
ext.m_monitor = d;
return update(env, ext);
}
environment vm_monitor_register(environment const & env, name const & d) {
auto new_env = vm_monitor_register_core(env, d);
return module::add(new_env, *g_vm_monitor_key, [=](environment const &, serializer & s) { s << d; });
return module::add_and_perform(env, std::make_shared<vm_monitor_modification>(d));
}
environment load_external_fn(environment & env, name const & extern_n) {
@ -3237,14 +3266,6 @@ environment load_external_fn(environment & env, name const & extern_n) {
}
}
static void vm_monitor_reader(deserializer & d, environment & env) {
name n;
d >> n;
vm_decls ext = get_extension(env);
ext.m_monitor = n;
env = update(env, ext);
}
class vm_index_manager {
shared_mutex m_mutex;
std::unordered_map<name, unsigned, name_hash> m_name2idx;
@ -3330,12 +3351,9 @@ void finalize_vm_core() {
void initialize_vm() {
g_ext = new vm_decls_reg();
// g_may_update_vm_builtins = false;
g_vm_reserve_key = new std::string("VMR");
g_vm_code_key = new std::string("VMC");
g_vm_monitor_key = new std::string("VMMonitor");
register_module_object_reader(*g_vm_reserve_key, reserve_reader);
register_module_object_reader(*g_vm_code_key, code_reader);
register_module_object_reader(*g_vm_monitor_key, vm_monitor_reader);
vm_reserve_modification::init();
vm_code_modification::init();
vm_monitor_modification::init();
#if defined(LEAN_MULTI_THREAD)
g_profiler = new name{"profiler"};
g_profiler_freq = new name{"profiler", "freq"};
@ -3351,9 +3369,9 @@ void initialize_vm() {
void finalize_vm() {
delete g_ext;
delete g_vm_reserve_key;
delete g_vm_code_key;
delete g_vm_monitor_key;
vm_reserve_modification::finalize();
vm_code_modification::finalize();
vm_monitor_modification::finalize();
#if defined(LEAN_MULTI_THREAD)
delete g_profiler;
delete g_profiler_freq;