src/Pure/ML-Systems/single_assignment_polyml.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_polyml.ML
     2     Author:     Makarius
     3 
     4 References with single assignment.  Unsynchronized!  Emulates
     5 structure SingleAssignment from Poly/ML 5.4.
     6 *)
     7 
     8 signature SINGLE_ASSIGNMENT =
     9 sig
    10   type 'a saref
    11   exception Locked
    12   val saref: unit -> 'a saref
    13   val savalue: 'a saref -> 'a option
    14   val saset: 'a saref * 'a -> unit
    15 end;
    16 
    17 structure SingleAssignment: SINGLE_ASSIGNMENT =
    18 struct
    19 
    20 exception Locked;
    21 
    22 abstype 'a saref = SARef of 'a option ref
    23 with
    24 
    25 fun saref () = SARef (ref NONE);
    26 
    27 fun savalue (SARef r) = ! r;
    28 
    29 fun saset (SARef (r as ref NONE), x) =
    30       (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
    31   | saset _ = raise Locked;
    32 
    33 end;
    34 
    35 end;