From aff7ceadee37db72f0763434f97e3f8ecae8e729 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 16 Apr 2016 17:34:43 -0700
Subject: [PATCH] feat(src/frontends/lean/pp): look at pp.proofs when pp-ing
 coercions

---
 src/frontends/lean/pp.cpp                      | 14 ++++++++++----
 tests/lean/pp_proofs_coercions.lean            | 18 ++++++++++++++++++
 .../lean/pp_proofs_coercions.lean.expected.out |  6 ++++++
 3 files changed, 34 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/pp_proofs_coercions.lean
 create mode 100644 tests/lean/pp_proofs_coercions.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index d1dc5dcc65..d8f0ed8fba 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -387,7 +387,10 @@ bool pretty_fn::is_prop(expr const & e) {
 
 auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
     if (sz == 1) {
-        return pp_child(app_arg(e), max_bp()-1, ignore_hide);
+        expr arg = app_arg(e);
+        if (auto thm = arg_is_proof(app_fn(e)))
+            arg = mk_inaccessible(*thm);
+        return pp_child(arg, max_bp()-1, ignore_hide);
     } else if (is_app(e) && is_implicit(app_fn(e))) {
         return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
     } else {
@@ -396,7 +399,10 @@ auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) ->
         format fn_fmt   = res_fn.fmt();
         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(), ignore_hide);
+        expr arg = app_arg(e);
+        if (auto thm = arg_is_proof(fn))
+            arg = mk_inaccessible(*thm);
+        result res_arg  = pp_child(arg, max_bp(), ignore_hide);
         return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
     }
 }
@@ -554,10 +560,10 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul
             return pp_abbreviation(e, *it, true, bp, ignore_hide);
         } else if (is_implicit(f)) {
             return pp_child(f, bp, ignore_hide);
-        } else if (auto thm = arg_is_proof(f)) {
-            return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide);
         } else if (!m_coercion && is_coercion(m_env, get_app_fn(e))) {
             return pp_coercion(e, bp, ignore_hide);
+        } else if (auto thm = arg_is_proof(f)) {
+            return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide);
         }
     }
     return pp_child_core(e, bp, ignore_hide);
diff --git a/tests/lean/pp_proofs_coercions.lean b/tests/lean/pp_proofs_coercions.lean
new file mode 100644
index 0000000000..bb158b7381
--- /dev/null
+++ b/tests/lean/pp_proofs_coercions.lean
@@ -0,0 +1,18 @@
+constants (A : Type) (B : A → Type) (C : Π a, B a → Type)
+constants (f : Π a b, C a b → (true → true))
+attribute f [coercion]
+
+print coercions
+
+constants (a : A) (b : B a) (c : C a b)
+
+definition messy₁ := f a b c
+definition messy₂ := f a b c trivial
+
+eval messy₁
+eval messy₂
+
+set_option pp.proofs false
+
+eval messy₁
+eval messy₂
diff --git a/tests/lean/pp_proofs_coercions.lean.expected.out b/tests/lean/pp_proofs_coercions.lean.expected.out
new file mode 100644
index 0000000000..ae220d49d6
--- /dev/null
+++ b/tests/lean/pp_proofs_coercions.lean.expected.out
@@ -0,0 +1,6 @@
+C ↣ _Fun : f
+C ↣ [fun-class] : f
+c
+c trivial
+c
+c ⌞true⌟