From 56d2d2a112c8de004f0cdfe2eeab736fdb606e45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Aug 2013 22:45:48 -0700 Subject: [PATCH] Improve pretty printer performance for deep formulas and formats with long lines. Add example that demonstrates performance problem (before: 13 secs, after: 1 sec). Signed-off-by: Leonardo de Moura --- examples/deep.lean | 7 +++++ src/util/sexpr/format.cpp | 65 +++++++++++++++++++++++++-------------- src/util/sexpr/format.h | 15 ++++++--- 3 files changed, 60 insertions(+), 27 deletions(-) create mode 100644 examples/deep.lean diff --git a/examples/deep.lean b/examples/deep.lean new file mode 100644 index 0000000000..aefe0784ea --- /dev/null +++ b/examples/deep.lean @@ -0,0 +1,7 @@ +Definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x))) +Definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x +Definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x +Variable f : Int -> Int. +Set pp::width 80. +Set pp::lean::max_depth 2000. +Eval f3 f 0. \ No newline at end of file diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 22d948fad1..564f2368b1 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -62,6 +62,7 @@ std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) { case format::format_kind::NEST: case format::format_kind::CHOICE: case format::format_kind::COMPOSE: + case format::format_kind::FLAT_COMPOSE: lean_unreachable(); break; @@ -168,15 +169,16 @@ sexpr format::flatten(sexpr const & s) { return flatten(sexpr_nest_s(s)); case format_kind::COMPOSE: /* flatten (s_1 <> ... <> s_n ) = flatten s_1 <> ... <> flatten s_n */ - return sexpr_compose(map(sexpr_compose_list(s), - [](sexpr const & s) { - return flatten(s); - })); + return sexpr_flat_compose(map(sexpr_compose_list(s), + [](sexpr const & s) { + return flatten(s); + })); case format_kind::CHOICE: /* flatten (x <|> y) = flatten x */ return flatten(sexpr_choice_1(s)); case format_kind::LINE: return sexpr_text(sexpr(" ")); + case format_kind::FLAT_COMPOSE: case format_kind::TEXT: case format_kind::COLOR_BEGIN: case format_kind::COLOR_END: @@ -212,20 +214,33 @@ format wrap(format const & f1, format const & f2) { f2}; } -unsigned format::space_upto_line_break_list(sexpr const & r, bool & found_newline) { +struct space_exceeded {}; + +// Return true iff the space upto line break fits in the available space. +bool format::space_upto_line_break_list_exceeded(sexpr const & r, int available) { // r : list of (int * format) - lean_assert(is_list(r)); - sexpr list = r; - unsigned len = 0; - while (!is_nil(list) && !found_newline) { - sexpr const & h = cdr(car(list)); - len += space_upto_line_break(h, found_newline); - list = cdr(list); + try { + lean_assert(is_list(r)); + sexpr list = r; + bool found_newline = false; + while (!is_nil(list) && !found_newline) { + if (available < 0) + return true; + sexpr const & h = cdr(car(list)); + available -= space_upto_line_break(h, available, found_newline); + list = cdr(list); + } + return available < 0; + } catch (space_exceeded) { + return true; } - return len; + return false; } -unsigned format::space_upto_line_break(sexpr const & s, bool & found_newline) { +/** + \brief Return the space upto line break. If the space exceeds available, then throw an exception. +*/ +int format::space_upto_line_break(sexpr const & s, int available, bool & found_newline) { // s : format lean_assert(!found_newline); lean_assert(sexpr_kind(s) <= format_kind::COLOR_END); @@ -238,20 +253,23 @@ unsigned format::space_upto_line_break(sexpr const & s, bool & found_newline) { return 0; } case format_kind::COMPOSE: + case format_kind::FLAT_COMPOSE: { sexpr list = sexpr_compose_list(s); - unsigned len = 0; + int len = 0; while(!is_nil(list) && !found_newline) { sexpr const & h = car(list); list = cdr(list); - len += space_upto_line_break(h, found_newline); + len += space_upto_line_break(h, available, found_newline); + if (len > available) + throw space_exceeded(); } return len; } case format_kind::NEST: { sexpr const & x = sexpr_nest_s(s); - return space_upto_line_break(x, found_newline); + return space_upto_line_break(x, available, found_newline); } case format_kind::TEXT: { return sexpr_text_length(s); @@ -262,7 +280,7 @@ unsigned format::space_upto_line_break(sexpr const & s, bool & found_newline) { case format_kind::CHOICE: { sexpr const & x = sexpr_choice_2(s); - return space_upto_line_break(x, found_newline); + return space_upto_line_break(x, available, found_newline); } } lean_unreachable(); @@ -289,6 +307,7 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) { case format_kind::COLOR_END: return sexpr(v, be(w, k, z)); case format_kind::COMPOSE: + case format_kind::FLAT_COMPOSE: { sexpr const & list = sexpr_compose_list(v); sexpr const & list_ = foldr(list, z, [i](sexpr const & s, sexpr const & res) { @@ -310,14 +329,14 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) { { sexpr const & x = sexpr_choice_1(v); sexpr const & y = sexpr_choice_2(v);; - bool found_newline = false; - int d = static_cast(w) - static_cast(k) - space_upto_line_break_list(sexpr(sexpr(i, x), z), found_newline); - if(d >= 0) { + int available = static_cast(w) - static_cast(k); + if (!space_upto_line_break_list_exceeded(sexpr(sexpr(i, x), z), available)) { sexpr const & s1 = be(w, k, sexpr(sexpr(i, x), z)); return s1; + } else { + sexpr const & s2 = be(w, k, sexpr(sexpr(i, y), z)); + return s2; } - sexpr const & s2 = be(w, k, sexpr(sexpr(i, y), z)); - return s2; } } lean_unreachable(); diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 04673f7bb4..95c1b3a26a 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -32,7 +32,7 @@ class options; class format { public: - enum format_kind { NIL, NEST, COMPOSE, CHOICE, LINE, TEXT, COLOR_BEGIN, COLOR_END}; + enum format_kind { NIL, NEST, COMPOSE, FLAT_COMPOSE, CHOICE, LINE, TEXT, COLOR_BEGIN, COLOR_END}; enum format_color {RED, GREEN, ORANGE, BLUE, PINK, CYAN, GREY}; private: sexpr m_value; @@ -48,11 +48,15 @@ private: lean_assert(is_list(l)); return sexpr(sexpr(format_kind::COMPOSE), l); } + static inline sexpr sexpr_flat_compose(sexpr const & l) { + lean_assert(is_list(l)); + return sexpr(sexpr(format_kind::FLAT_COMPOSE), l); + } static inline sexpr sexpr_compose(std::initializer_list const & l) { return sexpr_compose(sexpr(l)); } static inline sexpr const & sexpr_compose_list(sexpr const & s) { - lean_assert(sexpr_kind(s) == format_kind::COMPOSE); + lean_assert(sexpr_kind(s) == format_kind::COMPOSE || sexpr_kind(s) == format_kind::FLAT_COMPOSE); return cdr(s); } static inline sexpr sexpr_choice(sexpr const & s1, sexpr const & s2) { @@ -117,8 +121,8 @@ private: } // Functions used inside of pretty printing - static unsigned space_upto_line_break_list(sexpr const & r, bool & found); - static unsigned space_upto_line_break(sexpr const & s, bool & found); + static bool space_upto_line_break_list_exceeded(sexpr const & r, int available); + static int space_upto_line_break(sexpr const & s, int available, bool & found); static sexpr be(unsigned w, unsigned k, sexpr const & s); static sexpr best(unsigned w, unsigned k, sexpr const & s); @@ -128,6 +132,9 @@ private: static bool is_compose(format const & f) { return to_int(car(f.m_value)) == format_kind::COMPOSE; } + static bool is_flat_compose(format const & f) { + return to_int(car(f.m_value)) == format_kind::FLAT_COMPOSE; + } static bool is_nest(format const & f) { return to_int(car(f.m_value)) == format_kind::NEST; }