src/HOL/Import/susp.ML
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17802 f3b1ca16cebd
permissions -rw-r--r--
adaptions to codegen_package
     1 (*  Title:      HOL/Import/susp.ML
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg, TU Muenchen
     4 
     5 Delayed evaluation.
     6 *)
     7 
     8 signature SUSP =
     9 sig
    10 
    11 type 'a susp
    12 
    13 val force : 'a susp -> 'a
    14 val delay : (unit -> 'a) -> 'a susp
    15 val value : 'a -> 'a susp
    16 
    17 end
    18 
    19 structure Susp :> SUSP =
    20 struct
    21 
    22 datatype 'a suspVal
    23   = Value of 'a
    24   | Delay of unit -> 'a
    25 
    26 type 'a susp = 'a suspVal ref
    27 
    28 fun force (ref (Value v)) = v
    29   | force (r as ref (Delay f)) =
    30     let
    31 	val v = f ()
    32     in
    33 	r := Value v;
    34 	v
    35     end
    36 
    37 fun delay f = ref (Delay f)
    38 
    39 fun value v = ref (Value v)
    40 
    41 end