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