# HG changeset patch
# User wenzelm
# Date 1530737064 -7200
# Node ID 9258f16d68b411c7acd03681c7c0827d9eaef2a3
# Parent  1df516bffaa30094b51b1a2cc5bb8b74e1b1a8e9
more frugal single-assignment according to David Matthews: dispose mutable lock/cond eventually;

diff -r 1df516bffaa3 -r 9258f16d68b4 src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Wed Jul 04 14:26:27 2018 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Wed Jul 04 22:44:24 2018 +0200
@@ -16,40 +16,46 @@
 structure Single_Assignment: SINGLE_ASSIGNMENT =
 struct
 
-abstype 'a var = Var of
- {name: string,
-  lock: Mutex.mutex,
-  cond: ConditionVar.conditionVar,
-  var: 'a SingleAssignment.saref}
+datatype 'a state =
+    Set of 'a
+  | Unset of {lock: Mutex.mutex, cond: ConditionVar.conditionVar};
+
+fun init_state () =
+  Unset {lock = Mutex.mutex (), cond = ConditionVar.conditionVar ()};
+
+abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
 with
 
-fun var name = Var
- {name = name,
-  lock = Mutex.mutex (),
-  cond = ConditionVar.conditionVar (),
-  var = SingleAssignment.saref ()};
+fun var name = Var {name = name, state = Unsynchronized.ref (init_state ())};
+
+fun peek (Var {state, ...}) = (case ! state of Set x => SOME x | Unset _ => NONE);
 
-fun peek (Var {var, ...}) = SingleAssignment.savalue var;
+fun await (v as Var {name, state}) =
+  (case ! state of
+    Set x => x
+  | Unset {lock, cond} =>
+      Multithreading.synchronized name lock (fn () =>
+        let
+          fun wait () =
+            (case peek v of
+              NONE =>
+                (case Multithreading.sync_wait NONE cond lock of
+                  Exn.Res _ => wait ()
+                | Exn.Exn exn => Exn.reraise exn)
+            | SOME x => x);
+        in wait () end));
 
-fun await (v as Var {name, lock, cond, ...}) =
-  Multithreading.synchronized name lock (fn () =>
-    let
-      fun wait () =
+fun assign_fail name = raise Fail ("Duplicate assignment to " ^ name);
+fun assign (v as Var {name, state}) x =
+  (case ! state of
+    Set _ => assign_fail name
+  | Unset {lock, cond} =>
+      Multithreading.synchronized name lock (fn () =>
         (case peek v of
-          NONE =>
-            (case Multithreading.sync_wait NONE cond lock of
-              Exn.Res _ => wait ()
-            | Exn.Exn exn => Exn.reraise exn)
-        | SOME x => x);
-    in wait () end);
-
-fun assign (v as Var {name, lock, cond, var}) x =
-  Multithreading.synchronized name lock (fn () =>
-    (case peek v of
-      SOME _ => raise Fail ("Duplicate assignment to " ^ name)
-    | NONE =>
-        Thread_Attributes.uninterruptible (fn _ => fn () =>
-         (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
+          SOME _ => assign_fail name
+        | NONE =>
+            Thread_Attributes.uninterruptible (fn _ => fn () =>
+             (state := Set x; RunCall.clearMutableBit state; ConditionVar.broadcast cond)) ())));
 
 end;