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

@@ -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);
 }
 

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;

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());
+}
 }

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);
 }

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
+
+
+

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}