src/Pure/sequence.ML

-(*  Title: 	sequence
+(*  Title:      sequence
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1988  University of Cambridge
 
 Unbounded sequences implemented by closures.
 
 RECOMPUTES if sequence is re-inspected.

 
 
 signature SEQUENCE = 
   sig
   type 'a seq
-  val append	: 'a seq * 'a seq -> 'a seq
-  val chop	: int * 'a seq -> 'a list * 'a seq
-  val cons	: 'a * 'a seq -> 'a seq
-  val filters	: ('a -> bool) -> 'a seq -> 'a seq
-  val flats	: 'a seq seq -> 'a seq
-  val hd	: 'a seq -> 'a
+  val append    : 'a seq * 'a seq -> 'a seq
+  val chop      : int * 'a seq -> 'a list * 'a seq
+  val cons      : 'a * 'a seq -> 'a seq
+  val filters   : ('a -> bool) -> 'a seq -> 'a seq
+  val flats     : 'a seq seq -> 'a seq
+  val hd        : 'a seq -> 'a
   val interleave: 'a seq * 'a seq -> 'a seq
-  val its_right	: ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
-  val list_of_s	: 'a seq -> 'a list
-  val mapp	: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
-  val maps	: ('a -> 'b) -> 'a seq -> 'b seq
-  val null	: 'a seq
-  val prints	: (int -> 'a -> unit) -> int -> 'a seq -> unit
-  val pull	: 'a seq -> ('a * 'a seq) option
-  val s_of_list	: 'a list -> 'a seq
-  val seqof	: (unit -> ('a * 'a seq) option) -> 'a seq
-  val single	: 'a -> 'a seq
-  val tl	: 'a seq -> 'a seq
+  val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+  val list_of_s : 'a seq -> 'a list
+  val mapp      : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+  val maps      : ('a -> 'b) -> 'a seq -> 'b seq
+  val null      : 'a seq
+  val prints    : (int -> 'a -> unit) -> int -> 'a seq -> unit
+  val pull      : 'a seq -> ('a * 'a seq) option
+  val s_of_list : 'a list -> 'a seq
+  val seqof     : (unit -> ('a * 'a seq) option) -> 'a seq
+  val single    : 'a -> 'a seq
+  val tl        : 'a seq -> 'a seq
   end;
 
 
 functor SequenceFun () : SEQUENCE = 
 struct

 fun chop (n:int, s: 'a seq): 'a list * 'a seq =
   if n<=0 then ([],s)
   else case pull(s) of
            None => ([],s)
          | Some(x,s') => let val (xs,s'') = chop (n-1,s')
-		         in  (x::xs, s'')  end;
+                         in  (x::xs, s'')  end;
 
 (*conversion from sequence to list*)
 fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
         None => []
       | Some(x,s') => x :: list_of_s s';

 
 (*functional to print a sequence, up to "count" elements
   the function prelem should print the element number and also the element*)
 fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
   let fun pr (k,s) = 
-	   if k>count then ()
-	   else case pull(s) of
-	       None => ()
-	     | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
+           if k>count then ()
+           else case pull(s) of
+               None => ()
+             | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
   in  pr(1,s)  end;
 
 (*Map the function f over the sequence, making a new sequence*)
 fun maps f xq = seqof (fn()=> case pull(xq) of
         None       => None
       | Some(x,yq) => Some(f x,  maps f yq));
 
 (*Sequence append:  put the elements of xq in front of those of yq*)
 fun append (xq,yq)  =
   let fun copy xq = seqof (fn()=>
-	    case pull xq of  
-		 None       => pull yq
-	       | Some(x,xq') => Some (x, copy xq'))
+            case pull xq of  
+                 None       => pull yq
+               | Some(x,xq') => Some (x, copy xq'))
   in  copy xq end;
 
 (*Interleave elements of xq with those of yq -- fairer than append*)
 fun interleave (xq,yq) = seqof (fn()=>
       case pull(xq) of  
           None       => pull yq
-	| Some(x,xq') => Some (x, interleave(yq, xq')));
+        | Some(x,xq') => Some (x, interleave(yq, xq')));
 
 (*map over a sequence xq, append the sequence yq*)
 fun mapp f xq yq =
   let fun copy s = seqof (fn()=> 
             case pull(s) of
-	        None       => pull(yq)
+                None       => pull(yq)
               | Some(x,xq') => Some(f x, copy xq'))
   in  copy xq end;
 
 (*Flatten a sequence of sequences to a single sequence. *)
 fun flats ss = seqof (fn()=> case pull(ss) of

 
 (*accumulating a function over a sequence;  this is lazy*)
 fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
   let fun its s = seqof (fn()=>
             case pull(s) of
-	        None       => pull bstr
-	      | Some(a,s') => pull(f(a, its s')))
+                None       => pull bstr
+              | Some(a,s') => pull(f(a, its s')))
   in  its s end; 
 
 fun filters pred xq =
   let fun copy s = seqof (fn()=> 
             case pull(s) of
-	        None       => None
+                None       => None
               | Some(x,xq') => if pred x then Some(x, copy xq')
-			       else pull (copy xq') )
+                               else pull (copy xq') )
   in  copy xq end
 
 end;