From e69b508492f6ec69b9f45ba9c548da8b2cb4e5ac Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 17 Jul 2016 00:02:11 -0400 Subject: [PATCH] refactor(library/export_decl): Re-implement for new scoped_ext Use environment_extension to persist mapping from namespaces to export decls, use new scoped_ext to keep track of currently active export decls. --- src/frontends/lean/builtin_cmds.cpp | 8 +- src/frontends/lean/parser.cpp | 2 + src/library/export_decl.cpp | 122 +++++++++++++++++++++------- src/library/export_decl.h | 5 +- 4 files changed, 102 insertions(+), 35 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index e849cfec80..58ed1cea30 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -65,7 +65,7 @@ environment section_cmd(parser & p) { environment execute_open(environment env, io_state const & ios, export_decl const & edecl); environment replay_export_decls_core(environment env, io_state const & ios, unsigned old_sz) { - list new_export_decls = get_export_decls(env); + list new_export_decls = get_active_export_decls(env); unsigned new_sz = length(new_export_decls); lean_assert(new_sz >= old_sz); unsigned i = 0; @@ -86,7 +86,8 @@ environment execute_open(environment env, io_state const & ios, export_decl cons unsigned fingerprint = 0; name const & ns = edecl.m_ns; fingerprint = hash(fingerprint, ns.hash()); - unsigned old_export_decls_sz = length(get_export_decls(env)); + unsigned old_export_decls_sz = length(get_active_export_decls(env)); + env = activate_export_decls(env, ns); for (auto const & p : edecl.m_renames) { fingerprint = hash(hash(fingerprint, p.first.hash()), p.second.hash()); env = add_expr_alias(env, p.first, p.second); @@ -106,8 +107,9 @@ environment execute_open(environment env, io_state const & ios, export_decl cons environment namespace_cmd(parser & p) { name n = p.check_decl_id_next("invalid namespace declaration, identifier expected"); p.push_local_scope(); - unsigned old_export_decls_sz = length(get_export_decls(p.env())); + unsigned old_export_decls_sz = length(get_active_export_decls(p.env())); environment env = push_scope(p.env(), p.ios(), scope_kind::Namespace, n); + env = activate_export_decls(env, get_namespace(env)); return replay_export_decls_core(env, p.ios(), old_export_decls_sz); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index e3ec4c7174..e74f7cc83d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/interrupt.h" #include "util/sstream.h" #include "util/flet.h" @@ -1965,6 +1966,7 @@ void parser::parse_imports() { m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads, keep_imported_thms, m_ios); m_env = update_fingerprint(m_env, fingerprint); + m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace m_env = replay_export_decls_core(m_env, m_ios); if (imported) commit_info(1, 0); diff --git a/src/library/export_decl.cpp b/src/library/export_decl.cpp index 08d18c1284..b075d6bf21 100644 --- a/src/library/export_decl.cpp +++ b/src/library/export_decl.cpp @@ -10,7 +10,8 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" namespace lean { -static std::string * g_key = nullptr; +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; @@ -40,7 +41,65 @@ bool operator!=(export_decl const & d1, export_decl const & d2) { return !(d1 == d2); } -struct export_decl_config { +struct export_decl_env_ext : public environment_extension { + name_map> m_ns_map; + + export_decl_env_ext() {} + export_decl_env_ext(name_map> const & ns_map): m_ns_map(ns_map) {} +}; + +/** \brief Auxiliary object for registering the environment extension */ +struct export_decl_env_ext_reg { + unsigned m_ext_id; + export_decl_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static export_decl_env_ext_reg * g_ext = nullptr; + +/** \brief Retrieve environment extension */ +static export_decl_env_ext const & get_export_decl_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} + +/** \brief Update environment extension */ +static environment update(environment const & env, export_decl_env_ext const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + +static void read_export_decls(deserializer & d, shared_environment &, + std::function &, + std::function & add_delayed_update) { + 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); + add_delayed_update([=](environment const & env, io_state const &) -> environment { + return add_export_decl(env, in_ns, e); + }); +} + +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; + list decls; + if (ns_map.contains(in_ns)) + decls = *ns_map.find(in_ns); + + if (std::find(decls.begin(), decls.end(), e) != decls.end()) + 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); + }); +} +environment add_export_decl(environment const & env, export_decl const & entry) { + return add_export_decl(env, get_namespace(env), entry); +} + +struct active_export_decls_config { typedef export_decl entry; typedef list state; @@ -49,48 +108,49 @@ struct export_decl_config { s = cons(e, s); } } - - static std::string const & get_serialization_key() { - return *g_key; - } - - static void write_entry(serializer & s, entry const & e) { - s << e.m_ns << e.m_as << e.m_had_explicit; - write_list(s, e.m_except_names); - write_list>(s, e.m_renames); - } - - static entry read_entry(deserializer & d) { - entry e; - d >> 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 e; - } static optional get_fingerprint(entry const &) { return optional(); } + + // uses local scope only + static std::string const & get_serialization_key() { return *g_active_export_decls_key; } + static void write_entry(serializer &, entry const &) { lean_unreachable(); } + static entry read_entry(deserializer &) { lean_unreachable(); } }; -template class scoped_ext; -typedef scoped_ext export_decl_ext; +template class scoped_ext; +typedef scoped_ext active_export_decls_ext; -environment add_export_decl(environment const & env, export_decl const & entry) { - bool persistent = true; - return export_decl_ext::add_entry(env, get_dummy_ios(), entry, persistent); +environment activate_export_decls(environment env, name ns) { + auto ns_map = get_export_decl_extension(env).m_ns_map; + while (true) { + if (ns_map.contains(ns)) { + for (auto const & e : *ns_map.find(ns)) + env = active_export_decls_ext::add_entry(env, get_dummy_ios(), e, false); + } + if (ns.is_anonymous()) + break; + ns = ns.get_prefix(); + } + return env; } -list get_export_decls(environment const & env) { - return export_decl_ext::get_state(env); +list get_active_export_decls(environment const & env) { + return active_export_decls_ext::get_state(env); } void initialize_export_decl() { - g_key = new std::string("export_decl"); - export_decl_ext::initialize(); + 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); + active_export_decls_ext::initialize(); } void finalize_export_decl() { - delete g_key; - export_decl_ext::finalize(); + active_export_decls_ext::finalize(); + delete g_active_export_decls_key; + delete g_export_decl_key; + delete g_ext; } } diff --git a/src/library/export_decl.h b/src/library/export_decl.h index 8d93f67e05..4e244ef7dc 100644 --- a/src/library/export_decl.h +++ b/src/library/export_decl.h @@ -23,8 +23,11 @@ struct export_decl { }; /** \brief We store export commands to allow us to replay them whenever the namespace is opened. */ +environment add_export_decl(environment const & env, name const & in_ns, export_decl const & e); environment add_export_decl(environment const & env, export_decl const & entry); -list get_export_decls(environment const & env); + +environment activate_export_decls(environment, name); +list get_active_export_decls(environment const & env); void initialize_export_decl(); void finalize_export_decl();