From c73b2860d5211187e9aa1039d1a49dcabdca4292 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 10 May 2016 18:21:31 -0400 Subject: [PATCH] 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 | 7 ++----- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/builtin_tactics.cpp | 6 +++--- src/frontends/lean/structure_cmd.cpp | 4 ++-- tests/lean/bad_namespace.lean | 1 - tests/lean/bad_namespace.lean.expected.out | 1 - tests/lean/internal_names.lean | 2 ++ tests/lean/internal_names.lean.expected.out | 1 + tests/lean/run/ns2.lean | 5 +++++ tests/lean/t3.lean | 2 -- tests/lean/t3.lean.expected.out | 5 ++--- 11 files changed, 18 insertions(+), 18 deletions(-) delete mode 100644 tests/lean/bad_namespace.lean delete mode 100644 tests/lean/bad_namespace.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 4e808cff1..2d67b2e98 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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_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); + name n = p.check_decl_id_next("invalid namespace declaration, identifier expected"); 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> 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 { diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index e5d4f07ec..1ea89de05 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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 type; expr value; if (p.curr_is_token(get_assign_tk())) { diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index 34f76e218..1170d282d 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/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); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 60f5df709..7bf1285d8 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/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 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"); diff --git a/tests/lean/bad_namespace.lean b/tests/lean/bad_namespace.lean deleted file mode 100644 index b5a3ba24b..000000000 --- a/tests/lean/bad_namespace.lean +++ /dev/null @@ -1 +0,0 @@ -namespace _root_ diff --git a/tests/lean/bad_namespace.lean.expected.out b/tests/lean/bad_namespace.lean.expected.out deleted file mode 100644 index 0238afd21..000000000 --- a/tests/lean/bad_namespace.lean.expected.out +++ /dev/null @@ -1 +0,0 @@ -bad_namespace.lean:1:10: error: invalid namespace name, '_root_' is reserved diff --git a/tests/lean/internal_names.lean b/tests/lean/internal_names.lean index 21811b4bc..40e6eb8b5 100644 --- a/tests/lean/internal_names.lean +++ b/tests/lean/internal_names.lean @@ -3,3 +3,5 @@ definition _foo : nat := 0 -- error structure _bla := (a b : nat) inductive _empty : Type. + +namespace _no diff --git a/tests/lean/internal_names.lean.expected.out b/tests/lean/internal_names.lean.expected.out index 87e5e7754..c69281a64 100644 --- a/tests/lean/internal_names.lean.expected.out +++ b/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 diff --git a/tests/lean/run/ns2.lean b/tests/lean/run/ns2.lean index 321b37954..004d4e9e4 100644 --- a/tests/lean/run/ns2.lean +++ b/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 diff --git a/tests/lean/t3.lean b/tests/lean/t3.lean index 830f4323f..f87c2d8b1 100644 --- a/tests/lean/t3.lean +++ b/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 diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out index b480e1388..f65c00e51 100644 --- a/tests/lean/t3.lean.expected.out +++ b/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:37:16: error: unknown universe 'bla.u' +t3.lean:33:2: error: universe level alias 'u' shadows existing global universe level +t3.lean:35:16: error: unknown universe 'bla.u'