fix(frontends/lean): uniform handling of declaration compound names

* allow compound names in `namespace` and `structure`
* adjust error messages

src/frontends/lean/builtin_cmds.cpp

@@ -54,10 +54,7 @@ environment section_cmd(parser & p) {
 }
 
 environment namespace_cmd(parser & p) {
-    auto pos = p.pos();
+    name n = p.check_decl_id_next("invalid namespace declaration, identifier expected");
-    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);
     p.push_local_scope();
     return push_scope(p.env(), p.ios(), scope_kind::Namespace, n);
 }
@@ -105,7 +102,7 @@ environment end_scoped_cmd(parser & p) {
     list<pair<name, expr>> entries        = p.get_local_entries();
     p.pop_local_scope();
     if (p.curr_is_identifier()) {
-        name n = p.check_atomic_id_next("invalid end of scope, atomic identifier expected");
+        name n = p.check_id_next("invalid end of scope, identifier expected");
         environment env = pop_scope(p.env(), p.ios(), n);
         return redeclare_aliases(env, p, level_entries, entries);
     } else {

src/frontends/lean/builtin_exprs.cpp

@@ -93,7 +93,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
         return parse_let_body(p, pos);
     } else {
         auto id_pos     = p.pos();
-        name id         = p.check_atomic_id_next("invalid let declaration, identifier expected");
+        name id         = p.check_atomic_id_next("invalid let declaration, atomic identifier expected");
         optional<expr> type;
         expr value;
         if (p.curr_is_token(get_assign_tk())) {

src/frontends/lean/builtin_tactics.cpp

@@ -46,7 +46,7 @@ static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const &
 
 static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
     auto id_pos     = p.pos();
-    name id    = p.check_atomic_id_next("invalid 'let' tactic, identifier expected");
+    name id    = p.check_atomic_id_next("invalid 'let' tactic, atomic identifier expected");
     p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected");
     expr value = p.parse_tactic_expr_arg();
     // Register value as expandable local expr. Identical to let term parsing, but without surrounding mk_let.
@@ -57,7 +57,7 @@ static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const
 }
 
 static expr parse_note_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
-    name id    = p.check_atomic_id_next("invalid 'note' tactic, identifier expected");
+    name id    = p.check_atomic_id_next("invalid 'note' tactic, atomic identifier expected");
     p.check_token_next(get_assign_tk(), "invalid 'note' tactic, ':=' expected");
     expr value = p.parse_tactic_expr_arg();
     return p.save_pos(mk_note_tactic_expr(id, value), pos);
@@ -76,7 +76,7 @@ static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info
     name id;
     if (p.curr_is_token(get_as_tk())) {
         p.next();
-        id = p.check_atomic_id_next("invalid 'generalize' tactic, identifier expected");
+        id = p.check_atomic_id_next("invalid 'generalize' tactic, atomic identifier expected");
     } else {
         if (is_constant(e))
             id = const_name(e);

src/frontends/lean/structure_cmd.cpp

@@ -129,7 +129,7 @@ struct structure_cmd_fn {
     /** \brief Parse structure name and (optional) universe parameters */
     void parse_decl_name() {
         m_name_pos = m_p.pos();
-        m_name = m_p.check_atomic_decl_id_next("invalid 'structure', identifier expected");
+        m_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
         m_name = m_namespace + m_name;
         buffer<name> ls_buffer;
         if (parse_univ_params(m_p, ls_buffer)) {
@@ -937,7 +937,7 @@ struct structure_cmd_fn {
                 m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO;
                 m_mk_infer = implicit_infer_kind::Implicit;
             } else {
-                m_mk_short = m_p.check_atomic_id_next("invalid 'structure', identifier expected");
+                m_mk_short = m_p.check_atomic_id_next("invalid 'structure', atomic identifier expected");
                 m_mk_infer = parse_implicit_infer_modifier(m_p);
                 if (!m_p.curr_is_command_like())
                     m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");

tests/lean/bad_namespace.lean

@@ -1 +0,0 @@
-namespace _root_

tests/lean/bad_namespace.lean.expected.out

@@ -1 +0,0 @@
-bad_namespace.lean:1:10: error: invalid namespace name, '_root_' is reserved

tests/lean/internal_names.lean

@@ -3,3 +3,5 @@ definition _foo : nat := 0 -- error
 structure _bla := (a b : nat)
 
 inductive _empty : Type.
+
+namespace _no

tests/lean/internal_names.lean.expected.out

@@ -1,3 +1,4 @@
 internal_names.lean:1:11: error: invalid declaration name '_foo', identifiers starting with '_' are reserved to the system
 internal_names.lean:3:10: error: invalid declaration name '_bla', identifiers starting with '_' are reserved to the system
 internal_names.lean:5:10: error: invalid declaration name '_empty', identifiers starting with '_' are reserved to the system
+internal_names.lean:7:10: error: invalid declaration name '_no', identifiers starting with '_' are reserved to the system

tests/lean/run/ns2.lean

@@ -27,3 +27,8 @@ namespace vvv
 end vvv
 end bla
 check bla.vvv.my.empty
+
+namespace foo.bla
+  structure vvv.xyz := mk
+end foo.bla
+check foo.bla.vvv.xyz.mk

tests/lean/t3.lean

@@ -23,8 +23,6 @@ namespace tst
   end foo
 end tst
 print raw Type.{tst.foo.U}
-namespace tst.foo    -- Error: we cannot use qualified names in declarations
-universe full.name.U -- Error: we cannot use qualified names in declarations
 namespace tst
   namespace foo
     print raw Type.{v}  -- Remark: alias 'v' for 'tst.v' is available again

tests/lean/t3.lean.expected.out

@@ -9,8 +9,7 @@ t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declar
 Type
 Type
 Type
-t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected
 Type
 Type
-t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level
+t3.lean:33:2: error: universe level alias 'u' shadows existing global universe level
-t3.lean:37:16: error: unknown universe 'bla.u'
+t3.lean:35:16: error: unknown universe 'bla.u'