feat(library/module): add declaration reader

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

src/library/module.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <string>
 #include "util/hash.h"
+#include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/kernel_serializer.h"
 
@@ -87,6 +88,30 @@ environment add(environment const & env, std::string const & k, std::function<vo
 
 static std::string g_decl("decl");
 
+static void declaration_reader(deserializer & d, module_idx midx, shared_environment & senv,
+                               std::function<void(asynch_update_fn const &)> & add_asynch_update,
+                               std::function<void(delayed_update_fn const &)> &) {
+    declaration decl = read_declaration(d, midx);
+    environment env  = senv.env();
+    if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
+        senv.add(decl);
+    } else if (decl.is_theorem()) {
+        // First, we add the theorem as an axiom, and create an asychronous task for
+        // checking the actual theorem, and replace the axiom with the actual theorem.
+        certified_declaration tmp_c = check(env, mk_axiom(decl.get_name(), decl.get_params(), decl.get_type()));
+        senv.add(tmp_c);
+        add_asynch_update([=](shared_environment & senv) {
+                certified_declaration c = check(env, decl);
+                senv.replace(c);
+            });
+    } else {
+        certified_declaration c = check(env, decl);
+        senv.add(c);
+    }
+}
+
+static register_module_object_reader_fn g_reg_decl_reader(g_decl, declaration_reader);
+
 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(); });

src/library/module.h

@@ -24,20 +24,27 @@ environment import_module(environment const & env, std::string const & module);
 */
 void export_module(std::ostream & out, environment const & env);
 
-typedef std::function<environment(environment const & env)> update_env_fn;
+/** \brief An asynchronous update. It goes into a task queue, and can be executed by a different execution thread. */
+typedef std::function<void(shared_environment & env)> asynch_update_fn;
+
+/** \brief Delayed update. It is performed after all imported modules have been loaded.
+    The delayes updates are executed based on the import order.
+    Example: if module A was imported before B, then delayed updates from A
+    are executed before the ones from B.
+*/
+typedef std::function<environment(environment const & env)> delayed_update_fn;
+
 
 /**
    \brief A reader for importing data from a stream using deserializer \c d.
-   There are two way to update the environment being constructed.
+   There are three ways to update the environment being constructed.
-   We can directly update it using \c senv, or we may register a delayed
+     1- Direct update it using \c senv.
-   update using \c delayed_update. The delayed updates are executed using
+     2- Asynchronous update using add_asynch_update.
-   an order based on import order. The delayed updates are useful for
+     3- Delayed update using add_delayed_update.
-   objects such as rewrite rule sets where the order in which they are
-   constructed matter.
 */
-typedef void (*module_object_reader)(deserializer & d,
+typedef void (*module_object_reader)(deserializer & d, module_idx midx, shared_environment & senv,
-                                     shared_environment & senv,
+                                     std::function<void(asynch_update_fn const &)> & add_asynch_update,
-                                     std::function<void(update_env_fn const &)> & delayed_update);
+                                     std::function<void(delayed_update_fn const &)> & add_delayed_update);
 
 /**
    \brief Register a module object reader. The key \c k is used to identify the class of objects

src/library/shared_environment.cpp

@@ -20,6 +20,11 @@ void shared_environment::add(certified_declaration const & d) {
     m_env = m_env.add(d);
 }
 
+void shared_environment::add(declaration const & d) {
+    exclusive_lock l(m_mutex);
+    m_env = m_env.add(d);
+}
+
 void shared_environment::replace(certified_declaration const & t) {
     exclusive_lock l(m_mutex);
     m_env = m_env.replace(t);

src/library/shared_environment.h

@@ -19,12 +19,19 @@ public:
     shared_environment(environment const & env);
     /** \brief Return a copy of the current environment. This is a constant time operation. */
     environment get_environment() const;
+    environment env() const { return get_environment(); }
     /**
         \brief Add the given certified declaration to the environment.
         This is a constant time operation.
         It blocks this object for a small amount of time.
     */
     void add(certified_declaration const & d);
+    /**
+        \brief Add declaration that was not type checked.
+        The method throws an exception if trust_level() <= LEAN_BELIEVER_TRUST_LEVEL
+        It blocks this object for a small amount of time.
+    */
+    void add(declaration const & d);
     /**
         \brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
         This is a constant time operation.