fix(frontends/lean/pp): bugs when pretty printing abbreviations

src/frontends/lean/pp.cpp

@@ -359,13 +359,19 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
 }
 
 auto pretty_fn::pp_child(expr const & e, unsigned bp) -> result {
-    if (is_app(e) && is_implicit(app_fn(e))) {
-        return pp_child(app_fn(e), bp);
-    } else if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) {
+    if (auto it = is_abbreviated(e))
+        return pp_abbreviation(e, *it, false);
+    if (is_app(e)) {
+        expr const & f = app_fn(e);
+        if (auto it = is_abbreviated(f)) {
+            return pp_abbreviation(e, *it, true);
+        } else if (is_implicit(f)) {
+            return pp_child(f, bp);
+        } else if (!m_coercion && is_coercion(m_env, f)) {
             return pp_coercion(e, bp);
-    } else {
-        return pp_child_core(e, bp);
         }
+    }
+    return pp_child_core(e, bp);
 }
 
 auto pretty_fn::pp_var(expr const & e) -> result {
@@ -396,6 +402,12 @@ optional<name> pretty_fn::is_aliased(name const & n) const {
     }
 }
 
+optional<name> pretty_fn::is_abbreviated(expr const & e) const {
+    if (m_abbreviations)
+        return ::lean::is_abbreviated(m_env, e);
+    return optional<name>();
+}
+
 auto pretty_fn::pp_const(expr const & e) -> result {
     name n = const_name(e);
     if (!m_full_names) {
@@ -472,11 +484,8 @@ bool pretty_fn::has_implicit_args(expr const & f) {
 
 auto pretty_fn::pp_app(expr const & e) -> result {
     expr const & fn = app_fn(e);
-    if (m_abbreviations)  {
-        if (auto it = is_abbreviated(m_env, fn)) {
-            return pp_abbreviation(e, *it);
-        }
-    }
+    if (auto it = is_abbreviated(fn))
+        return pp_abbreviation(e, *it, true);
     result res_fn = pp_child(fn, max_bp()-1);
     format fn_fmt = res_fn.fmt();
     if (m_implict && !is_app(fn) && has_implicit_args(fn))
@@ -797,18 +806,24 @@ static unsigned get_some_precedence(token_table const & t, name const & tk) {
 }
 
 auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result {
-    if (is_app(e) && is_implicit(app_fn(e))) {
-        return pp_notation_child(app_fn(e), lbp, rbp);
-    } else if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) {
+    if (auto it = is_abbreviated(e))
+        return pp_abbreviation(e, *it, false);
+    if (is_app(e)) {
+        expr const & f = app_fn(e);
+        if (auto it = is_abbreviated(f)) {
+            return pp_abbreviation(e, *it, true);
+        } else if (is_implicit(f)) {
+            return pp_notation_child(f, lbp, rbp);
+        } else if (!m_coercion && is_coercion(m_env, f)) {
             return pp_coercion(e, rbp);
-    } else {
+        }
+    }
     result r = pp(e);
     if (r.rbp() < lbp || r.lbp() <= rbp) {
         return result(paren(r.fmt()));
     } else {
         return r;
     }
-    }
 }
 
 static bool add_extra_space_first(name const & tk) {
@@ -1037,13 +1052,14 @@ auto pretty_fn::pp_notation(expr const & e) -> optional<result> {
     return optional<result>();
 }
 
-auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev) -> result {
+auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn) -> result {
     declaration const & d = m_env.get(abbrev);
     unsigned num_univs    = d.get_num_univ_params();
     buffer<level> ls;
     for (unsigned i = 0; i < num_univs; i++)
         ls.push_back(mk_meta_univ(name("?l", i+1)));
     buffer<expr> args;
+    if (fn)
         get_app_args(e, args);
     return pp(mk_app(mk_constant(abbrev, to_list(ls)), args));
 }
@@ -1054,6 +1070,9 @@ auto pretty_fn::pp(expr const & e) -> result {
     flet<unsigned> let_d(m_depth, m_depth+1);
     m_num_steps++;
 
+    if (auto n = is_abbreviated(e))
+        return pp_abbreviation(e, *n, false);
+
     if (auto r = pp_notation(e))
         return *r;
 
@@ -1063,9 +1082,6 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_let(e))          return pp_let(e);
     if (is_typed_expr(e))   return pp(get_typed_expr_expr(e));
     if (is_let_value(e))    return pp(get_let_value_expr(e));
-    if (m_abbreviations)
-        if (auto n = is_abbreviated(m_env, e))
-            return pp_abbreviation(e, *n);
     if (m_numerals)
         if (auto n = to_num(e)) return pp_num(*n);
     if (m_num_nat_coe)

src/frontends/lean/pp.h

@@ -76,6 +76,7 @@ private:
     bool is_prop(expr const & e);
     bool has_implicit_args(expr const & f);
     optional<name> is_aliased(name const & n) const;
+    optional<name> is_abbreviated(expr const & e) const;
 
     format pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi);
     format pp_binders(buffer<expr> const & locals);
@@ -105,7 +106,8 @@ private:
     result pp_explicit(expr const & e);
     result pp_let(expr e);
     result pp_num(mpz const & n);
-    result pp_abbreviation(expr const & e, name const & abbrev);
+    // If fn is true, then \c e is of the form (f a), and the abbreviation is \c f.
+    result pp_abbreviation(expr const & e, name const & abbrev, bool fn);
     void set_options_core(options const & o);
 
 public:

tests/lean/abbrev2.lean

@@ -0,0 +1,27 @@
+open nat
+
+namespace bla
+  local abbreviation foo : nat := 10 + 1
+  definition tst : nat := foo
+  print definition tst
+end bla
+
+-- abbreviation is gone
+print definition bla.tst
+
+check bla.foo
+open bla
+check foo
+
+print definition tst
+
+namespace bla2
+  abbreviation foo2 : nat := 1
+  definition tst2 : nat := foo2
+  print definition tst2
+end bla2
+
+print definition bla2.tst2
+open bla2
+print definition bla2.tst2
+print definition tst2

tests/lean/abbrev2.lean.expected.out

@@ -0,0 +1,9 @@
+foo
+10 + 1
+abbrev2.lean:12:6: error: unknown identifier 'bla.foo'
+abbrev2.lean:14:6: error: unknown identifier 'foo'
+10 + 1
+foo2
+1
+foo2
+foo2