From aa99ac66184951e6e8087eff0479601d91f46736 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Oct 2013 11:42:23 -0700
Subject: [PATCH] feat(kernel/value): allow semantic attachments to use
 coercions when being pretty printed

For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp          | 4 ++--
 src/kernel/expr.cpp                | 2 +-
 src/kernel/expr.h                  | 2 +-
 src/library/arith/int.cpp          | 9 +++++++--
 src/library/arith/nat.cpp          | 2 +-
 src/library/arith/real.cpp         | 9 +++++++--
 tests/lean/subst.lean.expected.out | 2 +-
 7 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4e4dea7d9..275b252fe 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -248,7 +248,7 @@ class pp_fn {
         if (has_implicit_arguments(v.get_name())) {
             return mk_result(format(m_frontend.get_explicit_version(v.get_name())), 1);
         } else {
-            return mk_result(v.pp(m_unicode), 1);
+            return mk_result(v.pp(m_unicode, m_coercion), 1);
         }
     }
 
@@ -699,7 +699,7 @@ class pp_fn {
             if (is_constant(f))
                 p = mk_result(format(const_name(f)), 1);
             else if (is_value(f))
-                p = mk_result(to_value(f).pp(m_unicode), 1);
+                p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1);
             else
                 p = pp_child(f, depth);
             bool simple     = is_constant(f) && const_name(f).size() <= m_indent + 4;
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index dfc7ece40..5298ee8a7 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -127,7 +127,7 @@ bool value::operator<(value const & other) const {
         return get_name() < other.get_name();
 }
 format value::pp() const { return format(get_name()); }
-format value::pp(bool unicode) const { return unicode ? format(get_unicode_name()) : pp(); }
+format value::pp(bool unicode, bool) const { return unicode ? format(get_unicode_name()) : pp(); }
 unsigned value::hash() const { return get_name().hash(); }
 expr_value::expr_value(value & v):
     expr_cell(expr_kind::Value, v.hash(), false),
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index ee991067c..a70f14b19 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -244,7 +244,7 @@ public:
     bool operator<(value const & other) const;
     virtual void display(std::ostream & out) const;
     virtual format pp() const;
-    virtual format pp(bool unicode) const;
+    virtual format pp(bool unicode, bool coercion) const;
     virtual unsigned hash() const;
 };
 /** \brief Semantic attachments */
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index 6272c93ac..b83243bef 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -37,8 +37,13 @@ public:
         return _other && _other->m_val == m_val;
     }
     virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp() const { return pp(false, false); }
+    virtual format pp(bool unicode, bool coercion) const {
+        if (coercion)
+            return format{to_value(mk_nat_to_int_fn()).pp(unicode, coercion), space(), format(m_val)};
+        else
+            return format(m_val);
+    }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index 8a3be0081..8d172a5c2 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -37,7 +37,7 @@ public:
     }
     virtual void display(std::ostream & out) const { out << m_val; }
     virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp(bool, bool) const { return pp(); }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index cc94fbe65..fd0c3182f 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -40,8 +40,13 @@ public:
         return _other && _other->m_val == m_val;
     }
     virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp() const { return pp(false, false); }
+    virtual format pp(bool, bool coercion) const {
+        if (coercion)
+            return format{format(const_name(mk_nat_to_real_fn())), space(), format(m_val)};
+        else
+            return format(m_val);
+    }
     virtual unsigned hash() const { return m_val.hash(); }
     mpq const & get_num() const { return m_val; }
 };
diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out
index 8c36261b2..c377c8af2 100644
--- a/tests/lean/subst.lean.expected.out
+++ b/tests/lean/subst.lean.expected.out
@@ -9,4 +9,4 @@
   Set: lean::pp::notation
   Set: lean::pp::implicit
 Theorem T : eq::explicit ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
-    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == 10) H1 H2
+    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == nat_to_int 10) H1 H2