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