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

Add cmp (total order) for sexpr

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-21 17:05:32 -07:00
parent f6e18045f3
commit 24cf1a7c3d
3 changed files with 50 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/sexpr/sexpr.cpp
View file

@ -189,9 +189,32 @@ bool operator==(sexpr const & a, sexpr const & b) {
return false;
}
bool operator<(sexpr const & a, sexpr const & b) {
// TODO
return false;
int cmp(sexpr const & a, sexpr const & b) {
if (eqp(a, b))
return 0;
sexpr::kind ka = a.get_kind();
sexpr::kind kb = b.get_kind();
if (ka != kb)
return ka < kb ? -1 : 1;
if (a.hash() == b.hash()) {
if (a == b)
return 0;
}
switch (ka) {
case sexpr::kind::NIL: return 0;
case sexpr::kind::STRING: return strcmp(to_string(a).c_str(), to_string(b).c_str());
case sexpr::kind::INT: return to_int(a) == to_int(b) ? 0 : (to_int(a) < to_int(b) ? -1 : 1);
case sexpr::kind::DOUBLE: return to_double(a) == to_double(b) ? 0 : (to_double(a) < to_double(b) ? -1 : 1);
case sexpr::kind::NAME: return cmp(to_name(a), to_name(b));
case sexpr::kind::MPZ: return cmp(to_mpz(a), to_mpz(b));
case sexpr::kind::MPQ: return cmp(to_mpq(a), to_mpq(b));
case sexpr::kind::CONS: {
int r = cmp(head(a), head(b));
if (r != 0)
return r;
return cmp(tail(a), tail(b));
}}
return 0;
}
std::ostream & operator<<(std::ostream & out, sexpr const & s) {

9
src/sexpr/sexpr.h
View file

@ -116,9 +116,10 @@ template<typename T> inline bool operator==(T const & a, sexpr const & b) { retu
inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == b); }
template<typename T> inline bool operator!=(sexpr const & a, T const & b) { return !(a == b); }
template<typename T> inline bool operator!=(T const & a, sexpr const & b) { return !(a == b); }
bool operator<(sexpr const & a, sexpr const & b);
inline bool operator>(sexpr const & a, sexpr const & b) { return b < a; }
inline bool operator<=(sexpr const & a, sexpr const & b) { return !(a > b); }
inline bool operator>=(sexpr const & a, sexpr const & b) { return !(a < b); }
int cmp(sexpr const & a, sexpr const & b);
inline bool operator<(sexpr const & a, sexpr const & b) { return cmp(a, b) < 0; }
inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0; }
inline bool operator<=(sexpr const & a, sexpr const & b) { return cmp(a, b) <= 0; }
inline bool operator>=(sexpr const & a, sexpr const & b) { return cmp(a, b) >= 0; }
}

19
src/tests/sexpr/sexpr.cpp
View file

@ -119,10 +119,29 @@ static void tst3() {
lean_assert(sum == 10);
}
static void tst4() {
lean_assert(sexpr(1) < sexpr(2));
lean_assert(sexpr() < sexpr(2));
lean_assert(sexpr("foo") < sexpr(2));
lean_assert(sexpr(3) > sexpr(2));
lean_assert(sexpr(2) < sexpr(1.0));
lean_assert(sexpr("foo") < sexpr(name("foo")));
lean_assert(!(sexpr(name("foo")) < sexpr(name("foo"))));
auto e = sexpr(1);
lean_assert(e == e);
lean_assert((sexpr{1, 2, 3}) <= (sexpr{1, 2, 3}));
lean_assert((sexpr{1, 2, 3}) >= (sexpr{1, 2, 3}));
lean_assert((sexpr{1, 1, 3}) < (sexpr{1, 2, 3}));
lean_assert((sexpr{2, 1, 3}) > (sexpr{1, 2, 3}));
lean_assert((sexpr{2, 1, 3}) > (sexpr("foo")));
lean_assert(sexpr(1, 2) > sexpr(0, 1));
}
int main() {
continue_on_violation(true);
tst1();
tst2();
tst3();
tst4();
return has_violations() ? 1 : 0;
}