equal
deleted
inserted
replaced
1 (* Title: HOL/Import/lazy_seq.ML |
1 (* Title: HOL/Import/lazy_seq.ML |
2 ID: $Id$ |
|
3 Author: Sebastian Skalberg, TU Muenchen |
2 Author: Sebastian Skalberg, TU Muenchen |
4 |
3 |
5 Alternative version of lazy sequences. |
4 Alternative version of lazy sequences. |
6 *) |
5 *) |
7 |
6 |
406 | SOME(x,xs) => SOME(x,make (fn () => copy xs)) |
405 | SOME(x,xs) => SOME(x,make (fn () => copy xs)) |
407 in |
406 in |
408 make (fn () => copy (f x)) |
407 make (fn () => copy (f x)) |
409 end |
408 end |
410 |
409 |
411 fun EVERY fs = foldr (op THEN) succeed fs |
410 fun EVERY fs = List.foldr (op THEN) succeed fs |
412 fun FIRST fs = foldr (op ORELSE) fail fs |
411 fun FIRST fs = List.foldr (op ORELSE) fail fs |
413 |
412 |
414 fun TRY f x = |
413 fun TRY f x = |
415 make (fn () => |
414 make (fn () => |
416 case getItem (f x) of |
415 case getItem (f x) of |
417 NONE => SOME(x,Seq (Lazy.value NONE)) |
416 NONE => SOME(x,Seq (Lazy.value NONE)) |