feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -73,7 +73,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
         return parse_let_body(p, pos);
     } else {
         auto pos = p.pos();
-        name id  = p.check_id_next("invalid let declaration, identifier expected");
+        name id  = p.check_atomic_id_next("invalid let declaration, identifier expected");
         bool is_opaque = true;
         bool is_fact   = false;
         expr type, value;

src/frontends/lean/parser.cpp

@@ -284,6 +284,14 @@ name parser::check_id_next(char const * msg) {
     return r;
 }
 
+name parser::check_atomic_id_next(char const * msg) {
+    auto p  = pos();
+    name id = check_id_next(msg);
+    if (!id.is_atomic())
+        throw parser_error(msg, p);
+    return id;
+}
+
 expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
     return save_pos(::lean::mk_app(fn, arg), p);
 }
@@ -328,14 +336,6 @@ unsigned parser::get_local_index(name const & n) const {
     return m_local_decls.find_idx(n);
 }
 
-/** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
-void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
-    while (curr_is_identifier()) {
-        result.emplace_back(pos(), get_name_val());
-        next();
-    }
-}
-
 static name g_period("."), g_colon(":"), g_lparen("("), g_rparen(")"), g_llevel_curly(".{");
 static name g_lcurly("{"), g_rcurly("}"), g_ldcurly("⦃"), g_rdcurly("⦄"), g_lbracket("["), g_rbracket("]");
 static name g_bar("|"), g_comma(","), g_add("+"), g_max("max"), g_imax("imax"), g_cup("\u2294");
@@ -566,10 +566,7 @@ void parser::parse_close_binder_info(optional<binder_info> const & bi) {
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
 expr parser::parse_binder_core(binder_info const & bi) {
     auto p  = pos();
-    if (!curr_is_identifier())
-        throw parser_error("invalid binder, identifier expected", p);
-    name id = get_name_val();
-    next();
+    name id = check_atomic_id_next("invalid binder, atomic identifier expected");
     expr type;
     if (curr_is_token(g_colon)) {
         next();
@@ -597,7 +594,10 @@ expr parser::parse_binder() {
 */
 void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
     buffer<std::pair<pos_info, name>> names;
-    parse_names(names);
+    while (curr_is_identifier()) {
+        auto p = pos();
+        names.emplace_back(p, check_atomic_id_next("invalid binder, atomic identifier expected"));
+    }
     if (names.empty())
         throw parser_error("invalid binder, identifier expected", pos());
     optional<expr> type;
@@ -798,29 +798,42 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
         next();
         ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
     }
-    // locals
-    if (auto it1 = m_local_decls.find(id))
-        return copy_with_new_pos(propagate_levels(*it1, ls), p);
-    optional<expr> r;
-    // globals
-    if (m_env.find(id))
-        r = save_pos(mk_constant(id, ls), p);
-    // aliases
-    auto as = get_alias_exprs(m_env, id);
-    if (!is_nil(as)) {
-        buffer<expr> new_as;
-        if (r)
-            new_as.push_back(*r);
-        for (auto const & e : as) {
-            new_as.push_back(copy_with_new_pos(propagate_levels(e, ls), p));
+    if (id.is_atomic()) {
+        // locals
+        if (auto it1 = m_local_decls.find(id))
+            return copy_with_new_pos(propagate_levels(*it1, ls), p);
+        optional<expr> r;
+        // globals
+        if (m_env.find(id))
+            r = save_pos(mk_constant(id, ls), p);
+        // aliases
+        auto as = get_alias_exprs(m_env, id);
+        if (!is_nil(as)) {
+            buffer<expr> new_as;
+            if (r)
+                new_as.push_back(*r);
+            for (auto const & e : as) {
+                new_as.push_back(copy_with_new_pos(propagate_levels(e, ls), p));
+            }
+            r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
+        }
+        if (!r && m_no_undef_id_error)
+            r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
+        if (!r)
+            throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
+        return *r;
+    } else {
+        if (m_env.find(id)) {
+            return save_pos(mk_constant(id, ls), p);
+        } else {
+            for (name const & ns : get_namespaces(m_env)) {
+                auto new_id = ns + id;
+                if (m_env.find(new_id))
+                    return save_pos(mk_constant(new_id, ls), p);
+            }
         }
-        r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
-    }
-    if (!r && m_no_undef_id_error)
-        r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
-    if (!r)
         throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
-    return *r;
+    }
 }
 
 expr parser::parse_id() {

src/frontends/lean/parser.h

@@ -183,6 +183,9 @@ public:
     void check_token_next(name const & tk, char const * msg);
     /** \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 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);
 
     mpq const & get_num_val() const { return m_scanner.get_num_val(); }
     name const & get_name_val() const { return m_scanner.get_name_val(); }
@@ -193,7 +196,6 @@ public:
     regular regular_stream() const { return regular(env(), ios()); }
     diagnostic diagnostic_stream() const { return diagnostic(env(), ios()); }
 
-    void parse_names(buffer<std::pair<pos_info, name>> & result);
     unsigned get_small_nat();
     unsigned parse_small_nat();
     double parse_double();

src/library/aliases.cpp

@@ -126,13 +126,20 @@ static environment update(environment const & env, aliases_ext const & ext) {
     return env.update(g_ext.m_ext_id, std::make_shared<aliases_ext>(ext));
 }
 
+static void check_atomic(name const & a) {
+    if (!a.is_atomic())
+        throw exception(sstream() << "invalid alias '" << a << "', aliases must be atomic names");
+}
+
 environment add_alias(environment const & env, name const & a, expr const & e) {
+    check_atomic(a);
     aliases_ext ext = get_extension(env);
     ext.add_alias(a, e);
     return update(env, ext);
 }
 
 environment add_decl_alias(environment const & env, name const & a, expr const & e) {
+    check_atomic(a);
     aliases_ext ext = get_extension(env);
     ext.add_decl_alias(a, e);
     return update(env, ext);
@@ -154,6 +161,7 @@ static void check_no_shadow(environment const & env, name const & a) {
 }
 
 environment add_alias(environment const & env, name const & a, level const & l) {
+    check_atomic(a);
     check_no_shadow(env, a);
     aliases_ext ext = get_extension(env);
     ext.add_alias(a, l);

src/library/scoped_ext.cpp

@@ -49,6 +49,10 @@ name const & get_namespace(environment const & env) {
     return !is_nil(ext.m_namespaces) ? head(ext.m_namespaces) : name::anonymous();
 }
 
+list<name> const & get_namespaces(environment const & env) {
+    return get_extension(env).m_namespaces;
+}
+
 bool in_section(environment const & env) {
     scope_mng_ext const & ext = get_extension(env);
     return !is_nil(ext.m_in_section) && head(ext.m_in_section);

src/library/scoped_ext.h

@@ -28,6 +28,7 @@ environment push_scope(environment const & env, io_state const & ios, name const
 environment pop_scope(environment const & env);
 
 name const & get_namespace(environment const & env);
+list<name> const & get_namespaces(environment const & env);
 bool in_section(environment const & env);
 
 /** \brief Check if \c n may be a reference to a namespace, if it is return it.

tests/lean/run/algebra1.lean

@@ -77,6 +77,8 @@ namespace semigroup
 end
 
 namespace monoid
+  check semigroup.mul
+
   inductive monoid_struct (A : Type) : Type :=
   | mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A