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

Add small trick to improve pretty printer performance. Now, deep.lean takes 0.140secs to be processed.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-21 22:54:58 -07:00
parent 56d2d2a112
commit eb4315baab
1 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/util/sexpr/format.cpp
View file

@ -157,6 +157,9 @@ format const & colon() {
format const & dot() {
return g_dot;
}
// Auxiliary flag used to mark whether flatten
// produce a different sexpr
static bool thread_local g_diff_flatten = false;
//
sexpr format::flatten(sexpr const & s) {
lean_assert(is_cons(s));
@ -175,8 +178,10 @@ sexpr format::flatten(sexpr const & s) {
}));
case format_kind::CHOICE:
/* flatten (x <|> y) = flatten x */
g_diff_flatten = true;
return flatten(sexpr_choice_1(s));
case format_kind::LINE:
g_diff_flatten = true;
return sexpr_text(sexpr(" "));
case format_kind::FLAT_COMPOSE:
case format_kind::TEXT:
@ -191,7 +196,15 @@ format format::flatten(format const & f){
return format(flatten(f.m_value));
}
format group(format const & f) {
return choice(format::flatten(f), f);
g_diff_flatten = false;
format flat_f = format::flatten(f);
if (g_diff_flatten) {
return choice(flat_f, f);
} else {
// flat_f and f are essentially the same format object.
// So, we don't need to create a choice.
return flat_f;
}
}
format above(format const & f1, format const & f2) {
return format{f1, line(), f2};