src/Pure/sequence.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 669 a6dd3796009d
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	sequence
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1988  University of Cambridge
     5 *)
     6 
     7 (*Unbounded sequences implemented by closures.
     8 
     9   Could use   'a seq = Seq of ('a * (unit -> 'a seq)) option.
    10   Recomputes if sequence is re-inspected; memoing would need polymorphic refs.
    11 *)
    12 
    13 
    14 signature SEQUENCE = 
    15   sig
    16   type 'a seq
    17   val append : 'a seq * 'a seq -> 'a seq
    18   val chop: int * 'a seq -> 'a list * 'a seq
    19   val cons: 'a * 'a seq -> 'a seq
    20   val filters: ('a -> bool) -> 'a seq -> 'a seq
    21   val flats: 'a seq seq -> 'a seq
    22   val interleave : 'a seq * 'a seq -> 'a seq
    23   val its_right: ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    24   val list_of_s: 'a seq -> 'a list
    25   val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    26   val maps: ('a -> 'b) -> 'a seq -> 'b seq
    27   val null: 'a seq
    28   val prints: (int -> 'a -> unit) -> int -> 'a seq -> unit
    29   val pull: 'a seq -> ('a * 'a seq) option
    30   val s_of_list: 'a list -> 'a seq
    31   val seqof: (unit -> ('a * 'a seq) option) -> 'a seq
    32   val single: 'a -> 'a seq
    33   end;
    34 
    35 
    36 functor SequenceFun () : SEQUENCE = 
    37 struct
    38     
    39 datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
    40 
    41 (*Return next sequence element as None or Some(x,str) *)
    42 fun pull(Seq f) = f();
    43 
    44 (*the abstraction for making a sequence*)
    45 val seqof = Seq;
    46 
    47 (*prefix an element to the sequence
    48     use cons(x,s) only if evaluation of s need not be delayed,
    49       otherwise use seqof(fn()=> Some(x,s)) *)
    50 fun cons all = Seq(fn()=>Some all);
    51 
    52 (*the empty sequence*)
    53 val null = Seq(fn()=>None);
    54 
    55 fun single(x) = cons (x, null);
    56 
    57 (*The list of the first n elements, paired with rest of sequence.
    58   If length of list is less than n, then sequence had less than n elements.*)
    59 fun chop (n:int, s: 'a seq): 'a list * 'a seq =
    60   if n<=0 then ([],s)
    61   else case pull(s) of
    62            None => ([],s)
    63          | Some(x,s') => let val (xs,s'') = chop (n-1,s')
    64 		         in  (x::xs, s'')  end;
    65 
    66 (*conversion from sequence to list*)
    67 fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
    68         None => []
    69       | Some(x,s') => x :: list_of_s s';
    70 
    71 
    72 (*conversion from list to sequence*)
    73 fun s_of_list []     = null
    74   | s_of_list (x::l) = cons (x, s_of_list l);
    75 
    76 
    77 (*functional to print a sequence, up to "count" elements
    78   the function prelem should print the element number and also the element*)
    79 fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
    80   let fun pr (k,s) = 
    81 	   if k>count then ()
    82 	   else case pull(s) of
    83 	       None => ()
    84 	     | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
    85   in  pr(1,s)  end;
    86 
    87 (*Map the function f over the sequence, making a new sequence*)
    88 fun maps f xq = seqof (fn()=> case pull(xq) of
    89         None       => None
    90       | Some(x,yq) => Some(f x,  maps f yq));
    91 
    92 (*Sequence append:  put the elements of xq in front of those of yq*)
    93 fun append (xq,yq)  =
    94   let fun copy xq = seqof (fn()=>
    95 	    case pull xq of  
    96 		 None       => pull yq
    97 	       | Some(x,xq') => Some (x, copy xq'))
    98   in  copy xq end;
    99 
   100 (*Interleave elements of xq with those of yq -- fairer than append*)
   101 fun interleave (xq,yq) = seqof (fn()=>
   102       case pull(xq) of  
   103           None       => pull yq
   104 	| Some(x,xq') => Some (x, interleave(yq, xq')));
   105 
   106 (*map over a sequence xq, append the sequence yq*)
   107 fun mapp f xq yq =
   108   let fun copy s = seqof (fn()=> 
   109             case pull(s) of
   110 	        None       => pull(yq)
   111               | Some(x,xq') => Some(f x, copy xq'))
   112   in  copy xq end;
   113 
   114 (*Flatten a sequence of sequences to a single sequence. *)
   115 fun flats ss = seqof (fn()=> case pull(ss) of
   116         None => None
   117       | Some(s,ss') =>  pull(append(s, flats ss')));
   118 
   119 (*accumulating a function over a sequence;  this is lazy*)
   120 fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
   121   let fun its s = seqof (fn()=>
   122             case pull(s) of
   123 	        None       => pull bstr
   124 	      | Some(a,s') => pull(f(a, its s')))
   125   in  its s end; 
   126 
   127 fun filters pred xq =
   128   let fun copy s = seqof (fn()=> 
   129             case pull(s) of
   130 	        None       => None
   131               | Some(x,xq') => if pred x then Some(x, copy xq')
   132 			       else pull (copy xq') )
   133   in  copy xq end
   134 
   135 end;