refactor(library): add module namespace

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

src/library/coercion.cpp

@@ -286,7 +286,7 @@ struct add_coercion_fn {
         add_coercion(C, f, f_type, ls, num_args, cls);
         m_ext.update_from_to(C, cls, m_ios);
         name const & f_name = const_name(f);
-        m_env = add(m_env, g_coercion_key, [=](serializer & s) {
+        m_env = module::add(m_env, g_coercion_key, [=](serializer & s) {
                 s << f_name << C;
             });
         return update(m_env, m_ext);

src/library/kernel_bindings.cpp

@@ -1859,7 +1859,7 @@ static int add_declaration(lua_State * L) {
         d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
     else
         d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
-    return push_environment(L, add(to_environment(L, 1), *d));
+    return push_environment(L, module::add(to_environment(L, 1), *d));
 }
 
 static void open_type_checker(lua_State * L) {
@@ -1903,7 +1903,7 @@ static int add_inductive1(lua_State * L) {
     buffer<intro_rule> irules;
     for (int i = idx+1; i <= nargs; i+=2)
         irules.push_back(intro_rule(to_name_ext(L, i), to_expr(L, i+1)));
-    return push_environment(L, add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end())));
+    return push_environment(L, module::add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end())));
 }
 static int add_inductivek(lua_State * L) {
     environment env      = to_environment(L, 1);
@@ -1935,7 +1935,7 @@ static int add_inductivek(lua_State * L) {
     }
     if (decls.empty())
         throw exception("invalid add_inductive, at least one inductive type must be defined");
-    return push_environment(L, ::lean::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end())));
+    return push_environment(L, module::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end())));
 }
 static int add_inductive(lua_State * L) {
     if (is_name(L, 2) || lua_isstring(L, 2))

src/library/module.cpp

@@ -99,14 +99,15 @@ void register_module_object_reader(std::string const & k, module_object_reader r
     readers[k] = r;
 }
 
+static std::string g_decl("decl");
+
+namespace module {
 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);
     declaration _d = d.get_declaration();
@@ -145,6 +146,7 @@ static void inductive_reader(deserializer & d, module_idx, shared_environment &
 }
 
 static register_module_object_reader_fn g_reg_ind_reader(g_inductive, inductive_reader);
+} // end of namespace module
 
 struct import_modules_fn {
     typedef std::tuple<module_idx, unsigned, delayed_update_fn> delayed_update;

src/library/module.h

@@ -65,6 +65,7 @@ struct register_module_object_reader_fn {
     }
 };
 
+namespace module {
 /**
     \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
@@ -96,3 +97,4 @@ environment add_inductive(environment const &        env,
                           expr const &               type,             // type of the form: params -> indices -> Type
                           list<inductive::intro_rule> const & intro_rules);     // introduction rules
 }
+}