src/Pure/ML-Systems/single_assignment.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 35014 a725ff6ead26
permissions -rw-r--r--
removed bash from ML system bootstrap, and past the Secure ML barrier;
     1 (*  Title:      Pure/ML-Systems/single_assignment.ML
     2     Author:     Makarius
     3 
     4 References with single assignment.  Unsynchronized!
     5 *)
     6 
     7 signature SINGLE_ASSIGNMENT =
     8 sig
     9   type 'a saref
    10   exception Locked
    11   val saref: unit -> 'a saref
    12   val savalue: 'a saref -> 'a option
    13   val saset: 'a saref * 'a -> unit
    14 end;
    15 
    16 structure SingleAssignment: SINGLE_ASSIGNMENT =
    17 struct
    18 
    19 exception Locked;
    20 
    21 abstype 'a saref = SARef of 'a option ref
    22 with
    23 
    24 fun saref () = SARef (ref NONE);
    25 
    26 fun savalue (SARef r) = ! r;
    27 
    28 fun saset (SARef (r as ref NONE), x) = r := SOME x
    29   | saset _ = raise Locked;
    30 
    31 end;
    32 
    33 end;