Add basic list functions

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

src/frontends/lean/lean_operator_info.cpp

@@ -22,7 +22,7 @@ struct operator_info::imp {
         m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list<name>())) {}
 
     imp(unsigned num_parts, name const * parts, fixity f, unsigned p):
-        m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(copy_to_list<name const *, name>(parts, parts + num_parts)) {
+        m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(to_list<name const *>(parts, parts + num_parts)) {
         lean_assert(num_parts > 0);
     }
 

src/tests/util/list.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include "list.h"
+#include "list_fn.h"
 #include "test.h"
 using namespace lean;
 
@@ -24,7 +25,7 @@ static void tst1() {
 
 static void tst2() {
     std::vector<int> a{10, 20, 30};
-    list<int> l = copy_to_list(a.begin(), a.end());
+    list<int> l = to_list(a.begin(), a.end());
     std::cout << l << "\n";
     lean_assert(head(l) == 10);
     lean_assert(head(tail(l)) == 20);
@@ -34,7 +35,7 @@ static void tst2() {
 
 static void tst3() {
     int a[3] = {10, 20, 30};
-    list<int> l = copy_to_list<int*, int>(a, a+3);
+    list<int> l = to_list<int*>(a, a+3);
     std::cout << l << "\n";
     lean_assert(head(l) == 10);
     lean_assert(head(tail(l)) == 20);
@@ -57,10 +58,29 @@ static void tst4() {
     lean_assert(l1 != tail(list<int>{1, 2, 3, 4}));
 }
 
+static void tst5() {
+    for (unsigned n = 0; n < 16; n++) {
+        buffer<int> tmp;
+        for (unsigned i = 0; i < n; i++) { tmp.push_back(i); }
+        buffer<int> tmp2;
+        to_buffer(to_list(tmp.begin(), tmp.end()), tmp2);
+        lean_assert(tmp2 == tmp);
+        list<int> l = to_list(tmp.begin(), tmp.end());
+        lean_assert(n == 0 || car(reverse(l)) == n - 1);
+        lean_assert(reverse(reverse(l)) == l);
+        auto p = split(l);
+        list<int> l2 = append(p.first, p.second);
+        lean_assert(l2 == l);
+        int diff = static_cast<int>(length(p.first)) - static_cast<int>(length(p.second));
+        lean_assert(-1 <= diff && diff <= 1);
+    }
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }

src/util/buffer.h

@@ -73,6 +73,18 @@ public:
         return *this;
     }
 
+    bool operator==(buffer const & other) {
+        if (size() != other.size()) {
+            return false;
+        } else {
+            for (unsigned i = 0; i < size(); i++) {
+                if (operator[](i) != other[i])
+                    return false;
+            }
+            return true;
+        }
+    }
+
     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]; }

src/util/list.h

@@ -124,8 +124,8 @@ template<typename T> unsigned length(list<T> const & l) {
 }
 
 /** \brief Return a list containing the elements in the subrange <tt>[begin, end)</tt>. */
-template<typename It, typename T = typename It::value_type> list<T> copy_to_list(It const & begin, It const & end) {
-    list<T> r;
+template<typename It> list<typename std::iterator_traits<It>::value_type> to_list(It const & begin, It const & end) {
+    list<typename std::iterator_traits<It>::value_type> r;
     auto it = end;
     while (it != begin) {
         --it;

src/util/list_fn.h

@@ -0,0 +1,73 @@
+/*
+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 "list.h"
+#include "buffer.h"
+#include "pair.h"
+
+namespace lean {
+/**
+   \brief Copy the values in the list \c l to the buffer \c r.
+*/
+template<typename T>
+void to_buffer(list<T> const & l, buffer<T> & r) {
+    for (T const & v : l) {
+        r.push_back(v);
+    }
+}
+
+/**
+    \brief Auxiliary function for reverse function.
+*/
+template<typename T>
+list<T> reverse_aux(list<T> const & l, list<T> const & r) {
+    if (is_nil(l))
+        return r;
+    else
+        return reverse_aux(cdr(l), cons(car(l), r));
+}
+
+/**
+   \brief Return the reverse list.
+*/
+template<typename T>
+list<T> reverse(list<T> const & l) {
+    return reverse_aux(l, list<T>());
+}
+
+/**
+   \brief Return two lists \c l1 and \c l2 of approximately the same size s.t.
+   <tt>append(l1, l2) == l</tt>
+*/
+template<typename T>
+std::pair<list<T>, list<T>> split(list<T> const & l) {
+    if (is_nil(l)) {
+        return mk_pair(l, l);
+    } else if (is_nil(cdr(l))) {
+        return mk_pair(l, list<T>());
+    } else {
+        buffer<T> tmp;
+        to_buffer(l, tmp);
+        unsigned mid = tmp.size() / 2;
+        auto beg = tmp.begin();
+        lean_assert(beg + mid <= tmp.end());
+        return mk_pair(to_list(beg, beg + mid),
+                       to_list(beg + mid, tmp.end()));
+    }
+}
+
+/**
+   \brief Append two lists
+*/
+template<typename T>
+list<T> append(list<T> const & l1, list<T> const & l2) {
+    buffer<T> tmp;
+    to_buffer(l1, tmp);
+    to_buffer(l2, tmp);
+    return to_list(tmp.begin(), tmp.end());
+}
+}