Add useful goodies for S-expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/sexpr/CMakeLists.txt

@@ -1,2 +1,2 @@
-add_library(sexpr sexpr.cpp)
+add_library(sexpr sexpr.cpp sexpr_funcs.cpp)
 target_link_libraries(sexpr ${EXTRA_LIBS})

src/sexpr/sexpr.h

@@ -112,8 +112,14 @@ unsigned length(sexpr const & s);
 inline unsigned len(sexpr const & s) { return length(s); }
 
 bool operator==(sexpr const & a, sexpr const & b);
+inline bool operator==(sexpr const & a, int b) { return is_int(a) && to_int(a) == b; }
+inline bool operator==(sexpr const & a, double b) { return is_double(a) && to_double(a) == b; }
+inline bool operator==(sexpr const & a, std::string const & b) { return is_string(a) && to_string(a) == b; }
+inline bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(a) == b; }
+inline bool operator==(sexpr const & a, mpz const & b) { return is_mpz(a) && to_mpz(a) == b; }
+inline bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a) == b; }
+template<typename T> inline bool operator!=(sexpr const & a, T const & b) { return !(a == b); }
 bool operator<(sexpr const & a, sexpr const & b);
-inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == 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); }

src/sexpr/sexpr_funcs.cpp

@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "sexpr_funcs.h"
+
+namespace lean {
+
+sexpr append(sexpr const & l1, sexpr const & l2) {
+    lean_assert(is_list(l1));
+    if (is_nil(l1))
+        return l2;
+    else
+        return sexpr(head(l1), append(tail(l1), l2));
+}
+
+sexpr reverse_it(sexpr const & a, sexpr const & l) {
+    if (is_nil(l))
+        return a;
+    else
+        return reverse_it(sexpr(head(l), a), tail(l));
+}
+
+sexpr reverse(sexpr const & l) {
+    return reverse_it(nil(), l);
+}
+
+}

src/sexpr/sexpr_funcs.h

@@ -0,0 +1,68 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "sexpr.h"
+#include "debug.h"
+
+namespace lean {
+
+template<typename F>
+sexpr map(sexpr const & l, F f) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return l;
+    }
+    else {
+        lean_assert(is_cons(l));
+        return sexpr(f(head(l)), map(tail(l), f));
+    }
+}
+
+template<typename P>
+sexpr filter(sexpr const & l, P p) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return l;
+    }
+    else {
+        lean_assert(is_cons(l));
+        if (p(head(l)))
+            return sexpr(head(l), filter(tail(l), p));
+        else
+            return filter(tail(l), p);
+    }
+}
+
+template<typename P>
+bool contains(sexpr const & l, P p) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return false;
+    }
+    else {
+        lean_assert(is_cons(l));
+        return p(head(l)) || contains(tail(l), p);
+    }
+}
+
+template<typename T>
+bool member(T const & e, sexpr const & l) {
+    lean_assert(is_list(l));
+    sexpr const * curr = &l;
+    while (!is_nil(*curr)) {
+        if (head(*curr) == e)
+            return true;
+        curr = &tail(*curr);
+    }
+    return false;
+}
+
+sexpr append(sexpr const & l1, sexpr const & l2);
+
+sexpr reverse(sexpr const & l);
+
+}

src/tests/sexpr/sexpr.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "sexpr.h"
+#include "sexpr_funcs.h"
 #include "mpq.h"
 #include "name.h"
 #include "test.h"
@@ -48,6 +49,26 @@ static void tst1() {
     std::cout << sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) } << "\n";
     // list of lists
     std::cout << sexpr{ sexpr{1,2}, sexpr{2,3}, sexpr{0,1} } << "\n";
+    lean_assert(reverse(sexpr{1, 2, 3}) == (sexpr{3, 2, 1}));
+    sexpr l = map(sexpr{1, 2, 3},
+                  [](sexpr e) {
+                      return sexpr(to_int(e) + 10);
+                  });
+    std::cout << l << std::endl;
+    lean_assert(l == (sexpr{11, 12, 13}));
+    {
+        sexpr l = filter(sexpr{10, -2, 3, -1, 0}, [](sexpr e) { return to_int(e) >= 0; });
+        std::cout << l << std::endl;
+        lean_assert(l == (sexpr{10, 3, 0}));
+    }
+    lean_assert(member(3, sexpr{10, 2, 3, 1}));
+    lean_assert(!member(3, nil()));
+    lean_assert(!member(3, sexpr{10, 2, 1}));
+    lean_assert(append(sexpr{1,2}, sexpr{3,4}) == (sexpr{1,2,3,4}));
+    lean_assert(append(l, nil()) == l);
+    lean_assert(append(nil(), l) == l);
+    lean_assert(contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < 0; }));
+    lean_assert(!contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < -10; }));
 }
 
 int main() {