From a526cd92ac093c5e56ffb9e08dad73d6cfef33d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Apr 2015 12:44:08 -0700
Subject: [PATCH] fix(frontends/lean): bug in pretty printer

this is related to issue #530
---
 src/frontends/lean/pp.cpp                     | 31 +++++++++++++------
 src/frontends/lean/pp.h                       |  2 ++
 tests/lean/param_binder_update.lean           |  2 +-
 .../param_binder_update.lean.expected.out     |  1 +
 tests/lean/pp_param_bug.lean                  |  7 +++++
 tests/lean/pp_param_bug.lean.expected.out     |  1 +
 6 files changed, 34 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/pp_param_bug.lean
 create mode 100644 tests/lean/pp_param_bug.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 9fedaddf3..6ae5d0df4 100644
--- a/src/frontends/lean/pp.cpp
+++ b/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);
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index a8b863957..1da5b0f9f 100644
--- a/src/frontends/lean/pp.h
+++ b/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);
diff --git a/tests/lean/param_binder_update.lean b/tests/lean/param_binder_update.lean
index 98eb177e2..0fc9079ce 100644
--- a/tests/lean/param_binder_update.lean
+++ b/tests/lean/param_binder_update.lean
@@ -32,7 +32,7 @@ section
 
   check @foo1
   check @foo2
-  -- check @foo3 -- TODO
+  check @foo3
   check @foo4
 end
 
diff --git a/tests/lean/param_binder_update.lean.expected.out b/tests/lean/param_binder_update.lean.expected.out
index 4ad4d584b..4a7b109dd 100644
--- a/tests/lean/param_binder_update.lean.expected.out
+++ b/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
diff --git a/tests/lean/pp_param_bug.lean b/tests/lean/pp_param_bug.lean
new file mode 100644
index 000000000..f6ee56bf3
--- /dev/null
+++ b/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
diff --git a/tests/lean/pp_param_bug.lean.expected.out b/tests/lean/pp_param_bug.lean.expected.out
new file mode 100644
index 000000000..78704a0a9
--- /dev/null
+++ b/tests/lean/pp_param_bug.lean.expected.out
@@ -0,0 +1 @@
+foo3 : A → B → A