Add (temporary) buffer class

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

src/kernel/deep_copy.cpp

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <vector>
 #include "expr.h"
 #include "maps.h"
+#include "buffer.h"
 
 namespace lean {
 class deep_copy_fn {
@@ -23,7 +23,7 @@ class deep_copy_fn {
         case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
             r = copy(a); break; // shallow copy is equivalent to deep copy for these ones.
         case expr_kind::App: {
-            std::vector<expr> new_args;
+            buffer<expr> new_args;
             for (expr const & old_arg : args(a))
                 new_args.push_back(apply(old_arg));
             r = app(new_args.size(), new_args.data());

src/kernel/max_sharing.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <unordered_set>
-#include <vector>
+#include "buffer.h"
 #include "max_sharing.h"
 
 namespace lean {
@@ -36,7 +36,7 @@ struct max_sharing_fn::imp {
             cache(a);
             return a;
         case expr_kind::App: {
-            std::vector<expr> new_args;
+            buffer<expr> new_args;
             bool modified = false;
             for (expr const & old_arg : args(a)) {
                 new_args.push_back(apply(old_arg));

src/kernel/replace.h

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <vector>
+#include "buffer.h"
 #include "expr.h"
 #include "maps.h"
 namespace lean {
@@ -38,7 +38,7 @@ class replace_fn {
             case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
                 break;
             case expr_kind::App: {
-                std::vector<expr> new_args;
+                buffer<expr> new_args;
                 bool modified = false;
                 for (expr const & a : args(e)) {
                     new_args.push_back(apply(a, offset));

src/tests/util/CMakeLists.txt

@@ -4,6 +4,12 @@ add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt)
 add_executable(name name.cpp)
 target_link_libraries(name ${EXTRA_LIBS})
 add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name)
+<<<<<<< HEAD
 add_executable(format format.cpp)
 target_link_libraries(format ${EXTRA_LIBS})
 add_test(format ${CMAKE_CURRENT_BINARY_DIR}/format)
+=======
+add_executable(buffer buffer.cpp)
+target_link_libraries(buffer ${EXTRA_LIBS})
+add_test(buffer ${CMAKE_CURRENT_BINARY_DIR}/buffer)
+>>>>>>> Add (temporary) buffer class

src/tests/util/buffer.cpp

@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <vector>
+#include "buffer.h"
+using namespace lean;
+
+template<typename C>
+static void loop(int n) {
+    C b;
+    b.push_back(n);
+    lean_assert(b.size() == 1);
+    lean_assert(b.back() == n);
+    lean_assert(b[0] == n);
+    if (n > 0)
+        loop<C>(n-1);
+}
+
+void perftest() {
+    for (unsigned i = 0; i < 10000; i++)
+        loop<buffer<int>>(10000);
+//    for (unsigned i = 0; i < 10000; i++)
+//        loop<std::vector<int>>(10000);
+}
+
+int main() {
+    loop<buffer<int>>(100);
+    return 0;
+}

src/util/buffer.h

@@ -0,0 +1,119 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <algorithm>
+#include <cstring>
+#include "debug.h"
+
+namespace lean {
+
+template<typename T, unsigned INITIAL_SIZE=16>
+class buffer {
+protected:
+    T *      m_buffer;
+    unsigned m_pos;
+    unsigned m_capacity;
+    char     m_initial_buffer[INITIAL_SIZE * sizeof(T)];
+
+    void free_memory() {
+        if (m_buffer != reinterpret_cast<T*>(m_initial_buffer))
+            delete[] reinterpret_cast<char*>(m_buffer);
+    }
+
+    void expand() {
+        unsigned new_capacity = m_capacity << 1;
+        T * new_buffer        = reinterpret_cast<T*>(new char[sizeof(T) * new_capacity]);
+        std::memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
+        free_memory();
+        m_buffer              = new_buffer;
+        m_capacity            = new_capacity;
+    }
+
+    void destroy_elements() {
+        std::for_each(begin(), end(), [](T & e) { e.~T(); });
+    }
+
+    void destroy() {
+        destroy_elements();
+        free_memory();
+    }
+
+public:
+    typedef T value_type;
+    typedef T * iterator;
+    typedef T const * const_iterator;
+
+    buffer():
+        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+        m_pos(0),
+        m_capacity(INITIAL_SIZE) {
+    }
+
+    buffer(buffer const & source):
+        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+        m_pos(0),
+        m_capacity(INITIAL_SIZE) {
+        std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); });
+    }
+
+    ~buffer() { destroy(); }
+
+    buffer & operator=(buffer const & source) {
+        clear();
+        std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); });
+        return *this;
+    }
+
+    T const & back() const { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
+    T & back() { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
+    T & operator[](unsigned idx) { lean_assert(idx < size());  return m_buffer[idx]; }
+    T const & operator[](unsigned idx) const { lean_assert(idx < size()); return m_buffer[idx]; }
+    void clear() { destroy_elements(); m_pos = 0; }
+    unsigned size() const { return m_pos; }
+    T const * data() const { return m_buffer; }
+    T * data() { return m_buffer; }
+    bool empty() const { return m_pos == 0;  }
+    iterator begin() { return m_buffer; }
+    iterator end() { return m_buffer + size(); }
+    const_iterator begin() const { return m_buffer; }
+    const_iterator end() const { return m_buffer + size(); }
+
+    void push_back(T const & elem) {
+        if (m_pos >= m_capacity)
+            expand();
+        new (m_buffer + m_pos) T(elem);
+        m_pos++;
+    }
+
+    void pop_back() {
+        back().~T();
+        m_pos--;
+    }
+
+    void resize(unsigned nsz, T const & elem=T()) {
+        unsigned sz = size();
+        if (nsz > sz) {
+            for (unsigned i = sz; i < nsz; i++)
+                push_back(elem);
+        }
+        else if (nsz < sz) {
+            for (unsigned i = nsz; i < sz; i++)
+                pop_back();
+        }
+        lean_assert(size() == nsz);
+    }
+
+    void shrink(unsigned nsz) {
+        unsigned sz = size();
+        lean_assert(nsz <= sz);
+        for (unsigned i = nsz; i < sz; i++)
+            pop_back();
+        lean_assert(size() == nsz);
+    }
+};
+
+}

src/util/name.cpp

@@ -88,7 +88,7 @@ name::name(name const & prefix, char const * name) {
     lean_assert(sz < 1u<<31);
     char * mem = new char[sizeof(imp) + sz + 1];
     m_imp      = new (mem) imp(true, prefix.m_imp);
-    memcpy(mem + sizeof(imp), name, sz + 1);
+    std::memcpy(mem + sizeof(imp), name, sz + 1);
     m_imp->m_str       = mem + sizeof(imp);
     if (m_imp->m_prefix)
         m_imp->m_hash = hash_str(sz, name, m_imp->m_prefix->m_hash);