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

Add sexpr tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-22 08:30:52 -07:00
parent 6272408f12
commit 1b5fcb80ee
2 changed files with 34 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/tests/util/sexpr.cpp
View file

@ -174,6 +174,34 @@ static void tst7() {
std::cout << mk_pair(f, update(options({"pp", "width"}, 1000), {"pp", "colors"}, false)) << "\n";
}
static void tst8() {
lean_assert(!(sexpr("foo") == sexpr(10)));
lean_assert(sexpr() == sexpr());
lean_assert(sexpr(true) == sexpr(true));
lean_assert(sexpr(false) != sexpr(true));
sexpr s1(10);
sexpr s2 = s1;
lean_assert(cmp(s1, s2) == 0);
lean_assert(cmp(s1, sexpr(20)) < 0);
lean_assert(cmp(sexpr(), sexpr()) == 0);
lean_assert(cmp(sexpr("aaa"), sexpr("aaa")) == 0);
lean_assert(cmp(sexpr("bbb"), sexpr("aaa")) > 0);
lean_assert(cmp(sexpr(true), sexpr(true)) == 0);
lean_assert(cmp(sexpr(true), sexpr(false)) > 0);
lean_assert(cmp(sexpr(false), sexpr(true)) < 0);
lean_assert(cmp(sexpr(1.0), sexpr(2.0)) < 0);
lean_assert(cmp(sexpr(name("aaa")), sexpr(name("aaa"))) == 0);
lean_assert(cmp(sexpr(name("aaa")), sexpr(name("bbb"))) < 0);
lean_assert(cmp(sexpr(mpz(10)), sexpr(mpz(10))) == 0);
lean_assert(cmp(sexpr(mpz(20)), sexpr(mpz(10))) > 0);
lean_assert(cmp(sexpr(mpq(1,2)), sexpr(mpq(1,2))) == 0);
lean_assert(cmp(sexpr(mpq(1,3)), sexpr(mpq(1,2))) < 0);
std::ostringstream s;
s << sexpr() << " " << sexpr(mpq(1,2));
std::cout << s.str() << "\n";
lean_assert(s.str() == "nil 1/2");
}
int main() {
tst1();
tst2();
@ -182,5 +210,6 @@ int main() {
tst5();
tst6();
tst7();
tst8();
return has_violations() ? 1 : 0;
}

9
src/util/sexpr/sexpr.cpp
View file

@ -95,7 +95,7 @@ struct sexpr_cons : public sexpr_cell {
void sexpr_cell::dealloc() {
switch (m_kind) {
case sexpr_kind::NIL: lean_unreachable(); break;
case sexpr_kind::NIL: lean_unreachable(); break; // LCOV_EXCL_LINE
case sexpr_kind::STRING: delete static_cast<sexpr_string*>(this); break;
case sexpr_kind::BOOL: delete static_cast<sexpr_bool*>(this); break;
case sexpr_kind::INT: delete static_cast<sexpr_int*>(this); break;
@ -192,7 +192,8 @@ bool operator==(sexpr const & a, sexpr const & b) {
case sexpr_kind::MPQ: return to_mpq(a) == to_mpq(b);
case sexpr_kind::CONS: return head(a) == head(b) && tail(a) == tail(b);
}
return false;
lean_unreachable(); // LCOV_EXCL_LINE
return false; // LCOV_EXCL_LINE
}
int cmp(sexpr const & a, sexpr const & b) {
@ -221,7 +222,8 @@ int cmp(sexpr const & a, sexpr const & b) {
return r;
return cmp(tail(a), tail(b));
}}
return 0;
lean_unreachable(); // LCOV_EXCL_LINE
return 0; // LCOV_EXCL_LINE
}
std::ostream & operator<<(std::ostream & out, sexpr const & s) {
@ -258,7 +260,6 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(a) == b; }
bool operator==(sexpr const & a, mpz const & b) { return is_mpz(a) && to_mpz(a) == b; }
bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a) == b; }
}
void print(lean::sexpr const & n) { std::cout << n << "\n"; }