src/Pure/General/susp.ML
changeset 20594 b80c4a5cd018
child 23922 707639e9497d
equal deleted inserted replaced
20593:5af400cc64d5 20594:b80c4a5cd018
       
     1 (*  Title:      Pure/General/susp.ML
       
     2     ID:         $Id$
       
     3     Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
       
     4 
       
     5 Delayed evaluation.
       
     6 *)
       
     7 
       
     8 signature SUSP =
       
     9 sig
       
    10   type 'a T
       
    11   val value: 'a -> 'a T
       
    12   val delay: (unit -> 'a) -> 'a T
       
    13   val force: 'a T -> 'a
       
    14   val peek: 'a T -> 'a option
       
    15   val same: 'a T * 'a T -> bool
       
    16 end
       
    17 
       
    18 structure Susp : SUSP =
       
    19 struct
       
    20 
       
    21 datatype 'a susp =
       
    22     Value of 'a
       
    23   | Delay of unit -> 'a;
       
    24 
       
    25 type 'a T = 'a susp ref;
       
    26 
       
    27 fun value v = ref (Value v);
       
    28 
       
    29 fun delay f = ref (Delay f);
       
    30 
       
    31 fun force (ref (Value v)) = v
       
    32   | force (r as ref (Delay f)) =
       
    33       let
       
    34         val v = f ()
       
    35       in
       
    36         r := Value v;
       
    37         v
       
    38       end;
       
    39 
       
    40 fun peek (ref (Value v)) = SOME v
       
    41   | peek (ref (Delay _)) = NONE;
       
    42 
       
    43 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
       
    44 
       
    45 end