feat(util/list): add map_reuse template

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

src/tests/util/list.cpp

@@ -93,6 +93,27 @@ static void tst8() {
     lean_assert(c == length(l1));
 }
 
+static void tst9(int sz) {
+    list<int> l;
+    for (int i = 0; i < sz; i++) {
+        l = cons(i, l);
+    }
+    l = map_reuse(l, [&](int v) { return v > 90 ? v + 10 : v; });
+    std::cout << l << "\n";
+    unsigned sum = 0;
+    int j = length(l);
+    for (auto i : l) {
+        --j;
+        lean_assert(j > 90 || i == j);
+        sum += i;
+    }
+    auto l2 = map_reuse(l, [&](int v) { return v; });
+    lean_assert(l == l2);
+    auto l3 = map_reuse(l2, [&](int v) { return v + 2; });
+    lean_assert(compare(l2, l3, [](int v1, int v2) { return v1 + 2 == v2; }));
+    std::cout << l3 << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -102,5 +123,6 @@ int main() {
     tst6();
     tst7();
     tst8();
+    tst9(100);
     return has_violations() ? 1 : 0;
 }

src/util/list.h

@@ -16,14 +16,19 @@ namespace lean {
 */
 template<typename T>
 class list {
-    struct cell {
+public:
+    class cell {
         MK_LEAN_RC()
         T      m_head;
         list   m_tail;
+    public:
         cell(T const & h, list const & t):m_rc(1), m_head(h), m_tail(t) {}
         ~cell() {}
+        T const & head() const { return m_head; }
+        list const & tail() const { return m_tail; }
         void dealloc() { delete this; }
     };
+private:
     cell * m_ptr;
 public:
     list():m_ptr(nullptr) {}
@@ -38,11 +43,23 @@ public:
             *this = list(*it, *this);
         }
     }
+    explicit list(cell * c):m_ptr(c) { if (m_ptr) m_ptr->inc_ref(); }
     ~list() { if (m_ptr) m_ptr->dec_ref(); }
 
     list & operator=(list const & s) { LEAN_COPY_REF(list, s); }
     list & operator=(list && s) { LEAN_MOVE_REF(list, s); }
 
+    /**
+        \brief Return internal representation.
+        This method is useful when we know the list is not going to be deleted and
+        we want to save a temporary reference to it. Use raw() prevents us from updating the
+        reference counters.
+
+        \warning Use it with care. The main risk of storing references to cell is that
+        the list may be deleted.
+    */
+    cell * raw() const { return m_ptr; }
+
     /** \brief Return true iff it is not the empty/nil list. */
     operator bool() const { return m_ptr != nullptr; }
 
@@ -53,6 +70,8 @@ public:
 
     /** \brief Pointer equality. Return true iff \c l1 and \c l2 point to the same memory location. */
     friend bool is_eqp(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; }
+    friend bool is_eqp(list const & l1, cell const * l2) { return l1.m_ptr == l2; }
+
     /** \brief Structural equality. */
     friend bool operator==(list const & l1, list const & l2) {
         cell * it1 = l1.m_ptr;

src/util/list_fn.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <utility>
+#include <functional>
 #include "util/list.h"
 #include "util/buffer.h"
 #include "util/pair.h"
@@ -117,6 +118,41 @@ list<T> map(list<T> const & l, F f) {
     }
 }
 
+/**
+   \brief Semantically equivalent to \c map, but it tries to reuse
+   list cells. The elements are compared using the predicate \c eq.
+*/
+template<typename T, typename F, typename Eq = std::equal_to<T>>
+list<T> map_reuse(list<T> const & l, F f, Eq const & eq = Eq()) {
+    if (is_nil(l)) {
+        return l;
+    } else {
+        typedef typename list<T>::cell cell;
+        buffer<std::pair<T, cell*>> tmp;
+        cell * it = l.raw();
+        while (it) {
+            tmp.emplace_back(f(it->head()), it);
+            it = it->tail().raw();
+        }
+        unsigned i = tmp.size();
+        lean_assert(i > 0);
+        while (i > 0) {
+            --i;
+            std::pair<T, cell*> const & p = tmp[i];
+            if (!eq(p.first, p.second->head())) {
+                list<T> r(p.first, p.second->tail());
+                while (i > 0) {
+                    --i;
+                    std::pair<T, cell*> const & p = tmp[i];
+                    r = cons(p.first, r);
+                }
+                return r;
+            }
+        }
+        return l;
+    }
+}
+
 /**
    \brief Given list <tt>(a_0, ..., a_k)</tt>, exec f(a_0); f(a_1); ... f(a_k)</tt>.
 */