src/Pure/Concurrent/single_assignment_sequential.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/single_assignment_sequential.ML	Sat Feb 06 22:01:48 2010 +0100
@@ -0,0 +1,30 @@
+(*  Title:      Pure/Concurrent/single_assignment_sequential.ML
+    Author:     Makarius
+
+Single-assignment variables (sequential version).
+*)
+
+structure Single_Assignment: SINGLE_ASSIGNMENT =
+struct
+
+abstype 'a var = Var of 'a SingleAssignment.saref
+with
+
+fun var _ = Var (SingleAssignment.saref ());
+
+fun peek (Var var) = SingleAssignment.savalue var;
+
+fun await v =
+  (case peek v of
+    SOME x => x
+  | NONE => Thread.unavailable ());
+
+fun assign (v as Var var) x =
+  (case peek v of
+    SOME _ => raise Fail "Duplicate assignment to variable"
+  | NONE => SingleAssignment.saset (var, x));
+
+end;
+
+end;
+