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

Restructure format, and fix bugs

Browse source
This commit is contained in:
Soonho Kong 2013-08-08 11:45:06 -07:00
parent fe9d2147d2
commit 9516d9f88f
2 changed files with 46 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

102
src/util/format.cpp
View file

@ -127,84 +127,71 @@ format wrap(format const & f1, format const & f2) {
f2}; f2};
} }
unsigned format::space_upto_line_break_list(sexpr const & r, bool & found) { unsigned format::space_upto_line_break_list(sexpr const & r, bool & found_newline) {
// r : list of (int * format) // r : list of (int * format)
lean_assert(!found); lean_assert(is_list(r));
if (is_nil(r)) { sexpr list = r;
found = true; unsigned len = 0;
return 0; while (!is_nil(list) && !found_newline) {
sexpr const & h = cdr(car(list));
len += space_upto_line_break(h, found_newline);
list = cdr(list);
} }
return format::space_upto_line_break(cdr(car(r)), cdr(r), found); return len;
} }
unsigned format::space_upto_line_break(sexpr const & s, sexpr const & r, bool & found) { unsigned format::space_upto_line_break(sexpr const & s, bool & found_newline) {
// s : format // s : format
// r : list of (int * format) lean_assert(!found_newline);
lean_assert(!found); lean_assert(sexpr_kind(s) <= format_kind::COLOR_END);
if(is_nil(s)) {
found = true;
return 0;
}
switch (sexpr_kind(s)) { switch (sexpr_kind(s)) {
case format_kind::NIL: case format_kind::NIL:
case format_kind::COLOR_BEGIN: case format_kind::COLOR_BEGIN:
case format_kind::COLOR_END: case format_kind::COLOR_END:
return 0 + space_upto_line_break_list(r, found); {
return 0;
}
case format_kind::COMPOSE: case format_kind::COMPOSE:
{ {
sexpr list = sexpr_compose_list(s); sexpr list = sexpr_compose_list(s);
unsigned len = 0; unsigned len = 0;
while(!is_nil(list) && !found) { while(!is_nil(list) && !found_newline) {
sexpr const & h = car(list); sexpr const & h = car(list);
list = cdr(list); list = cdr(list);
len += space_upto_line_break(h, nil(), found); len += space_upto_line_break(h, found_newline);
}
if (found) {
return len;
} else {
return len + space_upto_line_break_list(r, found);
} }
return len;
} }
case format_kind::NEST: case format_kind::NEST:
{ {
sexpr const & x = sexpr_nest_s(s); sexpr const & x = sexpr_nest_s(s);
unsigned len = space_upto_line_break(x, nil(), found); return space_upto_line_break(x, found_newline);
if (found) { }
return len; case format_kind::TEXT: {
} else { return sexpr_text_length(s);
return len + space_upto_line_break_list(r, found);
}
} }
case format_kind::TEXT:
return sexpr_text_length(s) + space_upto_line_break_list(r, found);
case format_kind::LINE: case format_kind::LINE:
found = true; found_newline = true;
return 0; return 0;
case format_kind::CHOICE: case format_kind::CHOICE:
{ {
sexpr const & x = sexpr_choice_1(s); sexpr const & x = sexpr_choice_2(s);
return space_upto_line_break(x, r, found); return space_upto_line_break(x, found_newline);
} }
} }
std::cerr << "!!!!!!!!!!!!!!!" << s << std::endl;
lean_unreachable(); lean_unreachable();
return 0; return 0;
} }
sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) { sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
/* be w k [] = Nil */ /* s = (i, v) :: z, where h has the type int x format */
/* ret = list of format */
if(is_nil(s)) { if(is_nil(s)) {
if(is_nil(r)) { return sexpr{};
// s == Nil && r == Nil
return sexpr();
} else {
// s == Nil && r != Nil
return be(w, k, car(r), cdr(r));
}
} }
/* s = (i, v) :: z, where h has the type int x format */
sexpr const & h = car(s); sexpr const & h = car(s);
sexpr const & z = cdr(s); sexpr const & z = cdr(s);
int i = to_int(car(h)); int i = to_int(car(h));
@ -212,40 +199,39 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) {
switch (sexpr_kind(v)) { switch (sexpr_kind(v)) {
case format_kind::NIL: case format_kind::NIL:
return be(w, k, z, r); return be(w, k, z);
case format_kind::COLOR_BEGIN: case format_kind::COLOR_BEGIN:
case format_kind::COLOR_END: case format_kind::COLOR_END:
return sexpr(v, be(w, k, z, r)); return sexpr(v, be(w, k, z));
case format_kind::COMPOSE: case format_kind::COMPOSE:
{ {
sexpr const & list = sexpr_compose_list(v); sexpr const & list = sexpr_compose_list(v);
sexpr const & list_ = map(list, sexpr const & list_ = foldr(list, z, [i](sexpr const & s, sexpr const & res) {
[i](sexpr const & s) { return sexpr(sexpr(i, s), res);
return sexpr(i, s); });
}); return be(w, k, list_);
return be(w, k, list_, sexpr(z, r));
} }
case format_kind::NEST: case format_kind::NEST:
{ {
int j = sexpr_nest_i(v); int j = sexpr_nest_i(v);
sexpr const & x = sexpr_nest_s(v); sexpr const & x = sexpr_nest_s(v);
return be(w, k, sexpr(sexpr(i + j, x), z), r); return be(w, k, sexpr(sexpr(i + j, x), z));
} }
case format_kind::TEXT: case format_kind::TEXT:
return sexpr(v, be(w, k + sexpr_text_length(v), z, r)); return sexpr(v, be(w, k + sexpr_text_length(v), z));
case format_kind::LINE: case format_kind::LINE:
return sexpr(v, sexpr(sexpr_text(std::string(i, ' ')), be(w, i, z, r))); return sexpr(v, sexpr(sexpr_text(std::string(i, ' ')), be(w, i, z)));
case format_kind::CHOICE: case format_kind::CHOICE:
{ {
sexpr const & x = sexpr_choice_1(v); sexpr const & x = sexpr_choice_1(v);
sexpr const & y = sexpr_choice_2(v);; sexpr const & y = sexpr_choice_2(v);;
bool found = false; bool found_newline = false;
int d = static_cast<int>(w) - static_cast<int>(k) - space_upto_line_break(x, r, found); int d = static_cast<int>(w) - static_cast<int>(k) - space_upto_line_break_list(sexpr(sexpr(i, x), z), found_newline);
if(d >= 0) { if(d >= 0) {
sexpr const & s1 = be(w, k, sexpr(sexpr(i, x), z), r); sexpr const & s1 = be(w, k, sexpr(sexpr(i, x), z));
return s1; return s1;
} }
sexpr const & s2 = be(w, k, sexpr(sexpr(i, y), z), r); sexpr const & s2 = be(w, k, sexpr(sexpr(i, y), z));
return s2; return s2;
} }
} }
@ -254,7 +240,7 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) {
} }
sexpr format::best(unsigned w, unsigned k, sexpr const & s) { sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
return be(w, k, sexpr{sexpr(0, s)}, sexpr()); return be(w, k, sexpr{sexpr(0, s)});
} }
std::ostream & operator<<(std::ostream & out, format const & f) std::ostream & operator<<(std::ostream & out, format const & f)

4
src/util/format.h
View file

@ -109,9 +109,9 @@ private:
} }
// Functions used inside of pretty printing // Functions used inside of pretty printing
static unsigned space_upto_line_break(sexpr const & s, sexpr const & r, bool & found);
static unsigned space_upto_line_break_list(sexpr const & r, bool & found); static unsigned space_upto_line_break_list(sexpr const & r, bool & found);
static sexpr be(unsigned w, unsigned k, sexpr const & s, sexpr const & r); static unsigned space_upto_line_break(sexpr const & s, bool & found);
static sexpr be(unsigned w, unsigned k, sexpr const & s);
static sexpr best(unsigned w, unsigned k, sexpr const & s); static sexpr best(unsigned w, unsigned k, sexpr const & s);
static bool is_fnil(format const & f) { static bool is_fnil(format const & f) {