|
1 (* Title: Pure/seq.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
|
5 Unbounded sequences implemented by closures. RECOMPUTES if sequence |
|
6 is re-inspected. Memoing, using polymorphic refs, was found to be |
|
7 slower! (More GCs) |
|
8 *) |
|
9 |
|
10 signature SEQ = |
|
11 sig |
|
12 type 'a seq |
|
13 val make: (unit -> ('a * 'a seq) option) -> 'a seq |
|
14 val pull: 'a seq -> ('a * 'a seq) option |
|
15 val empty: 'a seq |
|
16 val cons: 'a * 'a seq -> 'a seq |
|
17 val single: 'a -> 'a seq |
|
18 val hd: 'a seq -> 'a |
|
19 val tl: 'a seq -> 'a seq |
|
20 val chop: int * 'a seq -> 'a list * 'a seq |
|
21 val list_of: 'a seq -> 'a list |
|
22 val of_list: 'a list -> 'a seq |
|
23 val map: ('a -> 'b) -> 'a seq -> 'b seq |
|
24 val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq |
|
25 val append: 'a seq * 'a seq -> 'a seq |
|
26 val filter: ('a -> bool) -> 'a seq -> 'a seq |
|
27 val flat: 'a seq seq -> 'a seq |
|
28 val interleave: 'a seq * 'a seq -> 'a seq |
|
29 val print: (int -> 'a -> unit) -> int -> 'a seq -> unit |
|
30 val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq |
|
31 end; |
|
32 |
|
33 structure Seq: SEQ = |
|
34 struct |
|
35 |
|
36 |
|
37 datatype 'a seq = Seq of unit -> ('a * 'a seq) option; |
|
38 |
|
39 (*the abstraction for making a sequence*) |
|
40 val make = Seq; |
|
41 |
|
42 (*return next sequence element as None or Some (x, xq)*) |
|
43 fun pull (Seq f) = f (); |
|
44 |
|
45 |
|
46 (*the empty sequence*) |
|
47 val empty = make (fn () => None); |
|
48 |
|
49 (*prefix an element to the sequence -- use cons (x, xq) only if |
|
50 evaluation of xq need not be delayed, otherwise use |
|
51 make (fn () => Some (x, xq))*) |
|
52 fun cons x_xq = make (fn () => Some x_xq); |
|
53 |
|
54 fun single x = cons (x, empty); |
|
55 |
|
56 (*head and tail -- beware of calling the sequence function twice!!*) |
|
57 fun hd xq = #1 (the (pull xq)) |
|
58 and tl xq = #2 (the (pull xq)); |
|
59 |
|
60 |
|
61 (*the list of the first n elements, paired with rest of sequence; |
|
62 if length of list is less than n, then sequence had less than n elements*) |
|
63 fun chop (n, xq) = |
|
64 if n <= 0 then ([], xq) |
|
65 else |
|
66 (case pull xq of |
|
67 None => ([], xq) |
|
68 | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))); |
|
69 |
|
70 (*conversion from sequence to list*) |
|
71 fun list_of xq = |
|
72 (case pull xq of |
|
73 None => [] |
|
74 | Some (x, xq') => x :: list_of xq'); |
|
75 |
|
76 (*conversion from list to sequence*) |
|
77 fun of_list xs = foldr cons (xs, empty); |
|
78 |
|
79 |
|
80 (*map the function f over the sequence, making a new sequence*) |
|
81 fun map f xq = |
|
82 make (fn () => |
|
83 (case pull xq of |
|
84 None => None |
|
85 | Some (x, xq') => Some (f x, map f xq'))); |
|
86 |
|
87 (*map over a sequence xq, append the sequence yq*) |
|
88 fun mapp f xq yq = |
|
89 let |
|
90 fun copy s = |
|
91 make (fn () => |
|
92 (case pull s of |
|
93 None => pull yq |
|
94 | Some (x, s') => Some (f x, copy s'))) |
|
95 in copy xq end; |
|
96 |
|
97 (*sequence append: put the elements of xq in front of those of yq*) |
|
98 fun append (xq, yq) = |
|
99 let |
|
100 fun copy s = |
|
101 make (fn () => |
|
102 (case pull s of |
|
103 None => pull yq |
|
104 | Some (x, s') => Some (x, copy s'))) |
|
105 in copy xq end; |
|
106 |
|
107 (*filter sequence by predicate*) |
|
108 fun filter pred xq = |
|
109 let |
|
110 fun copy s = |
|
111 make (fn () => |
|
112 (case pull s of |
|
113 None => None |
|
114 | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s'))); |
|
115 in copy xq end; |
|
116 |
|
117 (*flatten a sequence of sequences to a single sequence*) |
|
118 fun flat xqq = |
|
119 make (fn () => |
|
120 (case pull xqq of |
|
121 None => None |
|
122 | Some (xq, xqq') => pull (append (xq, flat xqq')))); |
|
123 |
|
124 (*interleave elements of xq with those of yq -- fairer than append*) |
|
125 fun interleave (xq, yq) = |
|
126 make (fn () => |
|
127 (case pull xq of |
|
128 None => pull yq |
|
129 | Some (x, xq') => Some (x, interleave (yq, xq')))); |
|
130 |
|
131 |
|
132 (*functional to print a sequence, up to "count" elements; |
|
133 the function prelem should print the element number and also the element*) |
|
134 fun print prelem count seq = |
|
135 let |
|
136 fun pr (k, xq) = |
|
137 if k > count then () |
|
138 else |
|
139 (case pull xq of |
|
140 None => () |
|
141 | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq'))) |
|
142 in pr (1, seq) end; |
|
143 |
|
144 (*accumulating a function over a sequence; this is lazy*) |
|
145 fun it_right f (xq, yq) = |
|
146 let |
|
147 fun its s = |
|
148 make (fn () => |
|
149 (case pull s of |
|
150 None => pull yq |
|
151 | Some (a, s') => pull (f (a, its s')))) |
|
152 in its xq end; |
|
153 |
|
154 |
|
155 end; |