From 3657320edb8d467046c6b950f82d0bb17cdc0c19 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Sep 2013 11:36:05 -0700 Subject: [PATCH] Add basic list functions Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_operator_info.cpp | 2 +- src/tests/util/list.cpp | 24 +++++++- src/util/buffer.h | 12 ++++ src/util/list.h | 4 +- src/util/list_fn.h | 73 +++++++++++++++++++++++ 5 files changed, 110 insertions(+), 5 deletions(-) create mode 100644 src/util/list_fn.h diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/lean_operator_info.cpp index 3af1d4687..cd56843cc 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/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())) {} 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(parts, parts + num_parts)) { + m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(to_list(parts, parts + num_parts)) { lean_assert(num_parts > 0); } diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index 196b0b43c..95de1cd4a 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #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 a{10, 20, 30}; - list l = copy_to_list(a.begin(), a.end()); + list 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 l = copy_to_list(a, a+3); + list l = to_list(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{1, 2, 3, 4})); } +static void tst5() { + for (unsigned n = 0; n < 16; n++) { + buffer tmp; + for (unsigned i = 0; i < n; i++) { tmp.push_back(i); } + buffer tmp2; + to_buffer(to_list(tmp.begin(), tmp.end()), tmp2); + lean_assert(tmp2 == tmp); + list 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 l2 = append(p.first, p.second); + lean_assert(l2 == l); + int diff = static_cast(length(p.first)) - static_cast(length(p.second)); + lean_assert(-1 <= diff && diff <= 1); + } +} + int main() { tst1(); tst2(); tst3(); tst4(); + tst5(); return has_violations() ? 1 : 0; } diff --git a/src/util/buffer.h b/src/util/buffer.h index 58287a7db..96b9cc628 100644 --- a/src/util/buffer.h +++ b/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]; } diff --git a/src/util/list.h b/src/util/list.h index d19158a64..996704fa8 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -124,8 +124,8 @@ template unsigned length(list const & l) { } /** \brief Return a list containing the elements in the subrange [begin, end). */ -template list copy_to_list(It const & begin, It const & end) { - list r; +template list::value_type> to_list(It const & begin, It const & end) { + list::value_type> r; auto it = end; while (it != begin) { --it; diff --git a/src/util/list_fn.h b/src/util/list_fn.h new file mode 100644 index 000000000..87175c08e --- /dev/null +++ b/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 +void to_buffer(list const & l, buffer & r) { + for (T const & v : l) { + r.push_back(v); + } +} + +/** + \brief Auxiliary function for reverse function. +*/ +template +list reverse_aux(list const & l, list const & r) { + if (is_nil(l)) + return r; + else + return reverse_aux(cdr(l), cons(car(l), r)); +} + +/** + \brief Return the reverse list. +*/ +template +list reverse(list const & l) { + return reverse_aux(l, list()); +} + +/** + \brief Return two lists \c l1 and \c l2 of approximately the same size s.t. + append(l1, l2) == l +*/ +template +std::pair, list> split(list const & l) { + if (is_nil(l)) { + return mk_pair(l, l); + } else if (is_nil(cdr(l))) { + return mk_pair(l, list()); + } else { + buffer 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 +list append(list const & l1, list const & l2) { + buffer tmp; + to_buffer(l1, tmp); + to_buffer(l2, tmp); + return to_list(tmp.begin(), tmp.end()); +} +}