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