From 4d4bc0551ff2dd4f03916e1c8eaacac54ded3cc1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Oct 2014 13:08:15 -0700 Subject: [PATCH] feat(frontends/lean/pp): minimize number of spaces when pretty printing notation --- src/frontends/lean/pp.cpp | 26 ++++++++++++++++++++++---- tests/lean/notation3.lean.expected.out | 8 ++++---- tests/lean/notation4.lean.expected.out | 8 ++++---- tests/lean/t10.lean.expected.out | 4 ++-- tests/lean/t11.lean.expected.out | 4 ++-- 5 files changed, 34 insertions(+), 16 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 965901054..e093c4aeb 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -691,6 +691,13 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> } } +static bool add_extra_space(name const & tk) { + // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra + // spaces should be added or not when pretty printing notation. + // We should implement a better solution in the future. + return tk != "," && tk != "(" && tk != ")"; +} + auto pretty_fn::pp_notation(notation_entry const & entry, buffer> & args) -> optional { if (entry.is_numeral()) { return some(result(format(entry.get_num()))); @@ -703,7 +710,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> unsigned i = ts.size(); unsigned last_rbp = max_bp()-1; unsigned token_lbp = 0; - bool last = true; + bool extra_space = false; + bool last = true; while (i > 0) { --i; format curr; @@ -723,7 +731,10 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> args.pop_back(); result e_r = pp_notation_child(e, token_lbp, a.rbp()); format e_fmt = e_r.fmt(); - curr = format(tk) + space() + e_fmt; + curr = format(tk); + if (add_extra_space(tk)) + curr = curr + space(); + curr = curr + e_fmt; if (last) last_rbp = a.rbp(); break; @@ -764,6 +775,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> unsigned curr_lbp = token_lbp; if (auto t = a.get_terminator()) { curr = format(*t); + if (add_extra_space(*t)) + curr = space() + curr; curr_lbp = get_some_precedence(m_token_table, *t); } unsigned i = rec_args.size(); @@ -774,7 +787,9 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> result arg_res = pp_notation_child(rec_args[i], curr_lbp, a.rbp()); if (i == 0) sep_fmt = format(tk); - curr = sep_fmt + space() + arg_res.fmt() + space() + curr; + curr = sep_fmt + space() + arg_res.fmt() + curr; + if (i > 0 && add_extra_space(a.get_sep())) + curr = space() + curr; curr_lbp = sep_lbp; } break; @@ -836,8 +851,11 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> fmt = curr; last = false; } else { - fmt = curr + space() + fmt; + if (extra_space) + curr = curr + space(); + fmt = curr + fmt; } + extra_space = add_extra_space(tk); } unsigned first_lbp = token_lbp; if (!entry.is_nud()) { diff --git a/tests/lean/notation3.lean.expected.out b/tests/lean/notation3.lean.expected.out index 9c3da25ea..23662a4fc 100644 --- a/tests/lean/notation3.lean.expected.out +++ b/tests/lean/notation3.lean.expected.out @@ -1,5 +1,5 @@ notation3.lean:2:0: warning: imported file uses 'sorry' -[ a , b , b ] : list num -( a , true , a = b , b ) : num × Prop × Prop × num -( a , b ) : num × num -[ 1 , 2 + 2 , 3 ] : list num +[ a, b, b ] : list num +(a, true, a = b, b) : num × Prop × Prop × num +(a, b) : num × num +[ 1, 2 + 2, 3 ] : list num diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out index 93f054583..33ced8645 100644 --- a/tests/lean/notation4.lean.expected.out +++ b/tests/lean/notation4.lean.expected.out @@ -1,5 +1,5 @@ notation4.lean:2:0: warning: imported file uses 'sorry' -∃ (A : Type₁) (x y : A) , x = y : Prop -∃ (x : num) , x = 0 : Prop -Σ (x : num) , x = 10 : Type₁ -Σ (A : Type₁) , list A : Type₂ +∃ (A : Type₁) (x y : A), x = y : Prop +∃ (x : num), x = 0 : Prop +Σ (x : num), x = 10 : Type₁ +Σ (A : Type₁), list A : Type₂ diff --git a/tests/lean/t10.lean.expected.out b/tests/lean/t10.lean.expected.out index de918b25c..c32b625e6 100644 --- a/tests/lean/t10.lean.expected.out +++ b/tests/lean/t10.lean.expected.out @@ -7,6 +7,6 @@ has type B but is expected to have type N -[ x , y , z , x , y , y ] : list -[ x ] : list +[ x, y, z, x, y, y ] : list +[ x ] : list [ ] : list diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out index d6f8a97a8..43663bc41 100644 --- a/tests/lean/t11.lean.expected.out +++ b/tests/lean/t11.lean.expected.out @@ -1,3 +1,3 @@ -∃ (x : A) , p x : bool -∃ (x y : A) , q x y : bool +∃ (x : A), p x : bool +∃ (x y : A), q x y : bool λ (x : A), x : A → A