src/Pure/General/susp.ML
changeset 25310 2b928fb92f53
parent 24299 91d893799212
child 25317 8b38b394fa8e
equal deleted inserted replaced
25309:30142fd3babf 25310:2b928fb92f53
     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. Supposed to be value oriented; may result in
     5 Delayed evaluation. Supposed to be value-oriented.
     6 multiple evaluations in a multi-threaded environment!
       
     7 *)
     6 *)
     8 
     7 
     9 signature SUSP =
     8 signature SUSP =
    10 sig
     9 sig
    11   type 'a T
    10   type 'a T
    28 fun value v = ref (Value v);
    27 fun value v = ref (Value v);
    29 
    28 
    30 fun delay f = ref (Delay f);
    29 fun delay f = ref (Delay f);
    31 
    30 
    32 fun force susp =
    31 fun force susp =
    33   (case ! susp of
    32   let
    34     Value v => v
    33     fun forc () = case ! susp
    35   | Delay f =>
    34      of Value v => v
    36       let
    35       | Delay f =>
    37         val v = f ();
    36           let
    38         val _ = susp := Value v;
    37             val v = f ();
    39       in v end);
    38             val _ = susp := Value v;
       
    39           in v end;
       
    40   in case ! susp
       
    41    of Value v => v
       
    42     | Delay _ => NAMED_CRITICAL "sups" forc
       
    43   end;
    40 
    44 
    41 fun peek susp =
    45 fun peek susp =
    42   (case ! susp of
    46   (case ! susp of
    43     Value v => SOME v
    47     Value v => SOME v
    44   | Delay _ => NONE);
    48   | Delay _ => NONE);