feat(util/lazy_list): add useful lazy_list function templates

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

src/tests/util/lazy_list.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/numerics/mpz.h"
 #include "util/pair.h"
 #include "util/lazy_list.h"
+#include "util/lazy_list_fn.h"
 #include "util/list.h"
 using namespace lean;
 
@@ -32,30 +33,28 @@ lazy_list<mpz> fact_list() {
     return fact_list_core(mpz(1), mpz(1));
 }
 
-template<typename T>
+lazy_list<int> mk_simple1(int y) {
-lazy_list<T> first(unsigned sz, lazy_list<T> l) {
+    int x = 3;
-    if (sz == 0 || !l) {
+    return map(map(append(from(10, 1, 15), from(20, 2, 25)), [=](int v) { return x + v; }),
-        return lazy_list<T>();
+               [=](int v) { return v - y; });
-    } else {
-        return lazy_list<T>(head(l), [=]() { return first(sz - 1, tail(l)); });
-    }
 }
 
-template<typename T1, typename T2>
+lazy_list<int> mk_simple2() {
-lazy_list<std::pair<T1, T2>> zip(lazy_list<T1> const & l1, lazy_list<T2> const & l2) {
+    int x = 10;
-    if (l1 && l2) {
+    return filter(map(interleave(from(0, 2, 10), from(10, 3, 20)), [=](int v) { return x * v; }),
-        return lazy_list<std::pair<T1, T2>>(mk_pair(head(l1), head(l2)), [=]() { return zip(tail(l1), tail(l2)); });
+                  [](int v) { return v > 40; });
-    } else {
+}
-        return lazy_list<std::pair<T1, T2>>();
+
-    }
+lazy_list<int> mk_simple3() {
+    return map_append(from(0, 2, 100), [=](int v) { return from(1, 1, v); });
 }
 
 template<typename T>
-lazy_list<T> to_lazy(list<T> const & l) {
+void display(lazy_list<T> const & l) {
-    if (l)
+    for (auto v : l) {
-        return lazy_list<T>(head(l), [=]() { return to_lazy(tail(l)); });
+        std::cout << v << " ";
-    else
+    }
-        return lazy_list<T>();
+    std::cout << "\n";
 }
 
 int main() {
@@ -69,7 +68,7 @@ int main() {
         std::cout << c << "\n";
     }
     int i = 1;
-    for (auto c : first(30, zip(seq(1), fact_list()))) {
+    for (auto c : take(30, zip(seq(1), fact_list()))) {
         lean_assert(c.first == i);
         std::cout << c.first << " " << c.second << "\n";
         i++;
@@ -80,5 +79,8 @@ int main() {
         lean_assert(c == i);
         i++;
     }
+    display(mk_simple1(4));
+    display(mk_simple2());
+    display(take(12, mk_simple3()));
     return 0;
 }

src/util/lazy_list_fn.h

@@ -0,0 +1,91 @@
+/*
+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 <utility>
+#include "util/lazy_list.h"
+#include "util/list.h"
+
+namespace lean {
+template<typename T>
+lazy_list<T> take(unsigned sz, lazy_list<T> l) {
+    if (sz == 0 || !l) {
+        return lazy_list<T>();
+    } else {
+        return lazy_list<T>(head(l), [=]() { return take(sz - 1, tail(l)); });
+    }
+}
+
+template<typename T1, typename T2>
+lazy_list<std::pair<T1, T2>> zip(lazy_list<T1> const & l1, lazy_list<T2> const & l2) {
+    if (l1 && l2) {
+        return lazy_list<std::pair<T1, T2>>(mk_pair(head(l1), head(l2)), [=]() { return zip(tail(l1), tail(l2)); });
+    } else {
+        return lazy_list<std::pair<T1, T2>>();
+    }
+}
+
+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>();
+}
+
+template<typename T>
+lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
+    if (!l1)
+        return l2;
+    else if (!l2)
+        return l1;
+    else
+        return lazy_list<T>(head(l1), [=]() { return append(tail(l1), l2); });
+}
+
+template<typename T, typename F>
+lazy_list<T> map(lazy_list<T> const & l, F && f) {
+    if (!l)
+        return l;
+    else
+        return lazy_list<T>(f(head(l)), [=]() { return map(tail(l), f); });
+}
+
+template<typename T>
+lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
+    if (!l1)
+        return l2;
+    else if (!l2)
+        return l1;
+    else
+        return lazy_list<T>(head(l1), [=]() { return interleave(l2, tail(l1)); });
+}
+
+template<typename T, typename P>
+lazy_list<T> filter(lazy_list<T> const & l, P && p) {
+    if (!l)
+        return l;
+    else if (p(head(l)))
+        return lazy_list<T>(head(l), [=]() { return filter(tail(l), p); });
+    else
+        return filter(tail(l), p);
+}
+
+template<typename T, typename F>
+lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F && f) {
+    if (!l)
+        return h;
+    else if (h)
+        return lazy_list<T>(head(h), [=]() { return map_append_aux(tail(h), l, f); });
+    else
+        return map_append_aux(f(head(l)), tail(l), f);
+}
+
+template<typename T, typename F>
+lazy_list<T> map_append(lazy_list<T> const & l, F && f) {
+    return map_append_aux(lazy_list<T>(), l, f);
+}
+}