From 76252816acc014be40de972dabed3a2e328eb708 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Nov 2013 16:47:52 -0800
Subject: [PATCH] perf(util/list): avoid recursion in map and destructor

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/list.cpp | 16 ++++++++++++++++
 src/util/list.h         | 18 +++++++++++++++++-
 src/util/list_fn.h      | 22 +++++++++++++++++++++-
 3 files changed, 54 insertions(+), 2 deletions(-)

diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index 520c6cdf6b..06dbc06b37 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -131,6 +131,21 @@ static void tst10(int sz, int num) {
     }
 }
 
+static void tst11(int sz, int num) {
+    list<int> l;
+    for (int i = 0; i < sz; i++) {
+        l = cons(i, l);
+    }
+    list<int> l2;
+    {
+        timeit timer(std::cout, "map");
+        for (int i = 0; i < num; i++) {
+            l2 = map(l, [&](int v) { return v; });
+        }
+    }
+    lean_assert(l == l2);
+}
+
 int main() {
     tst1();
     tst2();
@@ -142,5 +157,6 @@ int main() {
     tst8();
     tst9(100);
     tst10(1000, 5);
+    tst11(1000, 5);
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/list.h b/src/util/list.h
index 623985fd14..78eb29fa18 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -30,6 +30,7 @@ public:
     };
 private:
     cell * m_ptr;
+    cell * steal_ptr() { cell * r = m_ptr; m_ptr = nullptr; return r; }
 public:
     list():m_ptr(nullptr) {}
     list(T const & h, list const & t):m_ptr(new cell(h, t)) {}
@@ -44,7 +45,22 @@ public:
         }
     }
     explicit list(cell * c):m_ptr(c) { if (m_ptr) m_ptr->inc_ref(); }
-    ~list() { if (m_ptr) m_ptr->dec_ref(); }
+    ~list() {
+        if (m_ptr && m_ptr->dec_ref_core()) {
+            cell * it = m_ptr;
+            while (true) {
+                lean_assert(it);
+                lean_assert(it->get_rc() == 0);
+                cell * next = it->m_tail.steal_ptr();
+                delete it;
+                if (next && next->dec_ref_core()) {
+                    it = next;
+                } else {
+                    break;
+                }
+            }
+        }
+    }
 
     list & operator=(list const & s) { LEAN_COPY_REF(list, s); }
     list & operator=(list && s) { LEAN_MOVE_REF(list, s); }
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index 3b105e6813..af2ff4a2f3 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -22,6 +22,18 @@ void to_buffer(list<T> const & l, buffer<T> & r) {
     }
 }
 
+/**
+   \brief Copy the cells in the list \c l to the buffer \c r.
+*/
+template<typename T>
+void to_buffer(list<T> const & l, buffer<typename list<T>::cell *> & r) {
+    typename list<T>::cell * it = l.raw();
+    while (it) {
+        r.push_back(it);
+        it = it->tail().raw();
+    }
+}
+
 /**
     \brief Auxiliary function for reverse function.
 */
@@ -114,7 +126,15 @@ list<T> map(list<T> const & l, F f) {
     if (is_nil(l)) {
         return l;
     } else {
-        return list<T>(f(head(l)), map(tail(l), f));
+        buffer<typename list<T>::cell*> tmp;
+        to_buffer(l, tmp);
+        unsigned i = tmp.size();
+        list<T> r;
+        while (i > 0) {
+            --i;
+            r = cons(f(tmp[i]->head()), r);
+        }
+        return l;
     }
 }