diff options
Diffstat (limited to 'lib/iStream.ml')
-rw-r--r-- | lib/iStream.ml | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/lib/iStream.ml b/lib/iStream.ml new file mode 100644 index 00000000..f9351d4b --- /dev/null +++ b/lib/iStream.ml @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type ('a,'r) u = +| Nil +| Cons of 'a * 'r + +type 'a node = ('a,'a t) u + +and 'a t = 'a node Lazy.t + +let empty = Lazy.lazy_from_val Nil + +let cons x s = Lazy.lazy_from_val (Cons (x, s)) + +let thunk = Lazy.lazy_from_fun + +let rec make_node f s = match f s with +| Nil -> Nil +| Cons (x, s) -> Cons (x, make f s) + +and make f s = lazy (make_node f s) + +let rec force s = match Lazy.force s with +| Nil -> () +| Cons (_, s) -> force s + +let force s = force s; s + +let is_empty s = match Lazy.force s with +| Nil -> true +| Cons (_, _) -> false + +let peek = Lazy.force + +let rec of_list = function +| [] -> empty +| x :: l -> cons x (of_list l) + +let rec to_list s = match Lazy.force s with +| Nil -> [] +| Cons (x, s) -> x :: (to_list s) + +let rec iter f s = match Lazy.force s with +| Nil -> () +| Cons (x, s) -> f x; iter f s + +let rec map_node f = function +| Nil -> Nil +| Cons (x, s) -> Cons (f x, map f s) + +and map f s = lazy (map_node f (Lazy.force s)) + +let rec app_node n1 s2 = match n1 with +| Nil -> Lazy.force s2 +| Cons (x, s1) -> Cons (x, app s1 s2) + +and app s1 s2 = lazy (app_node (Lazy.force s1) s2) + +let rec fold f accu s = match Lazy.force s with +| Nil -> accu +| Cons (x, s) -> fold f (f accu x) s + +let rec map_filter_node f = function +| Nil -> Nil +| Cons (x, s) -> + begin match f x with + | None -> map_filter_node f (Lazy.force s) + | Some y -> Cons (y, map_filter f s) + end + +and map_filter f s = lazy (map_filter_node f (Lazy.force s)) + +let rec concat_node = function +| Nil -> Nil +| Cons (s, sl) -> app_node (Lazy.force s) (concat sl) + +and concat (s : 'a t t) = + lazy (concat_node (Lazy.force s)) + +let rec concat_map_node f = function +| Nil -> Nil +| Cons (x,s) -> app_node (Lazy.force (f x)) (concat_map f s) + +and concat_map f l = lazy (concat_map_node f (Lazy.force l)) |