From df008dc3c35bea4f91a29dbe978cd20ec8c1356a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 1 Nov 2014 19:15:46 -0700
Subject: [PATCH] feat(frontends/lean/inductive_cmd): create a namespace for
 each declared datatype

---
 src/frontends/lean/inductive_cmd.cpp |  9 +++++++++
 src/library/scoped_ext.cpp           | 12 ++++++++++++
 src/library/scoped_ext.h             |  3 +++
 tests/lean/run/ind_ns.lean           |  6 ++++++
 4 files changed, 30 insertions(+)
 create mode 100644 tests/lean/run/ind_ns.lean

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index e20d2cf3c..196558d93 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/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);
     }
 };
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 600aa2ab3..992ea8a39 100644
--- a/src/library/scoped_ext.cpp
+++ b/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");
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index a32d34d8c..9ca1a9acd 100644
--- a/src/library/scoped_ext.h
+++ b/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);
diff --git a/tests/lean/run/ind_ns.lean b/tests/lean/run/ind_ns.lean
new file mode 100644
index 000000000..d1aa1734f
--- /dev/null
+++ b/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