fix(frontends/lean/pp): pretty print issue, and fix broken tests output

Remark: we do not allow user to access abstracted version anymore inside
of a section.

src/frontends/lean/pp.cpp

@@ -521,16 +521,9 @@ auto pretty_fn::pp_overriden_local_ref(expr const & e) -> result {
     return result(max_bp()-1, r_fmt);
 }
 
-bool pretty_fn::ignore_local_ref(expr const & e) {
-    expr const & fn = get_app_fn(e);
-    return m_full_names && (!is_constant(fn) || !const_name(fn).is_atomic());
-}
-
 // Return some result if \c e is of the form (c p_1 ... p_n) where
 // c is a constant, and p_i's are parameters fixed in a section.
 auto pretty_fn::pp_local_ref(expr const & e) -> optional<result> {
-    if (ignore_local_ref(e))
-        return optional<result>();
     unsigned num_ref_univ_params;
     switch (check_local_ref(m_env, e, num_ref_univ_params)) {
     case NotLocalRef:
@@ -749,7 +742,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
     bool ignore_hide = true;
     result res_fn    = pp_child(fn, max_bp()-1, ignore_hide);
     format fn_fmt    = res_fn.fmt();
-    if (m_implict && (!is_app(fn) || (!ignore_local_ref(fn) && is_local_ref(m_env, fn))) && has_implicit_args(fn))
+    if (m_implict && (!is_app(fn) || (is_local_ref(m_env, fn))) && has_implicit_args(fn))
         fn_fmt = compose(*g_explicit_fmt, fn_fmt);
     result res_arg = pp_child(app_arg(e), max_bp());
     return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));

src/frontends/lean/pp.h

@@ -107,7 +107,6 @@ private:
     std::pair<bool, token_table const *> needs_space_sep(token_table const * t, std::string const &s1, std::string const &s2) const;
 
     result pp_overriden_local_ref(expr const & e);
-    bool ignore_local_ref(expr const & e);
     optional<result> pp_local_ref(expr const & e);
 
     result pp_hide_coercion(expr const & e, unsigned bp, bool ignore_hide = false);

tests/lean/634.lean

@@ -7,11 +7,11 @@ section
   set_option pp.implicit true
   check @A n
   set_option pp.full_names true
-  check @foo.A X n
+  check @foo.A n
   check @A n
 
   set_option pp.full_names false
-  check @foo.A X n
+  check @foo.A n
   check @A n
 end
 end foo

tests/lean/634.lean.expected.out

@@ -1,5 +1,5 @@
 @A n : Type
-@foo.A X n : Type
-@foo.A X n : Type
+@foo.A n : Type
+@foo.A n : Type
 @A n : Type
 @A n : Type

tests/lean/634b.lean

@@ -6,36 +6,36 @@ section
   definition B : Type := X
   variable {n : ℕ}
   check @A n
-  check foo.A nat
-  check foo.A (X × B)
-  check @foo.A (X × B) 10
-  check @foo.A (@foo.B (@A n)) n
-  check @foo.A (@foo.B (@foo.A X n)) n
-  check @foo.A (@foo.B (@foo.A nat n)) n
+  check foo.A
+  check foo.A
+  check @foo.A 10
+  check @foo.A n
+  check @foo.A n
+  check @foo.A  n
 
   set_option pp.full_names true
   check A
-  check foo.A nat
-  check @foo.A (X × B) 10
-  check @foo.A (@foo.B (@foo.A X n)) n
-  check @foo.A (@foo.B (@foo.A nat n)) n
+  check foo.A
+  check @foo.A 10
+  check @foo.A n
+  check @foo.A n
 
   set_option pp.full_names false
 
   set_option pp.implicit true
   check @A n
-  check @foo.A nat 10
-  check @foo.A X n
+  check @foo.A 10
+  check @foo.A n
   set_option pp.full_names true
-  check @foo.A X n
+  check @foo.A n
   check @A n
 
   set_option pp.full_names false
-  check @foo.A X n
-  check @foo.A B n
-  check @foo.A (@foo.B (@A n)) n
-  check @foo.A (@foo.B (@foo.A X n)) n
-  check @foo.A (@foo.B (@foo.A nat n)) n
+  check @foo.A n
+  check @foo.A n
+  check @foo.A n
+  check @foo.A n
+  check @foo.A n
   check @A n
 end
 end foo

tests/lean/634b.lean.expected.out

@@ -1,23 +1,23 @@
 A : Type
-foo.A ℕ : Type
-foo.A (X × B) : Type
-foo.A (X × B) : Type
-foo.A (foo.B A) : Type
-foo.A (foo.B A) : Type
-foo.A (foo.B (foo.A ℕ)) : Type
-foo.A X : Type
-foo.A ℕ : Type
-foo.A (X × foo.B X) : Type
-foo.A (foo.B (foo.A X)) : Type
-foo.A (foo.B (foo.A ℕ)) : Type
+A : Type
+A : Type
+A : Type
+A : Type
+A : Type
+A : Type
+foo.A : Type
+foo.A : Type
+foo.A : Type
+foo.A : Type
+foo.A : Type
+@A n : Type
+@A 10 : Type
+@A n : Type
+@foo.A n : Type
+@foo.A n : Type
+@A n : Type
+@A n : Type
 @A n : Type
-@foo.A ℕ 10 : Type
 @A n : Type
-@foo.A X n : Type
-@foo.A X n : Type
 @A n : Type
-@foo.A B n : Type
-@foo.A (foo.B (@A n)) n : Type
-@foo.A (foo.B (@A n)) n : Type
-@foo.A (foo.B (@foo.A ℕ n)) n : Type
 @A n : Type

tests/lean/elab_meta2.lean

@@ -1,4 +1,3 @@
-
 print "parametric meta definition"
 meta definition f {A : Type} : nat → A → A → A
 | n a b := if n / 2 = 0 then a else f (n / 2) b a
@@ -19,9 +18,8 @@ print "meta definition inside parametric scope"
 parameter {A : Type}
 meta definition bah : nat → A → A → A
 | n a b := if n / 2 = 0 then a else bah (n / 2) b a
-vm_eval
-  if foo.bah 10 1 2 = 2 then "OK" else "FAILED"
 end
+vm_eval if foo.bah 10 1 2 = 2 then "OK" else "FAILED"
 end foo
 
 print "private meta definition"

tests/lean/local_ref_bugs.lean.expected.out

@@ -1,15 +1,15 @@
-foo.b α : foo
-foo.b α : foo
-foo.b α : foo
+foo.b : foo
+foo.b : foo
+foo.b : foo
 -------
-foo.b α
+foo.b
 foo
 -------
 α : Type
 ⊢ 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 α
+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