From 0b8f57841afc34796735c3874c09abfbcabcbd4b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Aug 2015 17:50:44 -0700
Subject: [PATCH] feat(frontends/lean/decl_cmds): closes #791

---
 src/frontends/lean/decl_cmds.cpp | 11 ++++++++++-
 src/library/scoped_ext.cpp       |  6 +++++-
 tests/lean/run/791.lean          | 15 +++++++++++++++
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/791.lean

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 69363c1cb..41b138193 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -114,6 +114,12 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
         });
 }
 
+static environment ensure_decl_namespaces(environment const & env, name const & full_n) {
+    if (full_n.is_atomic())
+        return env;
+    return add_namespace(env, full_n.get_prefix());
+}
+
 static environment declare_var(parser & p, environment env,
                                name const & n, level_param_names const & ls, expr const & type,
                                variable_kind k, optional<binder_info> const & _bi, pos_info const & pos,
@@ -155,6 +161,7 @@ static environment declare_var(parser & p, environment env,
         }
         if (is_protected)
             env = add_protected(env, full_n);
+        env = ensure_decl_namespaces(env, full_n);
         return env;
     }
 }
@@ -885,8 +892,10 @@ class definition_cmd_fn {
                 }
             }
             // TODO(Leo): register aux_decls
-            if (!m_is_private)
+            if (!m_is_private) {
                 m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
+                m_env = ensure_decl_namespaces(m_env, real_n);
+            }
             if (m_is_protected)
                 m_env = add_protected(m_env, real_n);
             if (n != real_n) {
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index f463ab089..f73c9014f 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -127,7 +127,11 @@ environment add_namespace(environment const & env, name const & ns) {
     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, [=](environment const &, serializer & s) { s << ns; });
+        r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
+        if (ns.is_atomic())
+            return r;
+        else
+            return add_namespace(r, ns.get_prefix());
     } else {
         return env;
     }
diff --git a/tests/lean/run/791.lean b/tests/lean/run/791.lean
new file mode 100644
index 000000000..d29879df6
--- /dev/null
+++ b/tests/lean/run/791.lean
@@ -0,0 +1,15 @@
+definition foo.bar := 10
+definition boo.bla.foo := 20
+
+open foo
+open boo.bla
+
+eval bar
+eval foo
+
+constant x.y.z : nat
+
+open x
+check y.z
+open x.y
+check z