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