feat(library/module): export global universe level declarations

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

src/library/kernel_bindings.cpp

@@ -1104,7 +1104,7 @@ static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L,
 static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_proof_irrel()); }
 static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); }
 static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
-static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
+static int environment_add_global_level(lua_State * L) { return push_environment(L, module::add_global_level(to_environment(L, 1), to_name_ext(L, 2))); }
 static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); }
 static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
 static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); }

src/library/module.cpp

@@ -99,7 +99,8 @@ void register_module_object_reader(std::string const & k, module_object_reader r
     readers[k] = r;
 }
 
-static std::string g_decl("decl");
+static std::string g_glvl_key("glvl");
+static std::string g_decl_key("decl");
 
 namespace module {
 environment add(environment const & env, std::string const & k, std::function<void(serializer &)> const & wr) {
@@ -108,15 +109,20 @@ environment add(environment const & env, std::string const & k, std::function<vo
     return update(env, ext);
 }
 
+environment add_global_level(environment const & env, name const & l) {
+    environment new_env = env.add_global_level(l);
+    return add(new_env, g_glvl_key, [=](serializer & s) { s << l; });
+}
+
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
-    return add(new_env, g_decl, [=](serializer & s) { s << _d; });
+    return add(new_env, g_decl_key, [=](serializer & s) { s << _d; });
 }
 
 environment add(environment const & env, declaration const & d) {
     environment new_env = env.add(d);
-    return add(new_env, g_decl, [=](serializer & s) { s << d; });
+    return add(new_env, g_decl_key, [=](serializer & s) { s << d; });
 }
 
 static std::string g_inductive("ind");
@@ -287,6 +293,11 @@ struct import_modules_fn {
         }
     }
 
+    void import_global_level(deserializer & d) {
+        name const l = read_name(d);
+        m_senv.update([=](environment const & env) { return env.add_global_level(l); });
+    }
+
     void import_module(module_info_ptr const & r) {
         std::string s(r->m_obj_code.data(), r->m_obj_code.size());
         std::istringstream in(s, std::ios_base::binary);
@@ -305,8 +316,10 @@ struct import_modules_fn {
             d >> k;
             if (k == g_olean_end_file) {
                 break;
-            } else if (k == g_decl) {
+            } else if (k == g_decl_key) {
                 import_decl(d, r->m_module_idx);
+            } else if (k == g_glvl_key) {
+                import_global_level(d);
             } else {
                 object_readers & readers = get_object_readers();
                 auto it = readers.find(k);

src/library/module.h

@@ -75,6 +75,9 @@ namespace module {
 */
 environment add(environment const & env, std::string const & k, std::function<void(serializer &)> const & writer);
 
+/** \brief Add the global level declaration to the environment, and mark it to be exported. */
+environment add_global_level(environment const & env, name const & l);
+
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
 /**

tests/lua/glvl1.lua

@@ -0,0 +1,9 @@
+local env = environment()
+env = env:add_global_level("u")
+env = env:add_global_level("v")
+assert(env:is_global_level("u"))
+
+env:export("glvl1_mod.olean")
+local env2 = import_modules("glvl1_mod")
+assert(env2:is_global_level("u"))
+assert(env2:is_global_level("v"))