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