src/Pure/ML-Systems/single_assignment_polyml.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 35014 a725ff6ead26
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm@35014
     1
(*  Title:      Pure/ML-Systems/single_assignment_polyml.ML
wenzelm@35014
     2
    Author:     Makarius
wenzelm@35014
     3
wenzelm@35014
     4
References with single assignment.  Unsynchronized!  Emulates
wenzelm@35014
     5
structure SingleAssignment from Poly/ML 5.4.
wenzelm@35014
     6
*)
wenzelm@35014
     7
wenzelm@35014
     8
signature SINGLE_ASSIGNMENT =
wenzelm@35014
     9
sig
wenzelm@35014
    10
  type 'a saref
wenzelm@35014
    11
  exception Locked
wenzelm@35014
    12
  val saref: unit -> 'a saref
wenzelm@35014
    13
  val savalue: 'a saref -> 'a option
wenzelm@35014
    14
  val saset: 'a saref * 'a -> unit
wenzelm@35014
    15
end;
wenzelm@35014
    16
wenzelm@35014
    17
structure SingleAssignment: SINGLE_ASSIGNMENT =
wenzelm@35014
    18
struct
wenzelm@35014
    19
wenzelm@35014
    20
exception Locked;
wenzelm@35014
    21
wenzelm@35014
    22
abstype 'a saref = SARef of 'a option ref
wenzelm@35014
    23
with
wenzelm@35014
    24
wenzelm@35014
    25
fun saref () = SARef (ref NONE);
wenzelm@35014
    26
wenzelm@35014
    27
fun savalue (SARef r) = ! r;
wenzelm@35014
    28
wenzelm@35014
    29
fun saset (SARef (r as ref NONE), x) =
wenzelm@35014
    30
      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
wenzelm@35014
    31
  | saset _ = raise Locked;
wenzelm@35014
    32
wenzelm@35014
    33
end;
wenzelm@35014
    34
wenzelm@35014
    35
end;