From 8fe7465adeda2c5f13b2507b5241cbbf61b627d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Sep 2014 09:56:46 -0700
Subject: [PATCH] fix(frontends/lean/pp): when formatting a coercion to
 function-class that contains implicit arguments

---
 src/frontends/lean/pp.cpp        | 32 ++++++++++++++++++++++++++++----
 src/frontends/lean/pp.h          |  1 +
 tests/lean/coe.lean              | 12 ++++++++++++
 tests/lean/coe.lean.expected.out |  1 +
 4 files changed, 42 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/coe.lean
 create mode 100644 tests/lean/coe.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 6a6071283..8ae1ee7e7 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -152,17 +152,41 @@ bool pretty_fn::is_prop(expr const & e) {
     }
 }
 
+auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result {
+    if (sz == 1) {
+        return pp_child(app_arg(e), max_bp()-1);
+    } else if (is_app(e) && is_implicit(app_fn(e))) {
+        return pp_coercion_fn(app_fn(e), sz-1);
+    } else {
+        expr const & fn = app_fn(e);
+        result res_fn   = pp_coercion_fn(fn, sz-1);
+        format fn_fmt   = res_fn.first;
+        if (m_implict && sz == 2 && has_implicit_args(fn))
+            fn_fmt = compose(g_explicit_fmt, fn_fmt);
+        result res_arg  = pp_child(app_arg(e), max_bp());
+        return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1);
+    }
+}
+
 auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
     buffer<expr> args;
     expr const & f = get_app_args(e, args);
     optional<pair<name, unsigned>> r = is_coercion(m_env, f);
     lean_assert(r);
-    if (r->second >= args.size())
+    if (r->second >= args.size()) {
         return pp_child_core(e, bp);
-    else if (r->second == args.size() - 1)
+    } else if (r->second == args.size() - 1) {
         return pp_child(args.back(), bp);
-    else
-        return pp_child(mk_app(args.size() - r->second, args.data() + r->second), bp);
+    } else {
+        unsigned sz = args.size() - r->second;
+        lean_assert(sz >= 2);
+        auto r = pp_coercion_fn(e, sz);
+        if (r.second < bp) {
+            return mk_result(paren(r.first));
+        } else {
+            return r;
+        }
+    }
 }
 
 auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index a673cdd84..b45f9cabe 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -59,6 +59,7 @@ private:
     format pp_binders(buffer<expr> const & locals);
     format pp_level(level const & l);
 
+    result pp_coercion_fn(expr const & e, unsigned sz);
     result pp_coercion(expr const & e, unsigned bp);
     result pp_child_core(expr const & e, unsigned bp);
     result pp_child(expr const & e, unsigned bp);
diff --git a/tests/lean/coe.lean b/tests/lean/coe.lean
new file mode 100644
index 000000000..cacb825bd
--- /dev/null
+++ b/tests/lean/coe.lean
@@ -0,0 +1,12 @@
+import logic
+
+set_option pp.notation false
+
+inductive Functor :=
+mk : (Π (A B : Type), A → B) → Functor
+
+definition Functor.to_fun [coercion] (f : Functor) {A B : Type} : A → B :=
+Functor.rec (λ f, f) f A B
+
+variable f : Functor
+check f 0 = 0
diff --git a/tests/lean/coe.lean.expected.out b/tests/lean/coe.lean.expected.out
new file mode 100644
index 000000000..d247d6be7
--- /dev/null
+++ b/tests/lean/coe.lean.expected.out
@@ -0,0 +1 @@
+eq (f 0) 0 : Prop