From 570879b55f17efd7a41f12148760faf3f8d14093 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 17:59:40 -0700
Subject: [PATCH] feat(frontends/lean): add declaration to namespace without
 opening it, closes #161

---
 src/frontends/lean/decl_cmds.cpp     |  4 ----
 src/frontends/lean/inductive_cmd.cpp |  2 +-
 tests/lean/run/ns2.lean              | 29 ++++++++++++++++++++++++++++
 tests/lean/t3.lean.expected.out      |  1 -
 4 files changed, 30 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/ns2.lean

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index b2258ed17..739170248 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -33,7 +33,6 @@ static name g_coercion("[coercion]");
 
 environment universe_cmd(parser & p) {
     name n = p.check_id_next("invalid universe declaration, identifier expected");
-    check_atomic(n);
     environment env = p.env();
     if (in_section_or_context(env)) {
         p.add_local_level(n, mk_param_univ(n));
@@ -119,7 +118,6 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
     auto pos = p.pos();
     optional<binder_info> bi = parse_binder_info(p);
     name n = p.check_id_next("invalid declaration, identifier expected");
-    check_atomic(n);
     buffer<name> ls_buffer;
     if (p.curr_is_token(g_llevel_curly) && in_section_or_context(p.env()))
         throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
@@ -211,7 +209,6 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
     name n     = p.check_id_next("invalid declaration, identifier expected");
-    check_atomic(n);
     decl_modifiers modifiers;
     name real_n; // real name for this declaration
     modifiers.m_is_opaque = _is_opaque;
@@ -382,7 +379,6 @@ static environment variables_cmd(parser & p) {
         buffer<name> ids;
         while (!p.curr_is_token(g_colon)) {
             name id = p.check_id_next("invalid parameters declaration, identifier expected");
-            check_atomic(id);
             ids.push_back(id);
         }
         p.next();
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index bdb221faa..7a6d69104 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -121,9 +121,9 @@ struct inductive_cmd_fn {
     name parse_decl_name(optional<name> const & ind_name) {
         m_pos   = m_p.pos();
         name id = m_p.check_id_next("invalid declaration, identifier expected");
-        check_atomic(id);
         if (ind_name) {
             // for intro rules, we append the name of the inductive datatype
+            check_atomic(id);
             name full_id = *ind_name + id;
             m_decl_info.emplace_back(full_id, g_intro, m_pos);
             return full_id;
diff --git a/tests/lean/run/ns2.lean b/tests/lean/run/ns2.lean
new file mode 100644
index 000000000..d080c2021
--- /dev/null
+++ b/tests/lean/run/ns2.lean
@@ -0,0 +1,29 @@
+definition foo.id {A : Type} (a : A) := a
+variable foo.T : Type.{1}
+check foo.id
+check foo.T
+
+inductive foo.v.I := unit : foo.v.I
+
+check foo.v.I
+check foo.v.I.unit
+
+namespace foo
+  check id
+  check T
+  check v.I
+end foo
+
+namespace bla
+  definition vvv.pr {A : Type} (a b : A) := a
+  check vvv.pr
+end bla
+check bla.vvv.pr
+
+namespace bla
+namespace vvv
+  check pr
+  inductive my.empty : Type
+end vvv
+end bla
+check bla.vvv.my.empty
diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out
index 2a5f01a3f..6432d99de 100644
--- a/tests/lean/t3.lean.expected.out
+++ b/tests/lean/t3.lean.expected.out
@@ -10,7 +10,6 @@ Type
 Type
 Type
 t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected
-t3.lean:27:0: error: invalid declaration name 'full.name.U', identifier must be atomic
 Type
 Type
 t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level