/* 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 #include #include "util/test.h" #include "util/numerics/mpz.h" #include "util/pair.h" #include "util/lazy_list.h" using namespace lean; lazy_list seq(int s) { return lazy_list(s, [=]() { return seq(s + 1); }); } lazy_list from(int begin, int step, int end) { if (begin > end) return lazy_list(); else return lazy_list(begin, [=]() { return from(begin + step, step, end); }); } lazy_list fact_list_core(mpz i, mpz n) { return lazy_list(n, [=]() { return fact_list_core(i+1, n*(i+1)); }); } lazy_list fact_list() { return fact_list_core(mpz(1), mpz(1)); } template lazy_list first(unsigned sz, lazy_list l) { if (sz == 0 || !l) { return lazy_list(); } else { return lazy_list(head(l), [=]() { return first(sz - 1, tail(l)); }); } } template lazy_list> zip(lazy_list const & l1, lazy_list const & l2) { if (l1 && l2) { return lazy_list>(mk_pair(head(l1), head(l2)), [=]() { return zip(tail(l1), tail(l2)); }); } else { return lazy_list>(); } } int main() { lazy_list l(-10, from(10, 20, 100)); l = cons(-20, l); for (auto c : l) { std::cout << c << "\n"; } for (auto c : first(30, zip(seq(1), fact_list()))) { std::cout << c.first << " " << c.second << "\n"; } return 0; }