|
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 val succeed: 'a -> 'a seq |
|
32 val fail: 'a -> 'b seq |
|
33 val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq |
|
34 val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
35 val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
36 val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq |
|
37 val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq |
|
38 val TRY: ('a -> 'a seq) -> 'a -> 'a seq |
|
39 val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq |
|
40 end; |
|
41 |
|
42 structure Seq: SEQ = |
|
43 struct |
|
44 |
|
45 |
|
46 (** lazy sequences **) |
|
47 |
|
48 datatype 'a seq = Seq of unit -> ('a * 'a seq) option; |
|
49 |
|
50 (*the abstraction for making a sequence*) |
|
51 val make = Seq; |
|
52 |
|
53 (*return next sequence element as None or Some (x, xq)*) |
|
54 fun pull (Seq f) = f (); |
|
55 |
|
56 |
|
57 (*the empty sequence*) |
|
58 val empty = Seq (fn () => None); |
|
59 |
|
60 (*prefix an element to the sequence -- use cons (x, xq) only if |
|
61 evaluation of xq need not be delayed, otherwise use |
|
62 make (fn () => Some (x, xq))*) |
|
63 fun cons x_xq = make (fn () => Some x_xq); |
|
64 |
|
65 fun single x = cons (x, empty); |
|
66 |
|
67 (*head and tail -- beware of calling the sequence function twice!!*) |
|
68 fun hd xq = #1 (the (pull xq)) |
|
69 and tl xq = #2 (the (pull xq)); |
|
70 |
|
71 |
|
72 (*the list of the first n elements, paired with rest of sequence; |
|
73 if length of list is less than n, then sequence had less than n elements*) |
|
74 fun chop (n, xq) = |
|
75 if n <= 0 then ([], xq) |
|
76 else |
|
77 (case pull xq of |
|
78 None => ([], xq) |
|
79 | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))); |
|
80 |
|
81 (*conversion from sequence to list*) |
|
82 fun list_of xq = |
|
83 (case pull xq of |
|
84 None => [] |
|
85 | Some (x, xq') => x :: list_of xq'); |
|
86 |
|
87 (*conversion from list to sequence*) |
|
88 fun of_list xs = foldr cons (xs, empty); |
|
89 |
|
90 |
|
91 (*map the function f over the sequence, making a new sequence*) |
|
92 fun map f xq = |
|
93 make (fn () => |
|
94 (case pull xq of |
|
95 None => None |
|
96 | Some (x, xq') => Some (f x, map f xq'))); |
|
97 |
|
98 (*map over a sequence xq, append the sequence yq*) |
|
99 fun mapp f xq yq = |
|
100 let |
|
101 fun copy s = |
|
102 make (fn () => |
|
103 (case pull s of |
|
104 None => pull yq |
|
105 | Some (x, s') => Some (f x, copy s'))) |
|
106 in copy xq end; |
|
107 |
|
108 (*sequence append: put the elements of xq in front of those of yq*) |
|
109 fun append (xq, yq) = |
|
110 let |
|
111 fun copy s = |
|
112 make (fn () => |
|
113 (case pull s of |
|
114 None => pull yq |
|
115 | Some (x, s') => Some (x, copy s'))) |
|
116 in copy xq end; |
|
117 |
|
118 (*filter sequence by predicate*) |
|
119 fun filter pred xq = |
|
120 let |
|
121 fun copy s = |
|
122 make (fn () => |
|
123 (case pull s of |
|
124 None => None |
|
125 | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s'))); |
|
126 in copy xq end; |
|
127 |
|
128 (*flatten a sequence of sequences to a single sequence*) |
|
129 fun flat xqq = |
|
130 make (fn () => |
|
131 (case pull xqq of |
|
132 None => None |
|
133 | Some (xq, xqq') => pull (append (xq, flat xqq')))); |
|
134 |
|
135 (*interleave elements of xq with those of yq -- fairer than append*) |
|
136 fun interleave (xq, yq) = |
|
137 make (fn () => |
|
138 (case pull xq of |
|
139 None => pull yq |
|
140 | Some (x, xq') => Some (x, interleave (yq, xq')))); |
|
141 |
|
142 |
|
143 (*functional to print a sequence, up to "count" elements; |
|
144 the function prelem should print the element number and also the element*) |
|
145 fun print prelem count seq = |
|
146 let |
|
147 fun pr (k, xq) = |
|
148 if k > count then () |
|
149 else |
|
150 (case pull xq of |
|
151 None => () |
|
152 | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq'))) |
|
153 in pr (1, seq) end; |
|
154 |
|
155 (*accumulating a function over a sequence; this is lazy*) |
|
156 fun it_right f (xq, yq) = |
|
157 let |
|
158 fun its s = |
|
159 make (fn () => |
|
160 (case pull s of |
|
161 None => pull yq |
|
162 | Some (a, s') => pull (f (a, its s')))) |
|
163 in its xq end; |
|
164 |
|
165 |
|
166 |
|
167 (** sequence functions **) (*some code duplicated from Pure/tctical.ML*) |
|
168 |
|
169 fun succeed x = single x; |
|
170 fun fail _ = empty; |
|
171 |
|
172 |
|
173 fun THEN (f, g) x = flat (map g (f x)); |
|
174 |
|
175 fun ORELSE (f, g) x = |
|
176 (case pull (f x) of |
|
177 None => g x |
|
178 | some => make (fn () => some)); |
|
179 |
|
180 fun APPEND (f, g) x = |
|
181 append (f x, make (fn () => pull (g x))); |
|
182 |
|
183 |
|
184 fun EVERY fs = foldr THEN (fs, succeed); |
|
185 fun FIRST fs = foldr ORELSE (fs, fail); |
|
186 |
|
187 |
|
188 fun TRY f = ORELSE (f, succeed); |
|
189 |
|
190 fun REPEAT f = |
|
191 let |
|
192 fun rep qs x = |
|
193 (case pull (f x) of |
|
194 None => Some (x, make (fn () => repq qs)) |
|
195 | Some (x', q) => rep (q :: qs) x') |
|
196 and repq [] = None |
|
197 | repq (q :: qs) = |
|
198 (case pull q of |
|
199 None => repq qs |
|
200 | Some (x, q) => rep (q :: qs) x); |
|
201 in fn x => make (fn () => rep [] x) end; |
|
202 |
|
203 |
|
204 end; |