From 5be67bd42cc9bacb2df59f362b6e564bc4c93105 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 30 Jul 2013 00:05:30 -0700
Subject: [PATCH] Add forall, foldl, foldr to sexpr_funcs

---
 src/util/sexpr/sexpr_funcs.h | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/util/sexpr/sexpr_funcs.h b/src/util/sexpr/sexpr_funcs.h
index 9bc0d7cc6..b406ce21d 100644
--- a/src/util/sexpr/sexpr_funcs.h
+++ b/src/util/sexpr/sexpr_funcs.h
@@ -48,6 +48,42 @@ sexpr filter(sexpr const & l, P p) {
     }
 }
 
+template<class T, class BinaryOperation>
+T foldl(sexpr const & l, T init, BinaryOperation op) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return init;
+    }
+    else {
+        lean_assert(is_cons(l));
+        return foldl(tail(l), op(init, head(l)), op);
+    }
+}
+
+template<class T, class BinaryOperation>
+T foldr(sexpr const & l, T init, BinaryOperation op) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return init;
+    }
+    else {
+        lean_assert(is_cons(l));
+        return op(head(l), foldr(tail(l), init, op));
+    }
+}
+
+template<typename F>
+bool forall(sexpr const & l, F f) {
+    lean_assert(is_list(l));
+    if (is_nil(l)) {
+        return true;
+    }
+    else {
+        lean_assert(is_cons(l));
+        return f(head(l)) && forall(tail(l), f);
+    }
+}
+
 template<typename P>
 bool contains(sexpr const & l, P p) {
     lean_assert(is_list(l));