From 8ffe66dc4f23ccad61453a32f827a4e60c0af0c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 May 2014 18:34:15 -0700 Subject: [PATCH] feat(library): add module system API Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/module.cpp | 105 +++++++++++++++++++++++++++++++++++++ src/library/module.h | 66 +++++++++++++++++++++++ 3 files changed, 172 insertions(+), 1 deletion(-) create mode 100644 src/library/module.cpp create mode 100644 src/library/module.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index e7051de89..c97a356f4 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,7 +1,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp - normalize.cpp shared_environment.cpp) + normalize.cpp shared_environment.cpp module.cpp) # placeholder.cpp fo_unify.cpp hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/module.cpp b/src/library/module.cpp new file mode 100644 index 000000000..f52f5b888 --- /dev/null +++ b/src/library/module.cpp @@ -0,0 +1,105 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include +#include "util/hash.h" +#include "library/module.h" +#include "library/kernel_serializer.h" + +namespace lean { +typedef std::pair> writer; +typedef std::pair import_info; // imported module and its hashcode + +struct module_ext : public environment_extension { + list m_direct_imports; + list m_writers; +}; + +struct module_ext_reg { + unsigned m_ext_id; + module_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static module_ext_reg g_ext; +static module_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext.m_ext_id)); +} +static environment update(environment const & env, module_ext const & ext) { + return env.update(g_ext.m_ext_id, std::make_shared(ext)); +} + +void export_module(std::ostream & out, environment const & env) { + module_ext const & ext = get_extension(env); + buffer imports; + buffer writers; + to_buffer(ext.m_direct_imports, imports); + std::reverse(imports.begin(), imports.end()); + for (writer const & w : ext.m_writers) + writers.push_back(&w); + std::reverse(writers.begin(), writers.end()); + + std::string r; + std::ostringstream out1(r); + serializer s1(out1); + + // store imported files + s1 << imports.size(); + for (auto p : imports) + s1 << p.first << p.second; + + // store objects + for (auto p : writers) { + s1 << p->first; + p->second(s1); + } + + serializer s2(out); + unsigned h = hash_str(r.size(), r.c_str(), 13); + s2 << h; + for (unsigned i = 0; i < r.size(); i++) + s2.write_char(r[i]); +} + +typedef std::unordered_map object_readers; +static std::unique_ptr g_object_readers; +static object_readers & get_object_readers() { + if (!g_object_readers) + g_object_readers.reset(new object_readers()); + return *(g_object_readers.get()); +} + +void register_module_object_reader(std::string const & k, module_object_reader r) { + object_readers & readers = get_object_readers(); + lean_assert(readers.find(k) == readers.end()); + readers[k] = r; +} + +environment add(environment const & env, std::string const & k, std::function const & wr) { + module_ext ext = get_extension(env); + ext.m_writers = list(writer(k, wr), ext.m_writers); + return update(env, ext); +} + +static std::string g_decl("decl"); + +environment add(environment const & env, certified_declaration const & d) { + environment new_env = env.add(d); + new_env = add(new_env, g_decl, [=](serializer & s) { s << d.get_declaration(); }); + return new_env; +} + +environment import_modules(environment const & env, unsigned num_modules, std::string const * modules) { + // TODO(Leo) + for (unsigned i = 0; i < num_modules; i++) std::cout << modules[i]; + return env; +} + +environment import_module(environment const & env, std::string const & module) { + return import_modules(env, 1, &module); +} +} diff --git a/src/library/module.h b/src/library/module.h new file mode 100644 index 000000000..d8040e1de --- /dev/null +++ b/src/library/module.h @@ -0,0 +1,66 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "util/serializer.h" +#include "library/shared_environment.h" + +namespace lean { +/** + \brief Return an environment based on \c env, where all modules in \c modules are imported. + Modules included directly or indirectly by them are also imported. + The environment \c env is usually an empty environment. +*/ +environment import_modules(environment const & env, unsigned num_modules, std::string const * modules); +environment import_module(environment const & env, std::string const & module); + +/** + \brief Store/Export module using \c env to the output stream \c out. +*/ +void export_module(std::ostream & out, environment const & env); + +typedef std::function update_env_fn; + +/** + \brief A reader for importing data from a stream using deserializer \c d. + There are two way to update the environment being constructed. + We can directly update it using \c senv, or we may register a delayed + update using \c delayed_update. The delayed updates are executed using + an order based on import order. The delayed updates are useful for + objects such as rewrite rule sets where the order in which they are + constructed matter. +*/ +typedef void (*module_object_reader)(deserializer & d, + shared_environment & senv, + std::function & delayed_update); + +/** + \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); + +/** \brief Auxiliary class for registering module readers when the lean executable is loaded. */ +struct register_module_object_reader_fn { + register_module_object_reader_fn(std::string const & k, module_object_reader r) { + register_module_object_reader(k, r); + } +}; + +/** + \brief Add a function that should be invoked when the environment is exported. + The key \c k identifies which module_object_reader should be used to deserialize the object + when the module is imported. + + \see module_object_reader +*/ +environment add(environment const & env, std::string const & k, std::function const & writer); + +/** \brief Add the given declaration to the environment, and mark it to be exported. */ +environment add(environment const & env, certified_declaration const & d); +}