src/Pure/Concurrent/lazy.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@32815
     1
(*  Title:      Pure/Concurrent/lazy.ML
wenzelm@32815
     2
    Author:     Makarius
wenzelm@28673
     3
wenzelm@32815
     4
Lazy evaluation based on futures.
wenzelm@28673
     5
*)
wenzelm@28673
     6
wenzelm@28673
     7
signature LAZY =
wenzelm@28673
     8
sig
wenzelm@28971
     9
  type 'a lazy
wenzelm@32815
    10
  val peek: 'a lazy -> 'a Exn.result option
wenzelm@28971
    11
  val lazy: (unit -> 'a) -> 'a lazy
wenzelm@28971
    12
  val value: 'a -> 'a lazy
wenzelm@29422
    13
  val force_result: 'a lazy -> 'a Exn.result
wenzelm@28971
    14
  val force: 'a lazy -> 'a
wenzelm@32815
    15
end;
wenzelm@28673
    16
wenzelm@32815
    17
structure Lazy: LAZY =
wenzelm@28673
    18
struct
wenzelm@28673
    19
wenzelm@28673
    20
(* datatype *)
wenzelm@28673
    21
wenzelm@32815
    22
datatype 'a expr =
wenzelm@32815
    23
  Expr of unit -> 'a |
wenzelm@32815
    24
  Future of 'a future;
wenzelm@28673
    25
wenzelm@32815
    26
abstype 'a lazy = Lazy of 'a expr Synchronized.var
wenzelm@32815
    27
with
wenzelm@28673
    28
wenzelm@32815
    29
fun peek (Lazy var) =
wenzelm@32815
    30
  (case Synchronized.value var of
wenzelm@32815
    31
    Expr _ => NONE
wenzelm@32815
    32
  | Future x => Future.peek x);
wenzelm@28673
    33
wenzelm@32815
    34
fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
wenzelm@32815
    35
fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
wenzelm@28673
    36
wenzelm@28673
    37
wenzelm@28673
    38
(* force result *)
wenzelm@28673
    39
wenzelm@32815
    40
fun force_result (Lazy var) =
wenzelm@32815
    41
  (case peek (Lazy var) of
wenzelm@32815
    42
    SOME res => res
wenzelm@32815
    43
  | NONE =>
wenzelm@32815
    44
      Synchronized.guarded_access var
wenzelm@32815
    45
        (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
wenzelm@32815
    46
          | Future x => SOME (x, Future x))
wenzelm@32815
    47
      |> Future.join_result);
wenzelm@29422
    48
wenzelm@29422
    49
fun force r = Exn.release (force_result r);
wenzelm@28673
    50
wenzelm@28673
    51
end;
wenzelm@32815
    52
end;
wenzelm@28971
    53
wenzelm@28971
    54
type 'a lazy = 'a Lazy.lazy;
wenzelm@28971
    55