fix(library/aliases): aliasing behavior

The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

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

library/standard/pair.lean

@@ -27,7 +27,7 @@ section
   := pair_rec (λ x y, refl (mk_pair x y)) p
 end
 
-instance pair.pair_inhabited
+instance pair_inhabited
 
 precedence `×`:30
 infixr × := pair

src/frontends/lean/decl_cmds.cpp

@@ -273,10 +273,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         levels section_ls = collect_section_levels(ls, p);
         expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps);
         p.add_local_expr(n, ref);
-    } else {
-        if (real_n != n)
-            env = add_alias(env, n, mk_constant(real_n));
     }
+    if (real_n != n)
+        env = add_decl_alias(env, n, mk_constant(real_n));
     level_param_names new_ls;
     if (is_theorem) {
         // TODO(Leo): delay theorems

src/frontends/lean/inductive_cmd.cpp

@@ -498,18 +498,16 @@ struct inductive_cmd_fn {
     }
 
     /** \brief Create an alias for the fully qualified name \c full_id. */
-    environment create_alias(environment const & env, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
+    environment create_alias(environment env, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
         name id(full_id.get_string());
         if (in_section(env)) {
             expr r = mk_explicit(mk_constant(full_id, section_leves));
             r = mk_app(r, section_params);
             m_p.add_local_expr(id, r);
-            return env;
-        } else if (full_id != id) {
-            return add_alias(env, id, mk_constant(full_id));
-        } else {
-            return env;
         }
+        if (full_id != id)
+            env = add_decl_alias(env, id, mk_constant(full_id));
+        return env;
     }
 
     /** \brief Add aliases for the inductive datatype, introduction and elimination rules */

src/library/aliases.cpp

@@ -24,21 +24,28 @@ static environment update(environment const & env, aliases_ext const & ext);
 
 struct aliases_ext : public environment_extension {
     struct state {
+        bool                                      m_in_section;
         rb_map<name, list<expr>, name_quick_cmp>  m_aliases;
         rb_map<expr, name,       expr_quick_cmp>  m_inv_aliases;
         rb_map<name, level,      name_quick_cmp>  m_level_aliases;
         rb_map<level, name,      level_quick_cmp> m_inv_level_aliases;
+        state():m_in_section(false) {}
+
+        void add_alias(name const & a, expr const & e) {
+            auto it = m_aliases.find(a);
+            if (it)
+                m_aliases.insert(a, list<expr>(e, filter(*it, [&](expr const & t) { return t != e; })));
+            else
+                m_aliases.insert(a, list<expr>(e));
+            m_inv_aliases.insert(e, a);
+        }
     };
+
     state       m_state;
     list<state> m_scopes;
 
     void add_alias(name const & a, expr const & e) {
-        auto it = m_state.m_aliases.find(a);
-        if (it)
-            m_state.m_aliases.insert(a, list<expr>(e, filter(*it, [&](expr const & t) { return t != e; })));
-        else
-            m_state.m_aliases.insert(a, list<expr>(e));
-        m_state.m_inv_aliases.insert(e, a);
+        m_state.add_alias(a, e);
     }
 
     void add_alias(name const & a, level const & l) {
@@ -49,8 +56,31 @@ struct aliases_ext : public environment_extension {
         m_state.m_inv_level_aliases.insert(l, a);
     }
 
-    void push() {
+    list<state> add_decl_alias_core(list<state> const & scopes, name const & a, expr const & e) {
+        if (empty(scopes)) {
+            return scopes;
+        } else {
+            state s = head(scopes);
+            s.add_alias(a, e);
+            if (s.m_in_section) {
+                return cons(s, add_decl_alias_core(tail(scopes), a, e));
+            } else {
+                return cons(s, tail(scopes));
+            }
+        }
+    }
+
+    void add_decl_alias(name const & a, expr const & e) {
+        if (m_state.m_in_section) {
+            m_scopes = add_decl_alias_core(m_scopes, a, e);
+        } else {
+            add_alias(a, e);
+        }
+    }
+
+    void push(bool in_section) {
         m_scopes = list<state>(m_state, m_scopes);
+        m_state.m_in_section = in_section;
     }
 
     void pop() {
@@ -63,16 +93,16 @@ struct aliases_ext : public environment_extension {
         return env;
     }
 
-    static environment push_scope(environment const & env) {
+    static environment push_scope(environment const & env, bool in_section) {
         aliases_ext ext = get_extension(env);
-        ext.push();
+        ext.push(in_section);
         environment new_env = update(env, ext);
-        if (!in_section(new_env))
+        if (!::lean::in_section(new_env))
             new_env = add_aliases(new_env, get_namespace(new_env), name());
         return new_env;
     }
 
-    static environment pop_scope(environment const & env) {
+    static environment pop_scope(environment const & env, bool) {
         aliases_ext ext = get_extension(env);
         ext.pop();
         return update(env, ext);
@@ -102,6 +132,12 @@ environment add_alias(environment const & env, name const & a, expr const & e) {
     return update(env, ext);
 }
 
+environment add_decl_alias(environment const & env, name const & a, expr const & e) {
+    aliases_ext ext = get_extension(env);
+    ext.add_decl_alias(a, e);
+    return update(env, ext);
+}
+
 optional<name> is_aliased(environment const & env, expr const & t) {
     auto it = get_extension(env).m_state.m_inv_aliases.find(t);
     return it ? optional<name>(*it) : optional<name>();
@@ -112,9 +148,13 @@ list<expr> get_alias_exprs(environment const & env, name const & n) {
     return it ? *it : list<expr>();
 }
 
-environment add_alias(environment const & env, name const & a, level const & l) {
+static void check_no_shadow(environment const & env, name const & a) {
     if (env.is_universe(a))
         throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
+}
+
+environment add_alias(environment const & env, name const & a, level const & l) {
+    check_no_shadow(env, a);
     aliases_ext ext = get_extension(env);
     ext.add_alias(a, l);
     return update(env, ext);

src/library/aliases.h

@@ -12,6 +12,12 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Add the alias \c a for expression \c e. \c e must not have free variables. */
 environment add_alias(environment const & env, name const & a, expr const & e);
+/**
+   \brief Add alias \c a for expression \c e, and also add it to all parent scopes
+   until in a namespace scope.
+*/
+environment add_decl_alias(environment const & env, name const & a, expr const & e);
+
 
 /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
 optional<name> is_aliased(environment const & env, expr const & t);

src/library/scoped_ext.cpp

@@ -64,13 +64,14 @@ environment using_namespace(environment const & env, io_state const & ios, name
 environment push_scope(environment const & env, io_state const & ios, name const & n) {
     if (!n.is_anonymous() && in_section(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
+    bool in_section = n.is_anonymous();
     name new_n = get_namespace(env) + n;
     scope_mng_ext ext = get_extension(env);
     ext.m_namespaces = list<name>(new_n, ext.m_namespaces);
     ext.m_in_section = list<bool>(n.is_anonymous(), ext.m_in_section);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<2>(t)(r);
+        r = std::get<2>(t)(r, in_section);
     }
     if (!n.is_anonymous())
         r = using_namespace(r, ios, n);
@@ -81,11 +82,12 @@ environment pop_scope(environment const & env) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
         throw exception("invalid end of scope, there are no open namespaces/sections");
+    bool in_section  = head(ext.m_in_section);
     ext.m_namespaces = tail(ext.m_namespaces);
     ext.m_in_section = tail(ext.m_in_section);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<3>(t)(r);
+        r = std::get<3>(t)(r, in_section);
     }
     return r;
 }

src/library/scoped_ext.h

@@ -16,8 +16,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
-typedef environment (*push_scope_fn)(environment const &);
-typedef environment (*pop_scope_fn)(environment const &);
+typedef environment (*push_scope_fn)(environment const &, bool);
+typedef environment (*pop_scope_fn)(environment const &, bool);
 
 void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop);
 /** \brief Use objects defined in the namespace \c n, if \c c is not the anonymous name, then only object from "class" \c c are considered. */
@@ -137,10 +137,10 @@ public:
     static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) {
         return update(env, get(env).using_namespace(env, ios, n));
     }
-    static environment push_fn(environment const & env) {
+    static environment push_fn(environment const & env, bool) {
         return update(env, get(env).push());
     }
-    static environment pop_fn(environment const & env) {
+    static environment pop_fn(environment const & env, bool) {
         return update(env, get(env).pop());
     }
     static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) {

tests/lean/run/alias3.lean

@@ -0,0 +1,26 @@
+import logic
+
+namespace N1
+  section
+    section
+      variable A : Type
+      definition foo (a : A) : Bool := true
+      check foo
+    end
+    check foo
+  end
+  check foo
+end
+check N1.foo
+
+namespace N2
+  section
+    parameter A : Type
+    inductive list : Type :=
+    | nil {} : list
+    | cons   : A → list → list
+    check list
+  end
+  check list
+end
+check N2.list