src/Pure/Concurrent/lazy_sequential.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 33023 207c21697a48
child 34278 228f27469139
permissions -rw-r--r--
map_range (and map_index) combinator
wenzelm@32817
     1
(*  Title:      Pure/Concurrent/lazy_sequential.ML
wenzelm@32817
     2
    Author:     Florian Haftmann and Makarius, TU Muenchen
wenzelm@32817
     3
wenzelm@32817
     4
Lazy evaluation with memoing (sequential version).
wenzelm@32817
     5
*)
wenzelm@32817
     6
wenzelm@32817
     7
structure Lazy: LAZY =
wenzelm@32817
     8
struct
wenzelm@32817
     9
wenzelm@32817
    10
(* datatype *)
wenzelm@32817
    11
wenzelm@32817
    12
datatype 'a expr =
wenzelm@32817
    13
  Expr of unit -> 'a |
wenzelm@32817
    14
  Result of 'a Exn.result;
wenzelm@32817
    15
wenzelm@32817
    16
abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
wenzelm@32817
    17
with
wenzelm@32817
    18
wenzelm@32817
    19
fun peek (Lazy r) =
wenzelm@32817
    20
  (case ! r of
wenzelm@32817
    21
    Expr _ => NONE
wenzelm@32844
    22
  | Result res => SOME res);
wenzelm@32817
    23
wenzelm@32817
    24
fun lazy e = Lazy (Unsynchronized.ref (Expr e));
wenzelm@32817
    25
fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
wenzelm@32817
    26
wenzelm@32817
    27
wenzelm@32817
    28
(* force result *)
wenzelm@32817
    29
wenzelm@32817
    30
fun force_result (Lazy r) =
wenzelm@32817
    31
  (case ! r of
wenzelm@32817
    32
    Expr e => Exn.capture e ()
wenzelm@32817
    33
  | Result res => res);
wenzelm@32817
    34
wenzelm@32817
    35
fun force r = Exn.release (force_result r);
wenzelm@32817
    36
wenzelm@32817
    37
end;
wenzelm@32817
    38
end;
wenzelm@32817
    39
wenzelm@32817
    40
type 'a lazy = 'a Lazy.lazy;
wenzelm@32817
    41