Adding a persistent stream data structure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 86 insertions, 0 deletions

diff --git a/lib/iStream.ml b/lib/iStream.ml
new file mode 100644
index 0000000000..c1894da750
--- /dev/null
+++ b/lib/iStream.ml
@@ -0,0 +1,86 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a t =
+| Nil
+| Cons of 'a * 'a t
+| Lazy of 'a t Lazy.t
+
+let empty = Nil
+
+let cons x s = Cons (x, s)
+
+let thunk s = Lazy s
+
+let rec force = function
+| Nil -> ()
+| Cons (_, s) -> force s
+| Lazy t -> force (Lazy.force t)
+
+let force s = force s; s
+
+let rec is_empty = function
+| Nil -> true
+| Cons (_, _) -> false
+| Lazy t -> is_empty (Lazy.force t)
+
+let rec peek = function
+| Nil -> None
+| Cons (x, s) -> Some (x, s)
+| Lazy t -> peek (Lazy.force t)
+
+let rec of_list = function
+| [] -> Nil
+| x :: l -> Cons (x, of_list l)
+
+let rec to_list = function
+| Nil -> []
+| Cons (x, s) -> x :: (to_list s)
+| Lazy t -> to_list (Lazy.force t)
+
+let rec iter f = function
+| Nil -> ()
+| Cons (x, s) -> f x; iter f s
+| Lazy t -> iter f (Lazy.force t)
+
+let rec map f = function
+| Nil -> Nil
+| Cons (x, s) -> Cons (f x, map f s)
+| Lazy t -> Lazy (lazy (map f (Lazy.force t)))
+
+let rec app s1 s2 = match s1 with
+| Nil -> s2
+| Cons (x, s1) -> Cons (x, app s1 s2)
+| Lazy t ->
+  let t = lazy (app (Lazy.force t) s2) in
+  Lazy t
+
+let rec fold f accu = function
+| Nil -> accu
+| Cons (x, s) -> fold f (f accu x) s
+| Lazy t -> fold f accu (Lazy.force t)
+
+let rec map_filter f = function
+| Nil -> Nil
+| Cons (x, s) ->
+  begin match f x with
+  | None -> map_filter f s
+  | Some y -> Cons (y, map_filter f s)
+  end
+| Lazy t ->
+  let t = lazy (map_filter f (Lazy.force t)) in
+  Lazy t
+
+let rec concat = function
+| Nil -> Nil
+| Cons (s, sl) -> app s (concat sl)
+| Lazy t ->
+  let t = lazy (concat (Lazy.force t)) in
+  Lazy t
+
+let lempty = Lazy (lazy Nil)