4 files changed, 163 insertions, 1 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index e76162134..76fbbfdd5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -6,6 +6,7 @@ Option
 Store
 Exninfo
 Backtrace
+IStream
 Pp_control
 Loc
 Compat
@@ -120,7 +121,6 @@ Pretyping
 Declaremods
 
 Tok
-Int
 Lexer
 Ppextend
 Pputils
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 70e083de9..01f112715 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -7,6 +7,7 @@ Store
 Exninfo
 Backtrace
 IArray
+IStream
 Pp_control
 Flags
 Pp
diff --git a/lib/iStream.ml b/lib/iStream.ml
new file mode 100644
index 000000000..c1894da75
--- /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)
diff --git a/lib/iStream.mli b/lib/iStream.mli
new file mode 100644
index 000000000..2fcc92675
--- /dev/null
+++ b/lib/iStream.mli
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** {5 Purely functional streams}
+
+  Contrarily to OCaml module [Stream], these are meant to be used purely
+  functionally. This implies in particular that accessing an element does not
+  discard it. *)
+
+type +'a t
+(** Type of pure streams. *)
+
+(** {6 Constructors} *)
+
+val empty : 'a t
+(** The empty stream. *)
+
+val cons : 'a -> 'a t -> 'a t
+(** Append an element in front of a stream. *)
+
+val thunk : 'a t Lazy.t -> 'a t
+(** Internalize the lazyness of a stream. *)
+
+(** {6 Destructors} *)
+
+val is_empty : 'a t -> bool
+(** Whethere a stream is empty. *)
+
+val peek : 'a t -> ('a * 'a t) option
+(** Return the head and the tail of a stream, if any. *)
+
+(** {6 Standard operations}
+
+  The complexity of stream-returning functions depends on the lazy status of the
+  actual content of the stream, i.e. a lazy stream will be processed lazily.
+  Other functions are eager. *)
+
+val app : 'a t -> 'a t -> 'a t
+(** Append two streams. Not tail-rec. *)
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+(** Mapping of streams. Not tail-rec. *)
+
+val iter : ('a -> unit) -> 'a t -> unit
+(** Iteration over streams. *)
+
+val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+(** Fold over streams. *)
+
+val concat : 'a t t -> 'a t
+(** Appends recursively a stream of streams. *)
+
+val map_filter : ('a -> 'b option) -> 'a t -> 'b t
+(** Mixing [map] and [filter]. Not tail-rec. *)
+
+(** {6 Conversions} *)
+
+val of_list : 'a list -> 'a t
+(** Convert a list into a stream. *)
+
+val to_list : 'a t -> 'a list
+(** Convert a stream into a list. *)
+
+(** {6 Other}*)
+
+val force : 'a t -> 'a t
+(** Forces the whole stream. *)
+
+val lempty : 'a t
+(** Lazy empty stream. *)