feat(util): add sequence object with O(1) concatenation operation

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

src/tests/util/CMakeLists.txt

@@ -1,6 +1,9 @@
 add_executable(name name.cpp)
 target_link_libraries(name "util" ${EXTRA_LIBS})
 add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name)
+add_executable(sequence sequence.cpp)
+target_link_libraries(sequence "util" ${EXTRA_LIBS})
+add_test(sequence ${CMAKE_CURRENT_BINARY_DIR}/sequence)
 add_executable(sexpr_tst sexpr.cpp)
 target_link_libraries(sexpr_tst "util" "numerics" "sexpr" ${EXTRA_LIBS})
 add_test(sexpr ${CMAKE_CURRENT_BINARY_DIR}/sexpr_tst)

src/tests/util/sequence.cpp

@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/sequence.h"
+#include "util/test.h"
+using namespace lean;
+
+template class sequence<int>;
+
+static void tst1() {
+    sequence<int> l1;
+    lean_assert(!l1);
+    sequence<int> l2(10);
+    lean_assert(l2);
+    lean_assert(is_eqp(l2, l1 + l2));
+    lean_assert(is_eqp(l2, l2 + l1));
+    lean_assert(!is_eqp(l2, l2 + l2));
+    sequence<int> l3(20);
+    sequence<int> l4(5);
+    sequence<int> r = l4 + (l2 + l2) + (l3 + l4) + sequence<int>(3);
+    buffer<int> b;
+    r.linearize(b);
+    for (auto v : b) std::cout << v << " "; std::cout << "\n";
+    lean_assert(b[0] == 5 && b[1] == 10 && b[2] == 10 && b[3] == 20 && b[4] == 5 && b[5] == 3);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}

src/util/sequence.h

@@ -0,0 +1,127 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/rc.h"
+#include "util/debug.h"
+#include "util/buffer.h"
+#include "util/optional.h"
+#include "util/memory_pool.h"
+
+namespace lean {
+/** \brief Sequence datastructure with O(1) concatenation operation */
+template<typename T>
+class sequence {
+    struct cell {
+        bool m_join;
+        MK_LEAN_RC();
+        void dealloc();
+        cell(bool join):m_join(join), m_rc(1) {}
+    };
+
+    struct elem_cell : public cell {
+        T m_value;
+        elem_cell(T const & v):cell(false), m_value(v) {}
+    };
+
+    struct node {
+        cell * m_ptr;
+        node():m_ptr(nullptr) {}
+        explicit node(T const & v);
+        node(node const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+        node(node && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+        node(node const & f, node const & s);
+        ~node() { if (m_ptr) m_ptr->dec_ref(); }
+        node & operator=(node const & s) { LEAN_COPY_REF(s); }
+        node & operator=(node && s) { LEAN_MOVE_REF(s); }
+        cell * raw() const { return m_ptr; }
+        explicit operator bool() const { return m_ptr != nullptr; }
+    };
+
+    struct join_cell : public cell {
+        node m_first;
+        node m_second;
+        join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {}
+    };
+
+    typedef memory_pool<sizeof(elem_cell)> elem_cell_allocator;
+    typedef memory_pool<sizeof(join_cell)> join_cell_allocator;
+    static elem_cell_allocator & get_elem_cell_allocator() {
+        LEAN_THREAD_PTR(elem_cell_allocator) g_allocator;
+        if (!g_allocator.get())
+            g_allocator.reset(new elem_cell_allocator());
+        return *g_allocator;
+    }
+
+    static join_cell_allocator & get_join_cell_allocator() {
+        LEAN_THREAD_PTR(join_cell_allocator) g_allocator;
+        if (!g_allocator.get())
+            g_allocator.reset(new join_cell_allocator());
+        return *g_allocator;
+    }
+private:
+    node m_node;
+public:
+    sequence() {}
+    explicit sequence(T const & v):m_node(v) {}
+    sequence(sequence const & f, sequence const & s):m_node(f.m_node, s.m_node) {}
+
+    /** \brief Return true iff it is not the empty/nil sequence. */
+    explicit operator bool() const { return m_node.raw() != nullptr; }
+
+    /** \brief Pointer equality. Return true iff \c s1 and \c s2 point to the same memory location. */
+    friend bool is_eqp(sequence const & s1, sequence const & s2) { return s1.m_node.raw() == s2.m_node.raw(); }
+
+    friend sequence operator+(sequence const & s1, sequence const & s2) { return sequence(s1, s2); }
+
+    /** \brief Store sequence elements in \c r */
+    void linearize(buffer<T> & r) const {
+        buffer<cell const *> todo;
+        if (m_node) todo.push_back(m_node.raw());
+        while (!todo.empty()) {
+            cell const * c = todo.back();
+            todo.pop_back();
+            if (c->m_join) {
+                todo.push_back(static_cast<join_cell const *>(c)->m_second.raw());
+                todo.push_back(static_cast<join_cell const *>(c)->m_first.raw());
+            } else {
+                r.push_back(static_cast<elem_cell const *>(c)->m_value);
+            }
+        }
+    }
+};
+
+template<typename T>
+void sequence<T>::cell::dealloc() {
+    if (m_join) {
+        join_cell * c = static_cast<join_cell*>(this);
+        c->~join_cell();
+        get_join_cell_allocator().recycle(c);
+    } else {
+        elem_cell * c = static_cast<elem_cell*>(this);
+        c->~elem_cell();
+        get_elem_cell_allocator().recycle(c);
+    }
+}
+
+template<typename T>
+sequence<T>::node::node(T const & v):m_ptr(new (get_elem_cell_allocator().allocate()) elem_cell(v)) {}
+
+template<typename T>
+sequence<T>::node::node(node const & f, node const & s) {
+    if (f && s) {
+        m_ptr = new (get_join_cell_allocator().allocate()) join_cell(f, s);
+    } else if (f) {
+        m_ptr = f.m_ptr;
+        m_ptr->inc_ref();
+    } else if (s) {
+        m_ptr = s.m_ptr;
+        m_ptr->inc_ref();
+    } else {
+        m_ptr = nullptr;
+    }
+}
+}