feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype

src/frontends/lean/inductive_cmd.cpp

@@ -682,6 +682,14 @@ struct inductive_cmd_fn {
         return env;
     }
 
+    /** \brief Add a namespace for each inductive datatype */
+    environment add_namespaces(environment env, buffer<inductive_decl> const & decls) {
+        for (inductive_decl const & d : decls) {
+            env = add_namespace(env, inductive_decl_name(d));
+        }
+        return env;
+    }
+
     /** \brief Auxiliary method used for debugging */
     void display(std::ostream & out, buffer<inductive_decl> const & decls) {
         if (!m_levels.empty()) {
@@ -718,6 +726,7 @@ struct inductive_cmd_fn {
         env = mk_aux_decls(env, decls);
         update_declaration_index(env);
         env = add_aliases(env, ls, locals, decls);
+        env = add_namespaces(env, decls);
         return apply_modifiers(env);
     }
 };

src/library/scoped_ext.cpp

@@ -95,6 +95,18 @@ optional<name> to_valid_namespace_name(environment const & env, name const & n)
 }
 
 static std::string * g_new_namespace_key = nullptr;
+
+environment add_namespace(environment const & env, name const & ns) {
+    scope_mng_ext ext = get_extension(env);
+    if (!ext.m_namespace_set.contains(ns)) {
+        ext.m_namespace_set.insert(ns);
+        environment r = update(env, ext);
+        return module::add(r, *g_new_namespace_key, [=](serializer & s) { s << ns; });
+    } else {
+        return env;
+    }
+}
+
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
     if (k == scope_kind::Namespace && in_section_or_context(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");

src/library/scoped_ext.h

@@ -35,6 +35,9 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
 environment pop_scope(environment const & env, name const & n = name());
 bool has_open_scopes(environment const & env);
 
+/** \brief Add a new namespace (if it does not exist) */
+environment add_namespace(environment const & env, name const & ns);
+
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);
 bool in_context(environment const & env);

tests/lean/run/ind_ns.lean

@@ -0,0 +1,6 @@
+inductive day :=
+monday, tuesday, wednesday, thursday, friday, saturday, sunday
+
+check day.monday
+open day
+check monday