feat(library): add module system API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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 <unordered_map>
+#include <utility>
+#include <string>
+#include "util/hash.h"
+#include "library/module.h"
+#include "library/kernel_serializer.h"
+
+namespace lean {
+typedef std::pair<std::string, std::function<void(serializer &)>> writer;
+typedef std::pair<std::string, unsigned> import_info; // imported module and its hashcode
+
+struct module_ext : public environment_extension {
+    list<import_info> m_direct_imports;
+    list<writer> m_writers;
+};
+
+struct module_ext_reg {
+    unsigned m_ext_id;
+    module_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<module_ext>()); }
+};
+
+static module_ext_reg g_ext;
+static module_ext const & get_extension(environment const & env) {
+    return static_cast<module_ext const &>(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<module_ext>(ext));
+}
+
+void export_module(std::ostream & out, environment const & env) {
+    module_ext const & ext = get_extension(env);
+    buffer<import_info> imports;
+    buffer<writer const *> 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<std::string, module_object_reader> object_readers;
+static std::unique_ptr<object_readers> 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<void(serializer &)> const & wr) {
+    module_ext ext = get_extension(env);
+    ext.m_writers  = list<writer>(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);
+}
+}

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 <string>
+#include <iostream>
+#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<environment(environment const & env)> 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<void(update_env_fn const &)> & 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<void(serializer &)> 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);
+}