src/Pure/Concurrent/single_assignment_sequential.ML
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 35014 a725ff6ead26
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
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