| 32817 |      1 | (*  Title:      Pure/Concurrent/lazy_sequential.ML
 | 
|  |      2 |     Author:     Florian Haftmann and Makarius, TU Muenchen
 | 
|  |      3 | 
 | 
| 34278 |      4 | Lazy evaluation with memoing of results and regular exceptions
 | 
|  |      5 | (sequential version).
 | 
| 32817 |      6 | *)
 | 
|  |      7 | 
 | 
|  |      8 | structure Lazy: LAZY =
 | 
|  |      9 | struct
 | 
|  |     10 | 
 | 
|  |     11 | (* datatype *)
 | 
|  |     12 | 
 | 
|  |     13 | datatype 'a expr =
 | 
|  |     14 |   Expr of unit -> 'a |
 | 
|  |     15 |   Result of 'a Exn.result;
 | 
|  |     16 | 
 | 
|  |     17 | abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
 | 
|  |     18 | with
 | 
|  |     19 | 
 | 
|  |     20 | fun peek (Lazy r) =
 | 
|  |     21 |   (case ! r of
 | 
|  |     22 |     Expr _ => NONE
 | 
| 32844 |     23 |   | Result res => SOME res);
 | 
| 32817 |     24 | 
 | 
|  |     25 | fun lazy e = Lazy (Unsynchronized.ref (Expr e));
 | 
|  |     26 | fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
 | 
|  |     27 | 
 | 
|  |     28 | 
 | 
|  |     29 | (* force result *)
 | 
|  |     30 | 
 | 
|  |     31 | fun force_result (Lazy r) =
 | 
| 34278 |     32 |   let
 | 
|  |     33 |     val result =
 | 
|  |     34 |       (case ! r of
 | 
|  |     35 |         Expr e => Exn.capture e ()
 | 
|  |     36 |       | Result res => res);
 | 
|  |     37 |     val _ =
 | 
|  |     38 |       (case result of
 | 
|  |     39 |         Exn.Exn Exn.Interrupt => ()
 | 
| 34293 |     40 |       | _ => r := Result result);
 | 
| 34278 |     41 |   in result end;
 | 
| 32817 |     42 | 
 | 
|  |     43 | fun force r = Exn.release (force_result r);
 | 
|  |     44 | 
 | 
|  |     45 | end;
 | 
|  |     46 | end;
 | 
|  |     47 | 
 | 
|  |     48 | type 'a lazy = 'a Lazy.lazy;
 | 
|  |     49 | 
 |