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

@@ -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;

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),

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 */

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; }
 };

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; }
 };

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; }
 };

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