Add pp to expr

src/kernel/expr.cpp

@@ -3,11 +3,14 @@ Copyright (c) 2013 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
+        Soonho Kong
 */
 #include <vector>
+#include <sstream>
 #include "expr.h"
 #include "sets.h"
 #include "hash.h"
+#include "format.h"
 
 namespace lean {
 
@@ -183,4 +186,55 @@ expr copy(expr const & a) {
 }
 }
 
-void pp(lean::expr const & e) { std::cout << e << std::endl; }
+lean::format pp_aux(lean::expr const & a) {
+    using namespace lean;
+    switch (a.kind()) {
+    case expr_kind::Var:
+        return format{format("#"), format(static_cast<int>(var_idx(a)))};
+    case expr_kind::Constant:
+        return format(const_name(a));
+    case expr_kind::App:
+    {
+        format r("(");
+        for (unsigned i = 0; i < num_args(a); i++) {
+            if (i > 0) r += format(" ");
+            r += pp_aux(arg(a, i));
+        }
+        r += format(")");
+        return r;
+    }
+    case expr_kind::Lambda:
+        return format{format("(\u03BB ("), /* Use unicode lambda */
+                format(abst_name(a)),
+                format(" : "),
+                pp_aux(abst_type(a)),
+                format(") "),
+                pp_aux(abst_body(a)),
+                format(")")};
+    case expr_kind::Pi:
+        return format{format("(\u03A0 ("), /* Use unicode Pi */
+                format(abst_name(a)),
+                format(" : "),
+                pp_aux(abst_type(a)),
+                format(") "),
+                pp_aux(abst_body(a)),
+                format(")")};
+    case expr_kind::Type:
+    {
+        std::stringstream ss;
+        ss << ty_level(a);
+        return format{format("(Type "),
+                format(ss.str()),
+                format(")")};
+    }
+    case expr_kind::Numeral:
+        return format(num_value(a));
+    }
+    lean_unreachable();
+    return format();
+}
+
+void pp(lean::expr const & a) {
+    lean::format const & f = pp_aux(a);
+    std::cout << f;
+}

src/kernel/expr.h

@@ -365,3 +365,4 @@ template<typename F> expr update_abst(expr const & e, F f) {
 }
 // =======================================
 }
+void pp(lean::expr const & a);

src/tests/kernel/expr.cpp

@@ -3,6 +3,7 @@ Copyright (c) 2013 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
+        Soonho Kong
 */
 #include <algorithm>
 #include "expr.h"
@@ -36,6 +37,22 @@ void tst1() {
     std::cout << pi("x", ty, var(0)) << "\n";
 }
 
+void tst1_pp() {
+    std::cerr << "=============== PP =====================\n";
+    expr a;
+    a = numeral(mpz(10));
+    expr f;
+    f = var(0);
+    expr fa = f(a);
+    expr ty = type(level());
+    pp(fa(a)); std::cout << "\n";
+    pp(fa(fa, fa)); std::cout << "\n";
+    pp(lambda("x", ty, var(0))); std::cout << "\n";
+    pp(pi("x", ty, var(0))); std::cout << "\n";
+    std::cerr << "=============== PP =====================\n";
+}
+
+
 expr mk_dag(unsigned depth, bool _closed = false) {
     expr f = constant("f");
     expr a = _closed ? constant("a") : var(0);
@@ -321,6 +338,7 @@ int main() {
     std::cout << "sizeof(expr_app):  " << sizeof(expr_app) << "\n";
     std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";
     tst1();
+    tst1_pp();
     tst2();
     tst3();
     tst4();