src/Pure/General/lazy.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 29422 fdf396a24a9f
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
wenzelm@28673
     1
(*  Title:      Pure/General/lazy.ML
wenzelm@28673
     2
    Author:     Florian Haftmann and Makarius, TU Muenchen
wenzelm@28673
     3
wenzelm@28673
     4
Lazy evaluation with memoing.  Concurrency may lead to multiple
wenzelm@28673
     5
attempts of evaluation -- the first result persists.
wenzelm@28673
     6
*)
wenzelm@28673
     7
wenzelm@28673
     8
signature LAZY =
wenzelm@28673
     9
sig
wenzelm@28971
    10
  type 'a lazy
wenzelm@28971
    11
  val same: 'a lazy * 'a lazy -> bool
wenzelm@28971
    12
  val lazy: (unit -> 'a) -> 'a lazy
wenzelm@28971
    13
  val value: 'a -> 'a lazy
wenzelm@28971
    14
  val peek: 'a lazy -> 'a Exn.result option
wenzelm@29422
    15
  val force_result: 'a lazy -> 'a Exn.result
wenzelm@28971
    16
  val force: 'a lazy -> 'a
wenzelm@28971
    17
  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
wenzelm@28673
    18
end
wenzelm@28673
    19
wenzelm@28673
    20
structure Lazy :> LAZY =
wenzelm@28673
    21
struct
wenzelm@28673
    22
wenzelm@28673
    23
(* datatype *)
wenzelm@28673
    24
wenzelm@28971
    25
datatype 'a T =
wenzelm@28673
    26
  Lazy of unit -> 'a |
wenzelm@28673
    27
  Result of 'a Exn.result;
wenzelm@28673
    28
wenzelm@32738
    29
type 'a lazy = 'a T Unsynchronized.ref;
wenzelm@28673
    30
wenzelm@28971
    31
fun same (r1: 'a lazy, r2) = r1 = r2;
wenzelm@28673
    32
wenzelm@32738
    33
fun lazy e = Unsynchronized.ref (Lazy e);
wenzelm@32738
    34
fun value x = Unsynchronized.ref (Result (Exn.Result x));
wenzelm@28673
    35
wenzelm@28673
    36
fun peek r =
wenzelm@28673
    37
  (case ! r of
wenzelm@28673
    38
    Lazy _ => NONE
wenzelm@28673
    39
  | Result res => SOME res);
wenzelm@28673
    40
wenzelm@28673
    41
wenzelm@28673
    42
(* force result *)
wenzelm@28673
    43
wenzelm@29422
    44
fun force_result r =
wenzelm@28673
    45
  let
wenzelm@28673
    46
    (*potentially concurrent evaluation*)
wenzelm@28673
    47
    val res =
wenzelm@28673
    48
      (case ! r of
wenzelm@28673
    49
        Lazy e => Exn.capture e ()
wenzelm@28673
    50
      | Result res => res);
wenzelm@28673
    51
    (*assign result -- first one persists*)
wenzelm@28673
    52
    val res' = NAMED_CRITICAL "lazy" (fn () =>
wenzelm@28673
    53
      (case ! r of
wenzelm@28673
    54
        Lazy _ => (r := Result res; res)
wenzelm@28673
    55
      | Result res' => res'));
wenzelm@29422
    56
  in res' end;
wenzelm@29422
    57
wenzelm@29422
    58
fun force r = Exn.release (force_result r);
wenzelm@28673
    59
wenzelm@28673
    60
fun map_force f = value o f o force;
wenzelm@28673
    61
wenzelm@28673
    62
end;
wenzelm@28971
    63
wenzelm@28971
    64
type 'a lazy = 'a Lazy.lazy;
wenzelm@28971
    65