max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/pp): pretty print let-expressions

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-25 14:04:28 -07:00
parent e82cb6393f
commit 76e2f92d9c
4 changed files with 52 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/frontends/lean/pp.cpp
View file

@ -864,7 +864,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
}
}
auto pretty_fn::pp_let(expr e) -> result {
/* TODO(Leo): delete after lean3 is done */
auto pretty_fn::pp_let_macro(expr e) -> result {
buffer<pair<name, expr>> decls;
while (true) {
if (!is_let_macro(e))
@ -901,6 +902,42 @@ auto pretty_fn::pp_let(expr e) -> result {
return result(0, r);
}
auto pretty_fn::pp_let(expr e) -> result {
buffer<std::tuple<expr, expr, expr>> decls;
while (true) {
expr t = let_type(e);
expr v = let_value(e);
expr b = let_body(e);
auto p = let_body_fresh(e, true);
decls.emplace_back(p.second, t, v);
e = p.first;
if (!is_let(e))
break;
}
lean_assert(!decls.empty());
format r = *g_let_fmt;
unsigned sz = decls.size();
for (unsigned i = 0; i < sz; i++) {
expr l, t, v;
std::tie(l, t, v) = decls[i];
name const & n = local_pp_name(l);
format beg = i == 0 ? space() : line();
format sep = i < sz - 1 ? comma() : format();
format entry = format(n);
format v_fmt = pp_child(v, 0).fmt();
if (is_neutral_expr(t)) {
entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
} else {
format t_fmt = pp_child(t, 0).fmt();
entry += space() + colon() + space() + t_fmt + space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
}
r += nest(3 + 1, beg + group(entry));
}
format b = pp_child(e, 0).fmt();
r += line() + *g_in_fmt + space() + nest(2 + 1, b);
return result(0, r);
}
auto pretty_fn::pp_num(mpz const & n) -> result {
return result(format(n));
}
@ -1307,7 +1344,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
if (is_placeholder(e)) return result(*g_placeholder_fmt);
if (is_show(e)) return pp_show(e);
if (is_have(e)) return pp_have(e);
if (is_let_macro(e)) return pp_let(e);
if (is_let_macro(e)) return pp_let_macro(e);
if (is_typed_expr(e)) return pp(get_typed_expr_expr(e));
if (is_let_value(e)) return pp(get_let_value_expr(e));
if (m_num_nat_coe)
@ -1326,9 +1363,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
case expr_kind::Lambda: return pp_lambda(e);
case expr_kind::Pi: return pp_pi(e);
case expr_kind::Macro: return pp_macro(e);
case expr_kind::Let:
// NOT IMPLEMENTED YET
lean_unreachable();
case expr_kind::Let: return pp_let(e);
}
lean_unreachable(); // LCOV_EXCL_LINE
}

1
src/frontends/lean/pp.h
View file

@ -118,6 +118,7 @@ private:
result pp_show(expr const & e);
result pp_macro(expr const & e);
result pp_explicit(expr const & e);
result pp_let_macro(expr e);
result pp_let(expr e);
result pp_num(mpz const & n);
// If fn is true, then \c e is of the form (f a), and the abbreviation is \c f.

10
src/library/print.cpp
View file

@ -72,6 +72,16 @@ pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
return mk_pair(instantiate(binding_body(b), c), c);
}
pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type) {
lean_assert(is_let(b));
name n = let_name(b);
if (is_internal_name(n))
n = *g_x;
n = pick_unused_name(let_body(b), n);
expr c = mk_local(n, preserve_type ? let_type(b) : expr());
return mk_pair(instantiate(let_body(b), c), c);
}
name fix_internal_name(name const & a) {
if (a.is_atomic()) {
if (a.is_numeral())

1
src/library/print.h
View file

@ -19,6 +19,7 @@ name pick_unused_name(expr const & t, name const & s);
\remark If preserve_type is false, then the local constant will not use binding_domain.
*/
pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type = false);
pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type = false);
/** \brief Create a simple formatter object based on operator for "print" procedure.