From a2bc967fac3113ffcfa60a6bb6f4852d7d00a70b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 19 Dec 2016 15:42:11 -0500 Subject: [PATCH] feat(library/module): reuse pre-imported init module --- src/library/module.cpp | 33 ++++++++++++++++------ src/library/module.h | 9 +++++- src/library/module_mgr.cpp | 17 ++++++++--- src/library/module_mgr.h | 2 +- src/util/lazy_value.h | 58 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 105 insertions(+), 14 deletions(-) create mode 100644 src/util/lazy_value.h diff --git a/src/library/module.cpp b/src/library/module.cpp index 5e877afae3..42f31c502a 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -443,24 +443,41 @@ std::pair, std::vector> parse_olean(std::istream 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; - for (auto & dep : res.m_imports) { - import_module(env, res.m_module_name, dep, mod_ldr); + + auto & ext0 = get_extension(env); + if (ext0.m_imported.contains(res->m_module_name)) return; + + if (ext0.m_imported.empty() && res->m_env) { + env = *res->m_env; + } else { + for (auto & dep : res->m_imports) { + import_module(env, res->m_module_name, dep, mod_ldr); + } + import_module(res->m_modifications, res->m_module_name, env); } + auto ext = get_extension(env); - ext.m_imported.insert(res.m_module_name); + ext.m_imported.insert(res->m_module_name); env = update(env, ext); - import_module(res.m_modifications, res.m_module_name, env); } environment import_module(environment const & env0, std::string const & module_file_name, module_name const & ref, module_loader const & mod_ldr) { environment env = env0; + import_module(env, module_file_name, ref, mod_ldr); module_ext ext = get_extension(env); ext.m_direct_imports = cons(ref, ext.m_direct_imports); env = update(env, ext); - import_module(env, module_file_name, ref, mod_ldr); + return env; +} + +environment mk_preimported_module(environment const & initial_env, loaded_module const & lm, module_loader const & mod_ldr) { + auto env = initial_env; + for (auto & dep : lm.m_imports) { + import_module(env, lm.m_module_name, dep, mod_ldr); + } + import_module(lm.m_modifications, lm.m_module_name, env); return env; } @@ -509,12 +526,12 @@ module_loader mk_olean_loader() { 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 }; + return std::make_shared(loaded_module { fn, parsed.first, modifs, {} }); }; } module_loader mk_dummy_loader() { - return[=] (std::string const &, module_name const &) -> loaded_module { + return[=] (std::string const &, module_name const &) -> std::shared_ptr { throw exception("module importing disabled"); }; } diff --git a/src/library/module.h b/src/library/module.h index ded702f206..3115088d2a 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/io_state.h" #include "util/task_queue.h" +#include "util/lazy_value.h" namespace lean { class corrupted_file_exception : public exception { @@ -34,8 +35,10 @@ struct loaded_module { std::string m_module_name; std::vector m_imports; modification_list m_modifications; + + lazy_value m_env; }; -using module_loader = std::function; +using module_loader = std::function (std::string const &, module_name const &)>; module_loader mk_olean_loader(); module_loader mk_dummy_loader(); @@ -58,6 +61,10 @@ import_module(environment const & env, std::string const & current_mod, module_name const & ref, module_loader const & mod_ldr); +environment mk_preimported_module(environment const & initial_env, + loaded_module const & lm, + module_loader const & mod_ldr); + /** \brief Return the .olean file where decl_name was defined. The result is none if the declaration was not defined in an imported file. */ optional get_decl_olean(environment const & env, name const & decl_name); diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index d8a2e57db8..57228fd1fc 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -59,8 +59,9 @@ public: } module_info::parse_result execute() override { + auto deps = std::move(m_deps); module_loader import_fn = [=] (module_id const & base, module_name const & import) { - for (auto & d : m_deps) { + for (auto & d : deps) { if (std::get<0>(d) == base && std::get<1>(d).m_name == import.m_name && std::get<1>(d).m_relative == import.m_relative) { @@ -83,7 +84,13 @@ public: mod.m_snapshots = std::move(m_snapshots); - mod.m_loaded_module = export_module(p.env(), get_module_id()); + auto lm = std::make_shared(export_module(p.env(), get_module_id())); + std::weak_ptr weak_lm = lm; + auto initial_env = m_initial_env; + lm->m_env = lazy_value([initial_env, weak_lm, import_fn] { + return mk_preimported_module(initial_env, *weak_lm.lock(), import_fn); + }); + mod.m_loaded_module = lm; mod.m_env = optional(p.env()); @@ -128,7 +135,7 @@ public: 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); - write_module(res.m_loaded_module, out); + write_module(*res.m_loaded_module, out); return {}; } }; @@ -193,7 +200,9 @@ 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_loaded_module = { id, parsed_olean.first, parse_olean_modifications(parsed_olean.second, id) }; + // TODO(gabriel) + res.m_loaded_module = std::make_shared( + 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 7b4647fc86..936e0f6729 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -42,7 +42,7 @@ struct module_info { options m_opts; bool m_ok = false; - loaded_module m_loaded_module; + std::shared_ptr m_loaded_module; snapshot_vector m_snapshots; }; diff --git a/src/util/lazy_value.h b/src/util/lazy_value.h new file mode 100644 index 0000000000..2041e0c1e4 --- /dev/null +++ b/src/util/lazy_value.h @@ -0,0 +1,58 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#pragma once +#include "util/thread.h" +#include + +namespace lean { + +template +class lazy_value { + bool m_nonempty = false; + mutex m_mutex; + optional m_value; + std::exception_ptr m_ex; + std::function m_closure; + + T const & get() { + lean_assert(m_nonempty); + unique_lock _(m_mutex); + if (m_value) return *m_value; + if (m_ex) std::rethrow_exception(m_ex); + try { + m_value = { m_closure() }; + m_closure = {}; + return *m_value; + } catch (...) { + m_ex = std::current_exception(); + m_closure = {}; + throw; + } + } + +public: + lazy_value() {} + lazy_value(std::function && closure) : m_nonempty(true), m_closure(closure) {} + lazy_value(lazy_value const & other) { *this = other; } + + lazy_value & operator=(lazy_value const & other) { + unique_lock _(const_cast(other).m_mutex); + m_nonempty = other.m_nonempty; + m_value = other.m_value; + m_ex = other.m_ex; + m_closure = other.m_closure; + return *this; + } + + operator bool() const { return m_nonempty; } + + T const & operator*() const { + return const_cast(this)->get(); + } +}; + +}