feat(library/aliases,frontends/lean/parser): take local_ref's into account when defining new aliases; use get_local_ref at id_to_expr; use get_local_ref at resolve_local_name

see #1251

src/frontends/lean/elaborator.cpp

@@ -2844,6 +2844,11 @@ static expr resolve_local_name(environment const & env, local_context const & lc
         return copy_tag(src, decl->mk_ref());
     }
 
+    /* check local_refs */
+    if (auto ref = get_local_ref(env, id)) {
+        return copy_tag(src, copy(*ref));
+    }
+
     /* check in current namespaces */
     for (name const & ns : get_namespaces(env)) {
         auto new_id = ns + id;

src/frontends/lean/parser.cpp

@@ -1696,6 +1696,12 @@ expr parser::patexpr_to_expr(expr const & pat_or_expr) {
         });
 }
 
+static void check_no_levels(levels const & ls, pos_info const & p) {
+    if (ls)
+        throw parser_error("invalid use of explicit universe parameter, identifier is a variable, "
+                           "parameter or a constant bound to parameters in a section", p);
+}
+
 expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only) {
     buffer<level> lvl_buffer;
     levels ls;
@@ -1716,9 +1722,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only)
 
     // locals
     if (auto it1 = m_local_decls.find(id)) {
-        if (ls)
-            throw parser_error("invalid use of explicit universe parameter, identifier is a variable, "
-                               "parameter or a constant bound to parameters in a section", p);
+        check_no_levels(ls, p);
         return copy_with_new_pos(*it1, p);
     }
 
@@ -1726,6 +1730,11 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only)
         return save_pos(mk_local(id, save_pos(mk_expr_placeholder(), p)), p);
     }
 
+    if (auto ref = get_local_ref(m_env, id)) {
+        check_no_levels(ls, p);
+        return copy_with_new_pos(*ref, p);
+    }
+
     for (name const & ns : get_namespaces(m_env)) {
         auto new_id = ns + id;
         if (!ns.is_anonymous() && m_env.find(new_id) &&
@@ -1744,6 +1753,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only)
 
     optional<expr> r;
     // globals
+
     if (m_env.find(id))
         r = save_pos(mk_constant(id, ls), p);
     // aliases

src/library/aliases.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "library/trace.h"
 #include "library/expr_lt.h"
 #include "library/aliases.h"
 #include "library/placeholder.h"
@@ -31,13 +32,21 @@ struct aliases_ext : public environment_extension {
         name_map<expr>        m_local_refs;
         state():m_in_section(false) {}
 
+        void add_local_ref(name const & a, expr const & ref) {
+            m_local_refs.insert(a, ref);
+        }
+
         void add_expr_alias(name const & a, name const & e, bool overwrite) {
-            auto it = m_aliases.find(a);
-            if (it && !overwrite)
-                m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
-            else
-                m_aliases.insert(a, to_list(e));
-            m_inv_aliases.insert(e, a);
+            if (auto ref = m_local_refs.find(e)) {
+                add_local_ref(a, *ref);
+            } else {
+                auto it = m_aliases.find(a);
+                if (it && !overwrite)
+                    m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
+                else
+                    m_aliases.insert(a, to_list(e));
+                m_inv_aliases.insert(e, a);
+            }
         }
     };
 
@@ -78,7 +87,7 @@ struct aliases_ext : public environment_extension {
     }
 
     void add_local_ref(name const & a, expr const & ref) {
-        m_state.m_local_refs.insert(a, ref);
+        m_state.add_local_ref(a, ref);
     }
 
     void push(bool in_section) {

tests/lean/local_ref_bugs.lean

@@ -0,0 +1,45 @@
+set_option pp.all true
+
+section
+parameter α : Type
+inductive foo : Type | a : α → foo | b
+check (foo.b : foo)
+open foo
+check (foo.b : foo)
+check (b : foo)
+
+open tactic
+include α
+example : true :=
+by do
+  e ← to_expr `(b),
+  t ← infer_type e,
+  trace "-------",
+  trace e,
+  trace t,
+  trace "-------",
+  triv
+
+end
+
+namespace bla
+section
+parameter α : Type
+inductive foo : Type | a : α → foo | b
+check (foo.b : foo)
+open foo
+check (foo.b : foo)
+check (b : foo)
+end
+end bla
+
+namespace boo
+section
+parameter α : Type
+inductive foo : Type | a : α → foo | b
+check (foo.b : foo)
+open foo (b)
+check (foo.b : foo)
+check (b : foo)
+end
+end boo

tests/lean/local_ref_bugs.lean.expected.out

@@ -0,0 +1,13 @@
+foo.b α : foo
+foo.b α : foo
+foo.b α : foo
+-------
+foo.b α
+foo
+-------
+bla.foo.b α : bla.foo α
+bla.foo.b α : bla.foo α
+bla.foo.b α : bla.foo α
+boo.foo.b α : boo.foo α
+boo.foo.b α : boo.foo α
+boo.foo.b α : boo.foo α