feat(util/list): filter template

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

src/tests/util/list.cpp

@@ -178,6 +178,15 @@ static void tst13() {
     lean_assert(empty(map_filter(list<int>(), [](int in, int & out) { out = in; return true; })));
 }
 
+static void tst14() {
+    list<int> l({1, 2, 3, 4, 5, 6, 7, 8});
+    lean_assert_eq(filter(l, [](int i) { return i % 2 == 0; }), list<int>({2, 4, 6, 8}));
+    lean_assert_eq(filter(l, [](int i) { return i < 3; }), list<int>({1, 2}));
+    lean_assert_eq(filter(l, [](int i) { return i > 10; }), list<int>());
+    lean_assert_eq(filter(l, [](int i) { return i > 5; }), list<int>({6, 7, 8}));
+    lean_assert_eq(filter(l, [](int i) { return i % 3 == 0; }), list<int>({3, 6}));
+}
+
 int main() {
     tst1();
     tst2();
@@ -192,5 +201,6 @@ int main() {
     tst11(1000, 5);
     tst12();
     tst13();
+    tst14();
     return has_violations() ? 1 : 0;
 }

src/util/list_fn.h

@@ -156,6 +156,28 @@ list<T> map(list<T> const & l, F && f) {
     }
 }
 
+/**
+   \brief Filter/Remove elements from the list
+   that satisfy the given predicate.
+*/
+template<typename T, typename P>
+list<T> filter(list<T> const & l, P && p) {
+    if (is_nil(l)) {
+        return l;
+    } else {
+        buffer<typename list<T>::cell*> tmp;
+        to_buffer(l, tmp);
+        unsigned i = tmp.size();
+        list<T> r;
+        while (i > 0) {
+            --i;
+            if (p(tmp[i]->head()))
+                r = cons(tmp[i]->head(), r);
+        }
+        return r;
+    }
+}
+
 /**
    \brief Similar to \c map but \c f has signature