feat(frontends/lean): identifiers starting with '_' are now reserved

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<binder_info> 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<name> 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<expr> const & fns, buffer<ex
             auto lhs_pos = p.pos();
             if (p.curr_is_token(get_explicit_tk())) {
                 p.next();
-                name fn_name = p.check_id_next("invalid recursive equation, identifier expected");
+                name fn_name = p.check_decl_id_next("invalid recursive equation, identifier expected");
                 lhs_args.push_back(p.save_pos(mk_explicit(get_equation_fn(fns, fn_name, lhs_pos)), lhs_pos));
             } else {
                 expr first = p.parse_expr(get_max_prec());
@@ -534,7 +534,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
             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) {

src/frontends/lean/inductive_cmd.cpp

@@ -197,7 +197,7 @@ struct inductive_cmd_fn {
     */
     pair<name, name> parse_decl_name(optional<name> 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);

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

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<name> 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. */

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<name> ls_buffer;
         if (parse_univ_params(m_p, ls_buffer)) {

src/library/util.cpp

@@ -996,4 +996,8 @@ type_checker_ptr mk_simple_type_checker(environment const & env, name_generator
     return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
                                          std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred))));
 }
+
+bool is_internal_name(name const & n) {
+    return !n.is_anonymous() && n.is_string() && n.get_string() && n.get_string()[0] == '_';
+}
 }

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

tests/lean/internal_names.lean

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

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