michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add more to expr pretty-print

Browse source
This commit is contained in:
Soonho Kong 2013-08-01 18:54:06 -07:00
parent 229b4f8759
commit 322c2b472d
2 changed files with 31 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/kernel/expr.cpp
View file

@ -195,37 +195,38 @@ lean::format pp_aux(lean::expr const & a) {
return format(const_name(a));
case expr_kind::App:
{
format r("(");
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;
return paren(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(")")};
return paren(format{
highlight(format("\u03BB "), format::format_color::PINK), /* Use unicode lambda */
paren(format{
format(abst_name(a)),
format(" : "),
pp_aux(abst_type(a))}),
format(" "),
pp_aux(abst_body(a))});
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(")")};
return paren(format{
highlight(format("\u03A0 "), format::format_color::ORANGE), /* Use unicode lambda */
paren(format{
format(abst_name(a)),
format(" : "),
pp_aux(abst_type(a))}),
format(" "),
pp_aux(abst_body(a))});
case expr_kind::Type:
{
std::stringstream ss;
ss << ty_level(a);
return format{format("(Type "),
format(ss.str()),
format(")")};
return paren(format{format("Type "),
format(ss.str())});
}
case expr_kind::Numeral:
return format(num_value(a));

10
src/tests/kernel/expr.cpp
View file

@ -190,6 +190,12 @@ void tst5() {
expr r2 = max_sharing(r1);
std::cout << "count(r1): " << count(r1) << "\n";
std::cout << "count(r2): " << count(r2) << "\n";
std::cout << "r1 = " << std::endl;
pp(r1);
std::cout << std::endl;
std::cout << "r2 = " << std::endl;
pp(r2);
std::cout << std::endl;
lean_assert(r1 == r2);
}
{
@ -251,6 +257,10 @@ void tst8() {
r = lambda("y", p, app(lambda("x", p, var(0)), var(1)));
lean_assert(!closed(r));
lean_assert(closed(lambda("z", p, r)));
pp(lambda("y", p, app(lambda("x", p, y), var(0)))); std::cout << std::endl;
pp(pi("x", p, f(f(f(a))))); std::cout << std::endl;
}
void tst9() {