fix(frontends/lean): bug in pretty printer

this is related to issue #530

src/frontends/lean/pp.cpp

@@ -364,10 +364,30 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) ->
     }
 }
 
+// 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> {
+    lean_assert(is_app(e));
+    expr const & rfn = get_app_fn(e);
+    if (is_constant(rfn)) {
+        if (auto info = get_local_ref_info(m_env, const_name(rfn))) {
+            buffer<expr> args;
+            get_app_args(e, args);
+            if (args.size() == info->second) {
+                // TODO(Leo): must check if the arguments are really the fixed parameters.
+                return some(pp_const(rfn));
+            }
+        }
+    }
+    return optional<result>();
+}
+
 auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
     if (auto it = is_abbreviated(e))
         return pp_abbreviation(e, *it, false, bp, ignore_hide);
     if (is_app(e)) {
+        if (auto r = pp_local_ref(e))
+            return *r;
         expr const & f = app_fn(e);
         if (auto it = is_abbreviated(f)) {
             return pp_abbreviation(e, *it, true, bp, ignore_hide);
@@ -501,15 +521,8 @@ bool pretty_fn::has_implicit_args(expr const & f) {
 }
 
 auto pretty_fn::pp_app(expr const & e) -> result {
-    expr const & rfn = get_app_fn(e);
-    if (is_constant(rfn)) {
-        if (auto info = get_local_ref_info(m_env, const_name(rfn))) {
-            buffer<expr> args;
-            get_app_args(e, args);
-            if (args.size() == info->second)
-                return pp_const(rfn);
-        }
-    }
+    if (auto r = pp_local_ref(e))
+        return *r;
     expr const & fn = app_fn(e);
     if (auto it = is_abbreviated(fn))
         return pp_abbreviation(e, *it, true);

src/frontends/lean/pp.h

@@ -90,6 +90,8 @@ private:
     optional<result> pp_notation(notation_entry const & entry, buffer<optional<expr>> & args);
     optional<result> pp_notation(expr const & e);
 
+    optional<result> pp_local_ref(expr const & e);
+
     result pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide = false);
     result pp_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);

tests/lean/param_binder_update.lean

@@ -32,7 +32,7 @@ section
 
   check @foo1
   check @foo2
-  -- check @foo3 -- TODO
+  check @foo3
   check @foo4
 end
 

tests/lean/param_binder_update.lean.expected.out

@@ -2,6 +2,7 @@ id : Π (A : Type), A → A
 id₂ : Π {A : Type}, A → A
 foo1 : A → B → A
 foo2 : A → B → A
+foo3 : A → B → A
 foo4 : A → B → A
 foo1 : Π {A : Type} {B : Type}, A → B → A
 foo2 : Π {A : Type} (B : Type), A → B → A

tests/lean/pp_param_bug.lean

@@ -0,0 +1,7 @@
+section
+  parameters (A : Type) {B : Type}
+
+  definition foo3 (a : A) (b : B) := a
+
+  check foo3
+end

tests/lean/pp_param_bug.lean.expected.out

@@ -0,0 +1 @@
+foo3 : A → B → A