From 5aa9264091e88aab66cc63a4dee2e9e0e40a6b16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Dec 2013 23:08:10 -0800
Subject: [PATCH] feat(util/list): add remove_last template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/list.cpp | 11 +++++++++++
 src/util/list_fn.h      | 24 ++++++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index d0a08d40a..e70a81f2f 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -218,6 +218,16 @@ static void tst17() {
     lean_assert(is_eqp(tail(tail(l)), tail(l2)));
 }
 
+static void tst18() {
+    list<int> l({1, 2, 3, 4, 5});
+    lean_assert_eq(remove_last(l, [](int v) { return v % 2 == 0; }), list<int>({1, 2, 3, 5}));
+    lean_assert_eq(remove_last(l, [](int v) { return v < 0; }), l);
+    lean_assert(is_eqp(remove_last(l, [](int v) { return v < 0; }), l));
+    list<int> l2 = remove_last(l, [](int v) { return v < 3; });
+    lean_assert_eq(l2, list<int>({1, 3, 4, 5}));
+    lean_assert(is_eqp(tail(tail(l)), tail(l2)));
+}
+
 int main() {
     tst1();
     tst2();
@@ -236,5 +246,6 @@ int main() {
     tst15();
     tst16();
     tst17();
+    tst18();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index 61a1e1b60..86ec4c0fc 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -184,6 +184,30 @@ list<T> filter(list<T> const & l, P && p) {
     }
 }
 
+/**
+   \brief Remove the last element that satisfies \c p.
+*/
+template<typename T, typename P>
+list<T> remove_last(list<T> const & l, P && p) {
+    if (!is_nil(l)) {
+        buffer<typename list<T>::cell*> tmp;
+        to_buffer(l, tmp);
+        unsigned i = tmp.size();
+        while (i > 0) {
+            --i;
+            if (p(tmp[i]->head())) {
+                list<T> r = tmp[i]->tail();
+                while (i > 0) {
+                    --i;
+                    r = cons(tmp[i]->head(), r);
+                }
+                return r;
+            }
+        }
+    }
+    return l;
+}
+
 /**
    \brief Similar to \c map but \c f has signature