1 (* Title: Pure/General/lazy_seq.ML |
|
2 ID: $Id$ |
|
3 Author: Sebastian Skalberg, TU Muenchen |
|
4 |
|
5 Alternative version of lazy sequences. |
|
6 *) |
|
7 |
|
8 signature LAZY_SEQ = |
|
9 sig |
|
10 |
|
11 type 'a seq |
|
12 |
|
13 (* From LIST *) |
|
14 |
|
15 val null : 'a seq -> bool |
|
16 val length : 'a seq -> int |
|
17 val @ : 'a seq * 'a seq -> 'a seq |
|
18 val hd : 'a seq -> 'a |
|
19 val tl : 'a seq -> 'a seq |
|
20 val last : 'a seq -> 'a |
|
21 val getItem : 'a seq -> ('a * 'a seq) option |
|
22 val nth : 'a seq * int -> 'a |
|
23 val take : 'a seq * int -> 'a seq |
|
24 val drop : 'a seq * int -> 'a seq |
|
25 val rev : 'a seq -> 'a seq |
|
26 val concat : 'a seq seq -> 'a seq |
|
27 val revAppend : 'a seq * 'a seq -> 'a seq |
|
28 val app : ('a -> unit) -> 'a seq -> unit |
|
29 val map : ('a -> 'b) -> 'a seq -> 'b seq |
|
30 val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq |
|
31 val find : ('a -> bool) -> 'a seq -> 'a option |
|
32 val filter : ('a -> bool) -> 'a seq -> 'a seq |
|
33 val partition : ('a -> bool) |
|
34 -> 'a seq -> 'a seq * 'a seq |
|
35 val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b |
|
36 val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b |
|
37 val exists : ('a -> bool) -> 'a seq -> bool |
|
38 val all : ('a -> bool) -> 'a seq -> bool |
|
39 val tabulate : int * (int -> 'a) -> 'a seq |
|
40 val collate : ('a * 'a -> order) |
|
41 -> 'a seq * 'a seq -> order |
|
42 |
|
43 (* Miscellaneous *) |
|
44 |
|
45 val cycle : ((unit ->'a seq) -> 'a seq) -> 'a seq |
|
46 val iterates : ('a -> 'a) -> 'a -> 'a seq |
|
47 val of_function: (unit -> 'a option) -> 'a seq |
|
48 val of_string : string -> char seq |
|
49 val of_instream: TextIO.instream -> char seq |
|
50 |
|
51 (* From SEQ *) |
|
52 |
|
53 val make: (unit -> ('a * 'a seq) option) -> 'a seq |
|
54 val empty: 'a -> 'a seq |
|
55 val cons: 'a * 'a seq -> 'a seq |
|
56 val single: 'a -> 'a seq |
|
57 val try: ('a -> 'b) -> 'a -> 'b seq |
|
58 val chop: int * 'a seq -> 'a list * 'a seq |
|
59 val list_of: 'a seq -> 'a list |
|
60 val of_list: 'a list -> 'a seq |
|
61 val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq |
|
62 val interleave: 'a seq * 'a seq -> 'a seq |
|
63 val print: (int -> 'a -> unit) -> int -> 'a seq -> unit |
|
64 val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq |
|
65 val commute: 'a seq list -> 'a list seq |
|
66 val succeed: 'a -> 'a seq |
|
67 val fail: 'a -> 'b seq |
|
68 val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq |
|
69 val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
70 val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
71 val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq |
|
72 val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq |
|
73 val TRY: ('a -> 'a seq) -> 'a -> 'a seq |
|
74 val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq |
|
75 val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq |
|
76 val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq |
|
77 val DETERM: ('a -> 'b seq) -> 'a -> 'b seq |
|
78 |
|
79 end |
|
80 |
|
81 structure LazySeq :> LAZY_SEQ = |
|
82 struct |
|
83 |
|
84 open Susp |
|
85 |
|
86 datatype 'a seq = Seq of ('a * 'a seq) option susp |
|
87 |
|
88 exception Empty |
|
89 |
|
90 fun getItem (Seq s) = force s |
|
91 fun make f = Seq (delay f) |
|
92 |
|
93 fun null s = isSome (getItem s) |
|
94 |
|
95 local |
|
96 fun F n NONE = n |
|
97 | F n (SOME(_,s)) = F (n+1) (getItem s) |
|
98 in |
|
99 fun length s = F 0 (getItem s) |
|
100 end |
|
101 |
|
102 fun s1 @ s2 = |
|
103 let |
|
104 fun F NONE = getItem s2 |
|
105 | F (SOME(x,s1')) = SOME(x,F' s1') |
|
106 and F' s = make (fn () => F (getItem s)) |
|
107 in |
|
108 F' s1 |
|
109 end |
|
110 |
|
111 local |
|
112 fun F NONE = raise Empty |
|
113 | F (SOME arg) = arg |
|
114 in |
|
115 fun hd s = #1 (F (getItem s)) |
|
116 fun tl s = #2 (F (getItem s)) |
|
117 end |
|
118 |
|
119 local |
|
120 fun F x NONE = x |
|
121 | F _ (SOME(x,s)) = F x (getItem s) |
|
122 fun G NONE = raise Empty |
|
123 | G (SOME(x,s)) = F x (getItem s) |
|
124 in |
|
125 fun last s = G (getItem s) |
|
126 end |
|
127 |
|
128 local |
|
129 fun F NONE _ = raise Subscript |
|
130 | F (SOME(x,_)) 0 = x |
|
131 | F (SOME(_,s)) n = F (getItem s) (n-1) |
|
132 in |
|
133 fun nth(s,n) = |
|
134 if n < 0 |
|
135 then raise Subscript |
|
136 else F (getItem s) n |
|
137 end |
|
138 |
|
139 local |
|
140 fun F NONE _ = raise Subscript |
|
141 | F (SOME(x,s)) n = SOME(x,F' s (n-1)) |
|
142 and F' s 0 = Seq (value NONE) |
|
143 | F' s n = make (fn () => F (getItem s) n) |
|
144 in |
|
145 fun take (s,n) = |
|
146 if n < 0 |
|
147 then raise Subscript |
|
148 else F' s n |
|
149 end |
|
150 |
|
151 local |
|
152 fun F s 0 = s |
|
153 | F NONE _ = raise Subscript |
|
154 | F (SOME(_,s)) n = F (getItem s) (n-1) |
|
155 in |
|
156 fun drop (s,0) = s |
|
157 | drop (s,n) = |
|
158 if n < 0 |
|
159 then raise Subscript |
|
160 else make (fn () => F (getItem s) n) |
|
161 end |
|
162 |
|
163 local |
|
164 fun F s NONE = s |
|
165 | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s') |
|
166 in |
|
167 fun rev s = make (fn () => F NONE (getItem s)) |
|
168 end |
|
169 |
|
170 local |
|
171 fun F s NONE = getItem s |
|
172 | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s') |
|
173 in |
|
174 fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1)) |
|
175 end |
|
176 |
|
177 local |
|
178 fun F NONE = NONE |
|
179 | F (SOME(s1,s2)) = |
|
180 let |
|
181 fun G NONE = F (getItem s2) |
|
182 | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s))) |
|
183 in |
|
184 G (getItem s1) |
|
185 end |
|
186 in |
|
187 fun concat s = make (fn () => F (getItem s)) |
|
188 end |
|
189 |
|
190 fun app f = |
|
191 let |
|
192 fun F NONE = () |
|
193 | F (SOME(x,s)) = |
|
194 (f x; |
|
195 F (getItem s)) |
|
196 in |
|
197 F o getItem |
|
198 end |
|
199 |
|
200 fun map f = |
|
201 let |
|
202 fun F NONE = NONE |
|
203 | F (SOME(x,s)) = SOME(f x,F' s) |
|
204 and F' s = make (fn() => F (getItem s)) |
|
205 in |
|
206 F' |
|
207 end |
|
208 |
|
209 fun mapPartial f = |
|
210 let |
|
211 fun F NONE = NONE |
|
212 | F (SOME(x,s)) = |
|
213 (case f x of |
|
214 SOME y => SOME(y,F' s) |
|
215 | NONE => F (getItem s)) |
|
216 and F' s = make (fn()=> F (getItem s)) |
|
217 in |
|
218 F' |
|
219 end |
|
220 |
|
221 fun find P = |
|
222 let |
|
223 fun F NONE = NONE |
|
224 | F (SOME(x,s)) = |
|
225 if P x |
|
226 then SOME x |
|
227 else F (getItem s) |
|
228 in |
|
229 F o getItem |
|
230 end |
|
231 |
|
232 (*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*) |
|
233 |
|
234 fun filter P = |
|
235 let |
|
236 fun F NONE = NONE |
|
237 | F (SOME(x,s)) = |
|
238 if P x |
|
239 then SOME(x,F' s) |
|
240 else F (getItem s) |
|
241 and F' s = make (fn () => F (getItem s)) |
|
242 in |
|
243 F' |
|
244 end |
|
245 |
|
246 fun partition f s = |
|
247 let |
|
248 val s' = map (fn x => (x,f x)) s |
|
249 in |
|
250 (mapPartial (fn (x,true) => SOME x | _ => NONE) s', |
|
251 mapPartial (fn (x,false) => SOME x | _ => NONE) s') |
|
252 end |
|
253 |
|
254 fun exists P = |
|
255 let |
|
256 fun F NONE = false |
|
257 | F (SOME(x,s)) = P x orelse F (getItem s) |
|
258 in |
|
259 F o getItem |
|
260 end |
|
261 |
|
262 fun all P = |
|
263 let |
|
264 fun F NONE = true |
|
265 | F (SOME(x,s)) = P x andalso F (getItem s) |
|
266 in |
|
267 F o getItem |
|
268 end |
|
269 |
|
270 (*fun tabulate f = map f (iterates (fn x => x + 1) 0)*) |
|
271 |
|
272 fun tabulate (n,f) = |
|
273 let |
|
274 fun F n = make (fn () => SOME(f n,F (n+1))) |
|
275 in |
|
276 F n |
|
277 end |
|
278 |
|
279 fun collate c (s1,s2) = |
|
280 let |
|
281 fun F NONE _ = LESS |
|
282 | F _ NONE = GREATER |
|
283 | F (SOME(x,s1)) (SOME(y,s2)) = |
|
284 (case c (x,y) of |
|
285 LESS => LESS |
|
286 | GREATER => GREATER |
|
287 | EQUAL => F' s1 s2) |
|
288 and F' s1 s2 = F (getItem s1) (getItem s2) |
|
289 in |
|
290 F' s1 s2 |
|
291 end |
|
292 |
|
293 fun empty _ = Seq (value NONE) |
|
294 fun single x = Seq(value (SOME(x,Seq (value NONE)))) |
|
295 fun cons a = Seq(value (SOME a)) |
|
296 |
|
297 fun cycle seqfn = |
|
298 let |
|
299 val knot = ref (Seq (value NONE)) |
|
300 in |
|
301 knot := seqfn (fn () => !knot); |
|
302 !knot |
|
303 end |
|
304 |
|
305 fun iterates f = |
|
306 let |
|
307 fun F x = make (fn() => SOME(x,F (f x))) |
|
308 in |
|
309 F |
|
310 end |
|
311 |
|
312 fun interleave (s1,s2) = |
|
313 let |
|
314 fun F NONE = getItem s2 |
|
315 | F (SOME(x,s1')) = SOME(x,interleave(s2,s1')) |
|
316 in |
|
317 make (fn()=> F (getItem s1)) |
|
318 end |
|
319 |
|
320 (* val force_all = app ignore *) |
|
321 |
|
322 local |
|
323 fun F NONE = () |
|
324 | F (SOME(x,s)) = F (getItem s) |
|
325 in |
|
326 fun force_all s = F (getItem s) |
|
327 end |
|
328 |
|
329 fun of_function f = |
|
330 let |
|
331 fun F () = case f () of |
|
332 SOME x => SOME(x,make F) |
|
333 | NONE => NONE |
|
334 in |
|
335 make F |
|
336 end |
|
337 |
|
338 local |
|
339 fun F [] = NONE |
|
340 | F (x::xs) = SOME(x,F' xs) |
|
341 and F' xs = make (fn () => F xs) |
|
342 in |
|
343 fun of_list xs = F' xs |
|
344 end |
|
345 |
|
346 val of_string = of_list o String.explode |
|
347 |
|
348 fun of_instream is = |
|
349 let |
|
350 val buffer : char list ref = ref [] |
|
351 fun get_input () = |
|
352 case !buffer of |
|
353 (c::cs) => (buffer:=cs; |
|
354 SOME c) |
|
355 | [] => (case String.explode (TextIO.input is) of |
|
356 [] => NONE |
|
357 | (c::cs) => (buffer := cs; |
|
358 SOME c)) |
|
359 in |
|
360 of_function get_input |
|
361 end |
|
362 |
|
363 local |
|
364 fun F k NONE = k [] |
|
365 | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s) |
|
366 in |
|
367 fun list_of s = F (fn x => x) (getItem s) |
|
368 end |
|
369 |
|
370 (* Adapted from seq.ML *) |
|
371 |
|
372 val succeed = single |
|
373 fun fail _ = Seq (value NONE) |
|
374 |
|
375 (* fun op THEN (f, g) x = flat (map g (f x)) *) |
|
376 |
|
377 fun op THEN (f, g) = |
|
378 let |
|
379 fun F NONE = NONE |
|
380 | F (SOME(x,xs)) = |
|
381 let |
|
382 fun G NONE = F (getItem xs) |
|
383 | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys))) |
|
384 in |
|
385 G (getItem (g x)) |
|
386 end |
|
387 in |
|
388 fn x => make (fn () => F (getItem (f x))) |
|
389 end |
|
390 |
|
391 fun op ORELSE (f, g) x = |
|
392 make (fn () => |
|
393 case getItem (f x) of |
|
394 NONE => getItem (g x) |
|
395 | some => some) |
|
396 |
|
397 fun op APPEND (f, g) x = |
|
398 let |
|
399 fun copy s = |
|
400 case getItem s of |
|
401 NONE => getItem (g x) |
|
402 | SOME(x,xs) => SOME(x,make (fn () => copy xs)) |
|
403 in |
|
404 make (fn () => copy (f x)) |
|
405 end |
|
406 |
|
407 fun EVERY fs = foldr THEN succeed fs |
|
408 fun FIRST fs = foldr ORELSE fail fs |
|
409 |
|
410 fun TRY f x = |
|
411 make (fn () => |
|
412 case getItem (f x) of |
|
413 NONE => SOME(x,Seq (value NONE)) |
|
414 | some => some) |
|
415 |
|
416 fun REPEAT f = |
|
417 let |
|
418 fun rep qs x = |
|
419 case getItem (f x) of |
|
420 NONE => SOME(x, make (fn () => repq qs)) |
|
421 | SOME (x', q) => rep (q :: qs) x' |
|
422 and repq [] = NONE |
|
423 | repq (q :: qs) = |
|
424 case getItem q of |
|
425 NONE => repq qs |
|
426 | SOME (x, q) => rep (q :: qs) x |
|
427 in |
|
428 fn x => make (fn () => rep [] x) |
|
429 end |
|
430 |
|
431 fun REPEAT1 f = THEN (f, REPEAT f); |
|
432 |
|
433 fun INTERVAL f i = |
|
434 let |
|
435 fun F j = |
|
436 if i > j |
|
437 then single |
|
438 else op THEN (f j, F (j - 1)) |
|
439 in F end |
|
440 |
|
441 fun DETERM f x = |
|
442 make (fn () => |
|
443 case getItem (f x) of |
|
444 NONE => NONE |
|
445 | SOME (x', _) => SOME(x',Seq (value NONE))) |
|
446 |
|
447 (*partial function as procedure*) |
|
448 fun try f x = |
|
449 make (fn () => |
|
450 case Library.try f x of |
|
451 SOME y => SOME(y,Seq (value NONE)) |
|
452 | NONE => NONE) |
|
453 |
|
454 (*functional to print a sequence, up to "count" elements; |
|
455 the function prelem should print the element number and also the element*) |
|
456 fun print prelem count seq = |
|
457 let |
|
458 fun pr k xq = |
|
459 if k > count |
|
460 then () |
|
461 else |
|
462 case getItem xq of |
|
463 NONE => () |
|
464 | SOME (x, xq') => |
|
465 (prelem k x; |
|
466 writeln ""; |
|
467 pr (k + 1) xq') |
|
468 in |
|
469 pr 1 seq |
|
470 end |
|
471 |
|
472 (*accumulating a function over a sequence; this is lazy*) |
|
473 fun it_right f (xq, yq) = |
|
474 let |
|
475 fun its s = |
|
476 make (fn () => |
|
477 case getItem s of |
|
478 NONE => getItem yq |
|
479 | SOME (a, s') => getItem(f (a, its s'))) |
|
480 in |
|
481 its xq |
|
482 end |
|
483 |
|
484 (*map over a sequence s1, append the sequence s2*) |
|
485 fun mapp f s1 s2 = |
|
486 let |
|
487 fun F NONE = getItem s2 |
|
488 | F (SOME(x,s1')) = SOME(f x,F' s1') |
|
489 and F' s = make (fn () => F (getItem s)) |
|
490 in |
|
491 F' s1 |
|
492 end |
|
493 |
|
494 (*turn a list of sequences into a sequence of lists*) |
|
495 local |
|
496 fun F [] = SOME([],Seq (value NONE)) |
|
497 | F (xq :: xqs) = |
|
498 case getItem xq of |
|
499 NONE => NONE |
|
500 | SOME (x, xq') => |
|
501 (case F xqs of |
|
502 NONE => NONE |
|
503 | SOME (xs, xsq) => |
|
504 let |
|
505 fun G s = |
|
506 make (fn () => |
|
507 case getItem s of |
|
508 NONE => F (xq' :: xqs) |
|
509 | SOME(ys,ysq) => SOME(x::ys,G ysq)) |
|
510 in |
|
511 SOME (x :: xs, G xsq) |
|
512 end) |
|
513 in |
|
514 fun commute xqs = make (fn () => F xqs) |
|
515 end |
|
516 |
|
517 (*the list of the first n elements, paired with rest of sequence; |
|
518 if length of list is less than n, then sequence had less than n elements*) |
|
519 fun chop (n, xq) = |
|
520 if n <= 0 |
|
521 then ([], xq) |
|
522 else |
|
523 case getItem xq of |
|
524 NONE => ([], xq) |
|
525 | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')) |
|
526 |
|
527 fun foldl f e s = |
|
528 let |
|
529 fun F k NONE = k e |
|
530 | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s) |
|
531 in |
|
532 F (fn x => x) (getItem s) |
|
533 end |
|
534 |
|
535 fun foldr f e s = |
|
536 let |
|
537 fun F e NONE = e |
|
538 | F e (SOME(x,s)) = F (f(x,e)) (getItem s) |
|
539 in |
|
540 F e (getItem s) |
|
541 end |
|
542 |
|
543 end |
|