src/Pure/Concurrent/lazy_sequential.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 34293 df93c72c0206
child 43761 e72ba84ae58f
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm@32817
     1
(*  Title:      Pure/Concurrent/lazy_sequential.ML
wenzelm@32817
     2
    Author:     Florian Haftmann and Makarius, TU Muenchen
wenzelm@32817
     3
wenzelm@34278
     4
Lazy evaluation with memoing of results and regular exceptions
wenzelm@34278
     5
(sequential version).
wenzelm@32817
     6
*)
wenzelm@32817
     7
wenzelm@32817
     8
structure Lazy: LAZY =
wenzelm@32817
     9
struct
wenzelm@32817
    10
wenzelm@32817
    11
(* datatype *)
wenzelm@32817
    12
wenzelm@32817
    13
datatype 'a expr =
wenzelm@32817
    14
  Expr of unit -> 'a |
wenzelm@32817
    15
  Result of 'a Exn.result;
wenzelm@32817
    16
wenzelm@32817
    17
abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
wenzelm@32817
    18
with
wenzelm@32817
    19
wenzelm@32817
    20
fun peek (Lazy r) =
wenzelm@32817
    21
  (case ! r of
wenzelm@32817
    22
    Expr _ => NONE
wenzelm@32844
    23
  | Result res => SOME res);
wenzelm@32817
    24
wenzelm@32817
    25
fun lazy e = Lazy (Unsynchronized.ref (Expr e));
wenzelm@32817
    26
fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
wenzelm@32817
    27
wenzelm@32817
    28
wenzelm@32817
    29
(* force result *)
wenzelm@32817
    30
wenzelm@32817
    31
fun force_result (Lazy r) =
wenzelm@34278
    32
  let
wenzelm@34278
    33
    val result =
wenzelm@34278
    34
      (case ! r of
wenzelm@34278
    35
        Expr e => Exn.capture e ()
wenzelm@34278
    36
      | Result res => res);
wenzelm@39232
    37
    val _ = if Exn.is_interrupt_exn result then () else r := Result result;
wenzelm@34278
    38
  in result end;
wenzelm@32817
    39
wenzelm@32817
    40
fun force r = Exn.release (force_result r);
wenzelm@32817
    41
wenzelm@32817
    42
end;
wenzelm@32817
    43
end;
wenzelm@32817
    44
wenzelm@32817
    45
type 'a lazy = 'a Lazy.lazy;
wenzelm@32817
    46