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

Add format tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-22 08:20:42 -07:00
parent 3c5f993191
commit 6272408f12
2 changed files with 27 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/tests/util/format.cpp
View file

@ -6,10 +6,12 @@ Author: Soonho Kong
*/ */
#include <vector> #include <vector>
#include <algorithm> #include <algorithm>
#include <sstream>
#include "format.h" #include "format.h"
#include "test.h" #include "test.h"
#include "sexpr_funcs.h" #include "sexpr_funcs.h"
#include "options.h" #include "options.h"
#include "mpq.h"
using namespace lean; using namespace lean;
using std::cout; using std::cout;
@ -98,9 +100,24 @@ static void tst3() {
cout << mk_pair(f1, options({"pp", "colors"}, false)) << "\n"; cout << mk_pair(f1, options({"pp", "colors"}, false)) << "\n";
} }
static void tst4() {
std::ostringstream s;
s << "(" << format() << ") ";
s << "(" << (format("foo") ^ format("bar")) << ") ";
s << pp(sexpr()) << " ";
s << pp(sexpr("test")) << " ";
sexpr s1(mpz(100));
sexpr s2(mpq(1,2));
sexpr s3{s1, s2};
s << pp(s3);
std::cout << s.str() << "\n";
lean_assert(s.str() == "() (foo bar) nil \"test\" (100 1/2)");
}
int main() { int main() {
tst1(); tst1();
tst2(); tst2();
tst3(); tst3();
tst4();
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }

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

@ -63,8 +63,8 @@ std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) {
case format::format_kind::CHOICE: case format::format_kind::CHOICE:
case format::format_kind::COMPOSE: case format::format_kind::COMPOSE:
case format::format_kind::FLAT_COMPOSE: case format::format_kind::FLAT_COMPOSE:
lean_unreachable(); lean_unreachable(); // LCOV_EXCL_LINE
break; break; // LCOV_EXCL_LINE
case format::format_kind::NIL: case format::format_kind::NIL:
out << ""; out << "";
@ -189,8 +189,8 @@ sexpr format::flatten(sexpr const & s) {
case format_kind::COLOR_END: case format_kind::COLOR_END:
return s; return s;
} }
lean_unreachable(); lean_unreachable(); // LCOV_EXCL_LINE
return s; return s; // LCOV_EXCL_LINE
} }
format format::flatten(format const & f){ format format::flatten(format const & f){
return format(flatten(f.m_value)); return format(flatten(f.m_value));
@ -296,8 +296,8 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
return space_upto_line_break(x, available, found_newline); return space_upto_line_break(x, available, found_newline);
} }
} }
lean_unreachable(); lean_unreachable(); // LCOV_EXCL_LINE
return 0; return 0; // LCOV_EXCL_LINE
} }
sexpr format::be(unsigned w, unsigned k, sexpr const & s) { sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
@ -352,8 +352,8 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
} }
} }
} }
lean_unreachable(); lean_unreachable(); // LCOV_EXCL_LINE
return sexpr(); return sexpr(); // LCOV_EXCL_LINE
} }
sexpr format::best(unsigned w, unsigned k, sexpr const & s) { sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
@ -423,8 +423,8 @@ struct sexpr_pp_fn {
} }
} }
}} }}
lean_unreachable(); lean_unreachable(); // LCOV_EXCL_LINE
return format(); return format(); // LCOV_EXCL_LINE
} }
format operator()(sexpr const & s) { format operator()(sexpr const & s) {