2013-07-24 23:32:50 +00:00
|
|
|
/*
|
|
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
|
|
|
Author: Leonardo de Moura
|
|
|
|
*/
|
2013-08-12 01:06:37 +00:00
|
|
|
#include <vector>
|
2013-09-26 03:13:05 +00:00
|
|
|
#include "util/test.h"
|
2013-09-13 03:04:10 +00:00
|
|
|
#include "util/list.h"
|
|
|
|
#include "util/list_fn.h"
|
2013-07-24 23:32:50 +00:00
|
|
|
using namespace lean;
|
|
|
|
|
|
|
|
static void tst1() {
|
|
|
|
list<int> l;
|
|
|
|
lean_assert(is_nil(l));
|
|
|
|
for (int i = 0; i < 10; i++) {
|
|
|
|
list<int> old = l;
|
|
|
|
l = list<int>(i, l);
|
|
|
|
lean_assert(!is_nil(l));
|
|
|
|
lean_assert(car(l) == i);
|
2013-08-14 23:35:04 +00:00
|
|
|
lean_assert(is_eqp(cdr(l), old));
|
2013-07-24 23:32:50 +00:00
|
|
|
}
|
|
|
|
std::cout << l << "\n";
|
|
|
|
}
|
|
|
|
|
2013-08-12 01:06:37 +00:00
|
|
|
static void tst2() {
|
|
|
|
std::vector<int> a{10, 20, 30};
|
2013-09-11 18:36:05 +00:00
|
|
|
list<int> l = to_list(a.begin(), a.end());
|
2013-08-12 01:06:37 +00:00
|
|
|
std::cout << l << "\n";
|
|
|
|
lean_assert(head(l) == 10);
|
|
|
|
lean_assert(head(tail(l)) == 20);
|
|
|
|
lean_assert(head(tail(tail(l))) == 30);
|
|
|
|
lean_assert(length(l) == 3);
|
|
|
|
}
|
|
|
|
|
|
|
|
static void tst3() {
|
|
|
|
int a[3] = {10, 20, 30};
|
2013-09-11 18:36:05 +00:00
|
|
|
list<int> l = to_list<int*>(a, a+3);
|
2013-08-12 01:06:37 +00:00
|
|
|
std::cout << l << "\n";
|
|
|
|
lean_assert(head(l) == 10);
|
|
|
|
lean_assert(head(tail(l)) == 20);
|
|
|
|
lean_assert(head(tail(tail(l))) == 30);
|
|
|
|
lean_assert(length(l) == 3);
|
2013-08-14 21:42:48 +00:00
|
|
|
lean_assert(length(list<int>()) == 0);
|
|
|
|
lean_assert(length(list<int>(10, list<int>())) == 1);
|
|
|
|
lean_assert(length(tail(list<int>(10, list<int>()))) == 0);
|
2013-08-12 01:06:37 +00:00
|
|
|
}
|
|
|
|
|
2013-08-14 23:35:04 +00:00
|
|
|
static void tst4() {
|
|
|
|
list<int> l1{1, 2, 3};
|
|
|
|
list<int> l2{1, 2, 3};
|
|
|
|
lean_assert(l1 == l2);
|
|
|
|
lean_assert(l1 != cons(1, l2));
|
|
|
|
lean_assert(l1 != tail(l1));
|
|
|
|
lean_assert(list<int>() == list<int>());
|
|
|
|
lean_assert(l2 != list<int>());
|
|
|
|
lean_assert(l1 != list<int>({1, 2, 3, 4}));
|
|
|
|
lean_assert(l1 != tail(list<int>{1, 2, 3, 4}));
|
|
|
|
}
|
|
|
|
|
2013-09-11 18:36:05 +00:00
|
|
|
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());
|
2013-09-12 08:39:04 +00:00
|
|
|
lean_assert(n == 0 || car(reverse(l)) == static_cast<int>(n - 1));
|
2013-09-11 18:36:05 +00:00
|
|
|
lean_assert(reverse(reverse(l)) == l);
|
|
|
|
auto p = split(l);
|
|
|
|
list<int> l2 = append(p.first, p.second);
|
|
|
|
lean_assert(l2 == l);
|
2013-09-11 20:48:49 +00:00
|
|
|
lean_assert(-1 <= static_cast<int>(length(p.first)) - static_cast<int>(length(p.second)) && static_cast<int>(length(p.first)) - static_cast<int>(length(p.second)) <= 1);
|
2013-09-11 18:36:05 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-09-26 05:04:24 +00:00
|
|
|
static void tst6() {
|
|
|
|
lean_assert(list<int>(10) == list<int>{10});
|
|
|
|
}
|
|
|
|
|
|
|
|
static void tst7() {
|
|
|
|
list<int> l{10, 20};
|
|
|
|
list<int> l2(30, l);
|
|
|
|
list<int> l3(30, l);
|
|
|
|
lean_assert(l2 == l3);
|
|
|
|
}
|
|
|
|
|
2013-11-18 17:13:34 +00:00
|
|
|
static void tst8() {
|
|
|
|
list<int> l1{1, 2, 3};
|
|
|
|
unsigned c = 0;
|
|
|
|
for_each(l1, [&](int ){ c = c + 1; });
|
|
|
|
lean_assert(c == length(l1));
|
|
|
|
}
|
|
|
|
|
2013-11-18 23:29:35 +00:00
|
|
|
static void tst9(int sz) {
|
|
|
|
list<int> l;
|
|
|
|
for (int i = 0; i < sz; i++) {
|
|
|
|
l = cons(i, l);
|
|
|
|
}
|
|
|
|
l = map_reuse(l, [&](int v) { return v > 90 ? v + 10 : v; });
|
|
|
|
std::cout << l << "\n";
|
|
|
|
unsigned sum = 0;
|
|
|
|
int j = length(l);
|
|
|
|
for (auto i : l) {
|
|
|
|
--j;
|
|
|
|
lean_assert(j > 90 || i == j);
|
|
|
|
sum += i;
|
|
|
|
}
|
|
|
|
auto l2 = map_reuse(l, [&](int v) { return v; });
|
|
|
|
lean_assert(l == l2);
|
|
|
|
auto l3 = map_reuse(l2, [&](int v) { return v + 2; });
|
|
|
|
lean_assert(compare(l2, l3, [](int v1, int v2) { return v1 + 2 == v2; }));
|
|
|
|
std::cout << l3 << "\n";
|
|
|
|
}
|
|
|
|
|
2013-07-24 23:32:50 +00:00
|
|
|
int main() {
|
|
|
|
tst1();
|
2013-08-12 01:06:37 +00:00
|
|
|
tst2();
|
|
|
|
tst3();
|
2013-08-14 23:35:04 +00:00
|
|
|
tst4();
|
2013-09-11 18:36:05 +00:00
|
|
|
tst5();
|
2013-09-26 05:04:24 +00:00
|
|
|
tst6();
|
|
|
|
tst7();
|
2013-11-18 17:13:34 +00:00
|
|
|
tst8();
|
2013-11-18 23:29:35 +00:00
|
|
|
tst9(100);
|
2013-07-24 23:32:50 +00:00
|
|
|
return has_violations() ? 1 : 0;
|
|
|
|
}
|