michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lazy_list): add more tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-29 14:38:20 -07:00
parent 80c282d0a3
commit 02f621aa45
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/tests/util/lazy_list.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "util/numerics/mpz.h"
#include "util/pair.h"
#include "util/lazy_list.h"
#include "util/list.h"
using namespace lean;
lazy_list<int> seq(int s) {
@ -49,14 +50,35 @@ lazy_list<std::pair<T1, T2>> zip(lazy_list<T1> const & l1, lazy_list<T2> const &
}
}
template<typename T>
lazy_list<T> to_lazy(list<T> const & l) {
if (l)
return lazy_list<T>(head(l), [=]() { return to_lazy(tail(l)); });
else
return lazy_list<T>();
}
int main() {
lean_assert(head(lazy_list<int>(10)) == 10);
lean_assert(!lazy_list<int>());
lean_assert(!tail(lazy_list<int>(10)));
lazy_list<int> l(-10, from(10, 20, 100));
l = cons(-20, l);
lean_assert(head(l) == -20);
for (auto c : l) {
std::cout << c << "\n";
}
int i = 1;
for (auto c : first(30, zip(seq(1), fact_list()))) {
lean_assert(c.first == i);
std::cout << c.first << " " << c.second << "\n";
i++;
}
list<int> l2{1, 2, 3};
i = 1;
for (auto c : to_lazy(l2)) {
lean_assert(c == i);
i++;
}
return 0;
}