From a26e2c9108b63828113877fa9f559a9481ac85bf Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 19 Dec 2016 13:39:26 -0500 Subject: [PATCH] feat(library/module): intermediary data structure for environment modifications --- src/api/module.cpp | 3 +- src/frontends/lean/builtin_cmds.cpp | 36 +- src/frontends/lean/parser_config.cpp | 16 +- src/frontends/lean/parser_config.h | 1 + src/library/attribute_manager.cpp | 8 +- src/library/aux_recursors.cpp | 83 ++-- src/library/class.cpp | 7 +- src/library/documentation.cpp | 45 ++- src/library/export_decl.cpp | 54 ++- src/library/inductive_compiler/ginductive.cpp | 50 +-- src/library/inverse.cpp | 7 +- src/library/module.cpp | 359 ++++++++++-------- src/library/module.h | 43 ++- src/library/module_mgr.cpp | 23 +- src/library/module_mgr.h | 3 +- .../native_compiler/native_compiler.cpp | 46 +-- src/library/noncomputable.cpp | 39 +- src/library/private.cpp | 45 ++- src/library/projection.cpp | 48 ++- src/library/protected.cpp | 41 +- src/library/relation_manager.cpp | 8 +- src/library/scoped_ext.cpp | 42 +- src/library/scoped_ext.h | 36 +- src/library/tactic/eqn_lemmas.cpp | 40 +- src/library/tactic/kabstract.cpp | 43 ++- src/library/tactic/user_attribute.cpp | 37 +- src/library/unification_hint.cpp | 9 +- src/library/user_recursors.cpp | 8 +- src/library/vm/vm.cpp | 182 +++++---- 29 files changed, 769 insertions(+), 593 deletions(-) diff --git a/src/api/module.cpp b/src/api/module.cpp index a56114fdab..016be37b99 100644 --- a/src/api/module.cpp +++ b/src/api/module.cpp @@ -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; } diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 3bd1cff98c..773c29219a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -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 deserialize(deserializer & d) { + return std::make_shared(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(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; } } diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 424bfbc12b..f5a8dbf4f4 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -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; typedef scoped_ext 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(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; typedef scoped_ext 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; } } diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index bd8bf4ec54..ee80854afe 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -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); } diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 48e4a72336..44095f00bd 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -32,8 +32,6 @@ void set_user_attribute_ext(std::unique_ptr ext) { static std::vector> * 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(); g_user_attribute_ext = new user_attribute_ext(); g_incomp = new std::vector>(); - 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; diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp index ede5525a1c..497fc987e6 100644 --- a/src/library/aux_recursors.cpp +++ b/src/library/aux_recursors.cpp @@ -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(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 deserialize(deserializer & d) { + return std::make_shared(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 deserialize(deserializer & d) { + return std::make_shared(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(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(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; } } diff --git a/src/library/class.cpp b/src/library/class.cpp index cc0cdecc27..5e1311e4b4 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -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(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; diff --git a/src/library/documentation.cpp b/src/library/documentation.cpp index b31d5d25d4..f4ee897c6c 100644 --- a/src/library/documentation.cpp +++ b/src/library/documentation.cpp @@ -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(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 deserialize(deserializer & d) { + name decl; std::string doc; + d >> decl >> doc; + return std::make_shared(decl, doc); + } +}; static void remove_blank_lines_begin(std::string & s) { optional 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(n, doc)); } optional get_doc_string(environment const & env, name const & n) { @@ -161,24 +185,13 @@ void get_module_doc_strings(environment const & env, buffer & 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; } } diff --git a/src/library/export_decl.cpp b/src/library/export_decl.cpp index 701a640b80..347332304c 100644 --- a/src/library/export_decl.cpp +++ b/src/library/export_decl.cpp @@ -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 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(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(d, read_name); - e.m_renames = read_list>(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(s, m_export_decl.m_except_names); + write_list>(s, m_export_decl.m_renames); + } + + static std::shared_ptr deserialize(deserializer & d) { + auto m = std::make_shared(); + 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(d, read_name); + e.m_renames = read_list>(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(s, e.m_except_names); - write_list>(s, e.m_renames); - }); + return module::add(new_env, std::make_shared(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 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; } } diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp index e3f21ed5a2..fe5e403dea 100644 --- a/src/library/inductive_compiler/ginductive.cpp +++ b/src/library/inductive_compiler/ginductive.cpp @@ -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 m_all_nested_inds; list 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(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 deserialize(deserializer & d) { + ginductive_entry entry; + d >> entry; + return std::make_shared(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(entry)); } optional is_ginductive(environment const & env, name const & ind_name) { @@ -218,25 +236,13 @@ list 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; } } diff --git a/src/library/inverse.cpp b/src/library/inverse.cpp index f6d37dd829..2616f29658 100644 --- a/src/library/inverse.cpp +++ b/src/library/inverse.cpp @@ -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; } } diff --git a/src/library/module.cpp b/src/library/module.cpp index a6e371ac53..5e877afae3 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -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> writer; - struct module_ext : public environment_extension { list m_direct_imports; - list m_writers; + list> m_modifications; list m_module_univs; list m_module_decls; name_set m_module_defs; @@ -103,7 +101,6 @@ optional get_decl_olean(environment const & env, name const & decl_ return optional(); } -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 deserialize(deserializer & d) { + name decl_name; unsigned line, column; + d >> decl_name >> line >> column; + return std::make_shared(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(decl_name, pos_info {g_curr_line, g_curr_column})); } optional 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>, g_export_delayed_proofs); -class scoped_delayed_proofs { - std::vector> * m_old; -public: - scoped_delayed_proofs(std::vector> & 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 imports; - to_buffer(ext.m_direct_imports, imports); - std::reverse(imports.begin(), imports.end()); - - buffer 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(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> export_module_delayed(std::ostream & out, environment const & env) { - std::vector> 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 object_readers; +typedef std::unordered_map 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 deserialize(deserializer & d) { + return std::make_shared(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 deserialize(deserializer & d) { + return std::make_shared(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 deserialize(deserializer & d) { + return std::make_shared(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 deserialize(deserializer &) { + return std::make_shared(); + } +}; namespace module { -environment add(environment const & env, std::string const & k, std::function const & wr) { +environment add(environment const & env, std::shared_ptr 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 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(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(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(_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()); } 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(cdecl)); } } // end of namespace module @@ -376,28 +440,17 @@ std::pair, std::vector> 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 import_decl(deserializer & d, environment & env, - std::vector> 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(); - } - 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(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 const & olean_code, std::string const & file_name, environment & env, - std::vector> const & delayed_proofs) { - // TODO(gabriel): update extension +modification_list parse_olean_modifications(std::vector 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(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(m.get())) { + env = add_decl_olean(env, dm->m_decl.get_name(), file_name); + } else if (auto im = dynamic_cast(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; } } diff --git a/src/library/module.h b/src/library/module.h index 9608429c1a..ded702f206 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -27,10 +27,13 @@ struct module_name { optional m_relative; }; +struct modification; + +using modification_list = std::vector>; struct loaded_module { std::string m_module_name; - std::string m_obj_code; - std::vector> m_delayed_proofs; + std::vector m_imports; + modification_list m_modifications; }; using module_loader = std::function; module_loader mk_olean_loader(); @@ -66,25 +69,36 @@ optional 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> 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> parse_olean( std::istream & in, std::string const & file_name, bool check_hash = true); -void import_module(std::vector const & olean_code, std::string const & file_name, environment & env, - std::vector> const & delayed_proofs); +modification_list parse_olean_modifications(std::vector 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(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 const & writer); +environment add(environment const & env, std::shared_ptr const & modif); +environment add_and_perform(environment const & env, std::shared_ptr 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); diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 31901dd27d..d8a2e57db8 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -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(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(); @@ -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); diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index 0feccbefe0..7b4647fc86 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -42,8 +42,7 @@ struct module_info { options m_opts; bool m_ok = false; - std::string m_obj_code; - std::vector> m_obj_code_delayed_proofs; + loaded_module m_loaded_module; snapshot_vector m_snapshots; }; diff --git a/src/library/native_compiler/native_compiler.cpp b/src/library/native_compiler/native_compiler.cpp index 7891da0e5e..ee2a75403f 100644 --- a/src/library/native_compiler/native_compiler.cpp +++ b/src/library/native_compiler/native_compiler.cpp @@ -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 deserialize(deserializer & d) { + return std::make_shared(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(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(); } } diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 25ffca417a..0cb70ffd7b 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -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(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 deserialize(deserializer & d) { + return std::make_shared(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(n)); } optional 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; } } diff --git a/src/library/private.cpp b/src/library/private.cpp index f44f0b6e64..1733547772 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -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 deserialize(deserializer & d) { + name n, h; + d >> n >> h; + return std::make_shared(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(n, r)); } pair add_private_name(environment const & env, name const & n, optional const & extra_hash) { @@ -56,16 +82,6 @@ pair 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 hidden_to_user_name(environment const & env, name const & n) { auto it = get_extension(env).m_inv_map.find(n); return it ? optional(*it) : optional(); @@ -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; } diff --git a/src/library/projection.cpp b/src/library/projection.cpp index bb9f35e205..d4e9ffcc1b 100644 --- a/src/library/projection.cpp +++ b/src/library/projection.cpp @@ -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(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 deserialize(deserializer & d) { + name p, mk; unsigned nparams, i; bool inst_implicit; + d >> p >> mk >> nparams >> i >> inst_implicit; + return std::make_shared(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( + 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 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; } } diff --git a/src/library/protected.cpp b/src/library/protected.cpp index 201a3e0a12..8b7e58711f 100644 --- a/src/library/protected.cpp +++ b/src/library/protected.cpp @@ -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(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 deserialize(deserializer & d) { + return std::make_shared(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(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; } } diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index 46d62c0853..c19eb10461 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -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(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; } } diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index 074a3ee2fc..1d48b59c39 100644 --- a/src/library/scoped_ext.cpp +++ b/src/library/scoped_ext.cpp @@ -77,14 +77,37 @@ optional to_valid_namespace_name(environment const & env, name const & n) return optional(); } -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 deserialize(deserializer & d) { + name n; + d >> n; + return std::make_shared(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(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_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; } diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 8a05e05047..3fa528bc92 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -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 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 deserialize(deserializer & d) { + return std::make_shared(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()); } + ~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(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; } diff --git a/src/library/tactic/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp index 5f09f9dad7..a5b67ac9b9 100644 --- a/src/library/tactic/eqn_lemmas.cpp +++ b/src/library/tactic/eqn_lemmas.cpp @@ -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(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 deserialize(deserializer & d) { + return std::make_shared(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_lemma)); } void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer & 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; } } diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp index 2823be6e2a..e55bb7a3b7 100644 --- a/src/library/tactic/kabstract.cpp +++ b/src/library/tactic/kabstract.cpp @@ -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(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 deserialize(deserializer & d) { + name n1, n2; + d >> n1 >> n2; + return std::make_shared(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(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> 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; } } diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index 10c050e6f3..f8719dd2c0 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/src/library/tactic/user_attribute.cpp @@ -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 deserialize(deserializer & d) { + return std::make_shared(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(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(new actual_user_attribute_ext)); } void finalize_user_attribute() { - delete g_key; + user_attr_modification::finalize(); delete g_ext; } } diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp index 22c938a53b..5bf46dcce6 100644 --- a/src/library/unification_hint.cpp +++ b/src/library/unification_hint.cpp @@ -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 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; } } diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 84e2598501..3be2b6593e 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -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; } } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index e63ce414bb..65b0386f45 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -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 const & args_info, optional const & pos, - optional const & olean = optional()) { - 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 get_vm_builtin_idx(name const & n) { return optional(); } -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 deserialize(deserializer & d) { + name fn; expr e; + d >> fn >> e; + return std::make_shared(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 deserialize(deserializer & d) { + name fn; unsigned code_sz; expr e; optional pos; + d >> fn >> e >> code_sz >> pos; + auto args_info = read_list(d); + buffer code; + for (unsigned i = 0; i < code_sz; i++) + code.emplace_back(read_vm_instr(d)); + optional file_name; // TODO(gabriel) + return std::make_shared( + 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 deserialize(deserializer & d) { + auto m = std::make_shared(); + 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 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 args_info; optional pos; - d >> fn >> code_sz >> pos; - args_info = read_list(d); - vm_decls ext = get_extension(env); - buffer 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(fn, e)); } environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, list const & args_info, optional 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(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(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 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;