From da4c1922e372b602ffabe78c137b5b4251f017dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Jul 2014 19:15:46 -0700
Subject: [PATCH] feat(frontends/lean): add '_root_' prefix for referencing
 names in the root namespace

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_cmds.cpp |  6 ++++--
 src/frontends/lean/parser.cpp       |  6 ++++--
 src/frontends/lean/util.cpp         |  7 +++++++
 src/frontends/lean/util.h           |  2 ++
 tests/lean/run/root.lean            | 20 ++++++++++++++++++++
 tests/lean/t3.lean.expected.out     |  2 +-
 6 files changed, 38 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/root.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 0ffb72371..f09b78649 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -65,8 +65,10 @@ environment section_cmd(parser & p) {
 }
 
 environment namespace_cmd(parser & p) {
-    name n = p.check_id_next("invalid namespace declaration, identifier expected");
-    check_atomic(n);
+    auto pos = p.pos();
+    name n = p.check_atomic_id_next("invalid namespace declaration, atomic identifier expected");
+    if (is_root_namespace(n))
+        throw parser_error(sstream() << "invalid namespace name, '" << n << "' is reserved", pos);
     return push_scope(p.env(), p.ios(), n);
 }
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 270a13ce6..2ec77d526 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
 #include "frontends/lean/parser_bindings.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/elaborator.h"
@@ -823,8 +824,9 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
             throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
         return *r;
     } else {
-        if (m_env.find(id)) {
-            return save_pos(mk_constant(id, ls), p);
+        name new_id = remove_root_prefix(id);
+        if (m_env.find(new_id)) {
+            return save_pos(mk_constant(new_id, ls), p);
         } else {
             for (name const & ns : get_namespaces(m_env)) {
                 auto new_id = ns + id;
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index ff1853b7b..29b212dfb 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -18,4 +18,11 @@ void check_in_section(parser const & p) {
     if (!in_section(p.env()))
         throw exception(sstream() << "invalid command, it must be used in a section");
 }
+static name g_root("_root_");
+bool is_root_namespace(name const & n) {
+    return n == g_root;
+}
+name remove_root_prefix(name const & n) {
+    return n.replace_prefix(g_root, name());
+}
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index d116cb73a..440f00d23 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -10,4 +10,6 @@ namespace lean {
 class parser;
 void check_atomic(name const & n);
 void check_in_section(parser const & p);
+bool is_root_namespace(name const & n);
+name remove_root_prefix(name const & n);
 }
diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean
new file mode 100644
index 000000000..6a033dd51
--- /dev/null
+++ b/tests/lean/run/root.lean
@@ -0,0 +1,20 @@
+import standard
+using num
+
+variable foo : Bool
+
+namespace N1
+  variable foo : Bool
+  check N1.foo
+  check _root_.foo
+  namespace N2
+    variable foo : Bool
+    check N1.foo
+    check N1.N2.foo
+    print raw foo
+    print raw _root_.foo
+  end
+end
+
+
+
diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out
index 0504d47d8..97aea5de3 100644
--- a/tests/lean/t3.lean.expected.out
+++ b/tests/lean/t3.lean.expected.out
@@ -9,7 +9,7 @@ t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declar
 Type.{tst.v}
 Type.{u}
 Type.{tst.foo.U}
-t3.lean:26:0: error: invalid declaration name 'tst.foo', identifier must be atomic
+t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected
 t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic
 Type.{tst.v}
 Type.{tst.foo.U}