feat(util/list): map_append template

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

src/tests/util/list.cpp

@@ -187,6 +187,21 @@ static void tst14() {
     lean_assert_eq(filter(l, [](int i) { return i % 3 == 0; }), list<int>({3, 6}));
 }
 
+static list<int> range(int l, int u) {
+    if (l > u)
+        return list<int>();
+    else
+        return cons(l, range(l+1, u));
+}
+
+static void tst15() {
+    list<int> l({1, 2, 3, 4});
+    std::cout << map_append(l, [](int i) { return range(1, i); }) << "\n";
+    lean_assert_eq(map_append(l, [](int i) { return range(1, i); }), list<int>({1, 1, 2, 1, 2, 3, 1, 2, 3, 4}));
+    lean_assert_eq(map_append(l, [](int i) { return i == 2 ? list<int>({2, 2, 2}) : list<int>(i); }),
+                   list<int>({1, 2, 2, 2, 3, 4}));
+}
+
 int main() {
     tst1();
     tst2();
@@ -202,5 +217,6 @@ int main() {
     tst12();
     tst13();
     tst14();
+    tst15();
     return has_violations() ? 1 : 0;
 }

src/util/list_fn.h

@@ -204,6 +204,18 @@ list<T> map_filter(list<T> const & l, F && f) {
     }
 }
 
+template<typename T, typename F>
+list<T> map_append(list<T> const & l, F && f) {
+    if (is_nil(l)) {
+        return l;
+    } else {
+        buffer<T> tmp;
+        for (auto const & v : l)
+            to_buffer(f(v), tmp);
+        return to_list(tmp.begin(), tmp.end());
+    }
+}
+
 /**
    \brief Semantically equivalent to \c map, but it tries to reuse
    list cells. The elements are compared using the predicate \c eq.