src/Pure/General/susp.ML
changeset 24299 91d893799212
parent 24058 81aafd465662
child 25310 2b928fb92f53
equal deleted inserted replaced
24298:229fdfc1ddd9 24299:91d893799212
     1 (*  Title:      Pure/General/susp.ML
     1 (*  Title:      Pure/General/susp.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
     3     Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
     4 
     4 
     5 Delayed evaluation.
     5 Delayed evaluation. Supposed to be value oriented; may result in
       
     6 multiple evaluations in a multi-threaded environment!
     6 *)
     7 *)
     7 
     8 
     8 signature SUSP =
     9 signature SUSP =
     9 sig
    10 sig
    10   type 'a T
    11   type 'a T
    26 
    27 
    27 fun value v = ref (Value v);
    28 fun value v = ref (Value v);
    28 
    29 
    29 fun delay f = ref (Delay f);
    30 fun delay f = ref (Delay f);
    30 
    31 
    31 fun force susp = NAMED_CRITICAL "susp" (fn () =>
    32 fun force susp =
    32   (case ! susp of
    33   (case ! susp of
    33     Value v => v
    34     Value v => v
    34   | Delay f =>
    35   | Delay f =>
    35       let
    36       let
    36         val v = f ();
    37         val v = f ();
    37         val _ = susp := Value v;
    38         val _ = susp := Value v;
    38       in v end));
    39       in v end);
    39 
    40 
    40 fun peek susp =
    41 fun peek susp =
    41   (case ! susp of
    42   (case ! susp of
    42     Value v => SOME v
    43     Value v => SOME v
    43   | Delay _ => NONE);
    44   | Delay _ => NONE);
    44 
    45 
    45 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
    46 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
    46 
    47 
    47 end
    48 end;