src/Pure/ML-Systems/single_assignment.ML
author wenzelm
Sat, 06 Feb 2010 22:01:48 +0100
changeset 35014 a725ff6ead26
permissions -rw-r--r--
explicit representation of single-assignment variables;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/single_assignment.ML
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     3
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     4
References with single assignment.  Unsynchronized!
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     5
*)
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     6
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     7
signature SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     8
sig
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     9
  type 'a saref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    10
  exception Locked
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    11
  val saref: unit -> 'a saref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    12
  val savalue: 'a saref -> 'a option
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    13
  val saset: 'a saref * 'a -> unit
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    14
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    15
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    16
structure SingleAssignment: SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    17
struct
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    18
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    19
exception Locked;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    20
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    21
abstype 'a saref = SARef of 'a option ref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    22
with
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    23
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    24
fun saref () = SARef (ref NONE);
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    25
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    26
fun savalue (SARef r) = ! r;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    27
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    28
fun saset (SARef (r as ref NONE), x) = r := SOME x
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    29
  | saset _ = raise Locked;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    30
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    31
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    32
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    33
end;