src/Pure/RAW/single_assignment_polyml.ML
author Manuel Eberl <eberlm@in.tum.de>
Tue, 19 Jan 2016 11:19:25 +0100
changeset 62201 eca7b38c8ee5
parent 61925 ab52f183f020
permissions -rw-r--r--
Added approximation of powr to NEWS/CONTRIBUTORS
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 35014
diff changeset
     1
(*  Title:      Pure/RAW/single_assignment_polyml.ML
35014
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!  Emulates
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     5
structure SingleAssignment from Poly/ML 5.4.
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     6
*)
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     7
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     8
signature SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     9
sig
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    10
  type 'a saref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    11
  exception Locked
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    12
  val saref: unit -> 'a saref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    13
  val savalue: 'a saref -> 'a option
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    14
  val saset: 'a saref * 'a -> unit
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    15
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    16
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    17
structure SingleAssignment: SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    18
struct
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    19
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    20
exception Locked;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    21
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    22
abstype 'a saref = SARef of 'a option ref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    23
with
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    24
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    25
fun saref () = SARef (ref NONE);
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    26
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    27
fun savalue (SARef r) = ! r;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    28
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    29
fun saset (SARef (r as ref NONE), x) =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    30
      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    31
  | saset _ = raise Locked;
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;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    34
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    35
end;