From cf61adc5d5d7269ff62b4b5c118f1e9a8adadf94 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Dec 2015 22:32:03 -0800 Subject: [PATCH] feat(frontends/lean): identifiers starting with '_' are now reserved --- src/frontends/lean/decl_cmds.cpp | 10 +++++----- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/parser.cpp | 19 +++++++++++++++++++ src/frontends/lean/parser.h | 3 +++ src/frontends/lean/structure_cmd.cpp | 2 +- src/library/util.cpp | 4 ++++ src/library/util.h | 3 +++ tests/lean/internal_names.lean | 5 +++++ tests/lean/internal_names.lean.expected.out | 3 +++ 9 files changed, 44 insertions(+), 7 deletions(-) create mode 100644 tests/lean/internal_names.lean create mode 100644 tests/lean/internal_names.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index fa5d34f23..9be5736d2 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -73,7 +73,7 @@ static environment universe_cmd(parser & p) { p.next(); local = true; } - name n = p.check_id_next("invalid 'universe' command, identifier expected"); + name n = p.check_decl_id_next("invalid 'universe' command, identifier expected"); return declare_universe(p, p.env(), n, local); } } @@ -222,7 +222,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, bool is_protec check_variable_kind(p, k); auto pos = p.pos(); optional bi = parse_binder_info(p, k); - name n = p.check_id_next("invalid declaration, identifier expected"); + name n = p.check_decl_id_next("invalid declaration, identifier expected"); buffer ls_buffer; if (p.curr_is_token(get_llevel_curly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable)) throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos()); @@ -473,7 +473,7 @@ static void parse_equations_core(parser & p, buffer const & fns, buffer while (p.curr_is_token(get_with_tk())) { p.next(); auto pos = p.pos(); - name g_name = p.check_id_next("invalid declaration, identifier expected"); + name g_name = p.check_decl_id_next("invalid declaration, identifier expected"); p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected"); expr g_type = p.parse_expr(); expr g = p.save_pos(mk_local(g_name, g_type), pos); @@ -683,7 +683,7 @@ class definition_cmd_fn { if (m_kind == Example) m_name = get_this_tk(); else - m_name = m_p.check_id_next("invalid declaration, identifier expected"); + m_name = m_p.check_decl_id_next("invalid declaration, identifier expected"); } expr extract_nested(expr const & v) { diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index e271cbb47..f4ad64fd9 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -197,7 +197,7 @@ struct inductive_cmd_fn { */ pair parse_decl_name(optional const & ind_name) { m_pos = m_p.pos(); - name id = m_p.check_id_next("invalid declaration, identifier expected"); + name id = m_p.check_decl_id_next("invalid declaration, identifier expected"); if (ind_name) { // for intro rules, we append the name of the inductive datatype check_atomic(id); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 852d80932..7562bfd0d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -514,6 +514,18 @@ name parser::check_id_next(char const * msg) { return r; } +static void check_not_internal(name const & id, pos_info const & p) { + if (is_internal_name(id)) + throw parser_error(sstream() << "invalid declaration name '" << id << "', identifiers starting with '_' are reserved to the system", p); +} + +name parser::check_decl_id_next(char const * msg) { + auto p = pos(); + name id = check_id_next(msg); + check_not_internal(id, p); + return id; +} + name parser::check_atomic_id_next(char const * msg) { auto p = pos(); name id = check_id_next(msg); @@ -522,6 +534,13 @@ name parser::check_atomic_id_next(char const * msg) { return id; } +name parser::check_atomic_decl_id_next(char const * msg) { + auto p = pos(); + name id = check_atomic_id_next(msg); + check_not_internal(id, p); + return id; +} + expr parser::mk_app(expr fn, expr arg, pos_info const & p) { return save_pos(::lean::mk_app(fn, arg), p); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index a78a1474e..ebd04d2be 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -378,9 +378,12 @@ public: /** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */ name check_id_next(char const * msg); + /** \brief Similar to check_id_next, but also ensures the identifier is *not* an internal/reserved name. */ + name check_decl_id_next(char const * msg); /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, otherwise throw an exception. */ name check_atomic_id_next(char const * msg); + name check_atomic_decl_id_next(char const * msg); list to_constants(name const & id, char const * msg, pos_info const & p) const; name to_constant(name const & id, char const * msg, pos_info const & p); /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 5835aaff8..92c8b42de 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -122,7 +122,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_id_next("invalid 'structure', identifier expected"); + m_name = m_p.check_atomic_decl_id_next("invalid 'structure', identifier expected"); m_name = m_namespace + m_name; buffer ls_buffer; if (parse_univ_params(m_p, ls_buffer)) { diff --git a/src/library/util.cpp b/src/library/util.cpp index c41dfa35e..8b0029d4d 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -996,4 +996,8 @@ type_checker_ptr mk_simple_type_checker(environment const & env, name_generator return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new hint_converter(env, pred)))); } + +bool is_internal_name(name const & n) { + return !n.is_anonymous() && n.is_string() && n.get_string() && n.get_string()[0] == '_'; +} } diff --git a/src/library/util.h b/src/library/util.h index f01fd0d2b..c538308aa 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -282,6 +282,9 @@ expr instantiate_meta(expr const & meta, substitution & subst); metavariable application \c m of the form (?m l_1 ... l_k) */ justification mk_failed_to_synthesize_jst(environment const & env, expr const & m); +/** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */ +bool is_internal_name(name const & n); + void initialize_library_util(); void finalize_library_util(); } diff --git a/tests/lean/internal_names.lean b/tests/lean/internal_names.lean new file mode 100644 index 000000000..21811b4bc --- /dev/null +++ b/tests/lean/internal_names.lean @@ -0,0 +1,5 @@ +definition _foo : nat := 0 -- error + +structure _bla := (a b : nat) + +inductive _empty : Type. diff --git a/tests/lean/internal_names.lean.expected.out b/tests/lean/internal_names.lean.expected.out new file mode 100644 index 000000000..87e5e7754 --- /dev/null +++ b/tests/lean/internal_names.lean.expected.out @@ -0,0 +1,3 @@ +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