src/Pure/General/susp.ML
changeset 14278 ae499452700a
child 16179 fa7e70be26b0
equal deleted inserted replaced
14277:ad66687ece6e 14278:ae499452700a
       
     1 signature SUSP =
       
     2 sig
       
     3 
       
     4 type 'a susp
       
     5 
       
     6 val force : 'a susp -> 'a
       
     7 val delay : (unit -> 'a) -> 'a susp
       
     8 val value : 'a -> 'a susp
       
     9 
       
    10 end
       
    11 
       
    12 structure Susp :> SUSP =
       
    13 struct
       
    14 
       
    15 datatype 'a suspVal
       
    16   = Value of 'a
       
    17   | Delay of unit -> 'a
       
    18 
       
    19 type 'a susp = 'a suspVal ref
       
    20 
       
    21 fun force (ref (Value v)) = v
       
    22   | force (r as ref (Delay f)) =
       
    23     let
       
    24 	val v = f ()
       
    25     in
       
    26 	r := Value v;
       
    27 	v
       
    28     end
       
    29 
       
    30 fun delay f = ref (Delay f)
       
    31 
       
    32 fun value v = ref (Value v)
       
    33 
       
    34 end