src/Pure/Concurrent/single_assignment_sequential.ML
author wenzelm
Sun, 22 Jul 2012 12:26:41 +0200
changeset 48423 0ccf143a2a69
parent 35014 a725ff6ead26
permissions -rw-r--r--
maintain set of source digests, including relevant parts of session entry;
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/Concurrent/single_assignment_sequential.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
Single-assignment variables (sequential version).
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
structure Single_Assignment: SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     8
struct
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     9
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    10
abstype 'a var = Var of 'a SingleAssignment.saref
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    11
with
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    12
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    13
fun var _ = Var (SingleAssignment.saref ());
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    14
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    15
fun peek (Var var) = SingleAssignment.savalue var;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    16
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    17
fun await v =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    18
  (case peek v of
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    19
    SOME x => x
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    20
  | NONE => Thread.unavailable ());
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    21
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    22
fun assign (v as Var var) x =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    23
  (case peek v of
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    24
    SOME _ => raise Fail "Duplicate assignment to variable"
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    25
  | NONE => SingleAssignment.saset (var, x));
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    26
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    27
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    28
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    29
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    30