# HG changeset patch
# User wenzelm
# Date 1256217584 -7200
# Node ID e66b41782cb59e9e12028c7f0e8baa856eb67992
# Parent  d1c9bf0f8ae8e22768dcd7f53b00c960c72d7b4f
support single-assigment variables -- based on magic RTS operations by David Matthews;

diff -r d1c9bf0f8ae8 -r e66b41782cb5 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 09:50:29 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Oct 22 15:19:44 2009 +0200
@@ -11,8 +11,10 @@
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
+  val readonly_access: 'a var -> ('a -> 'b option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
+  val assign: 'a var -> ('a -> 'a) -> unit
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -37,29 +39,48 @@
 
 (* synchronized access *)
 
-fun timed_access (Var {name, lock, cond, var}) time_limit f =
+fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f =
   SimpleThread.synchronized name lock (fn () =>
     let
       fun try_change () =
         let val x = ! var in
           (case f x of
-            SOME (y, x') => (var := x'; SOME y)
-          | NONE =>
+            NONE =>
               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
                 Exn.Result true => try_change ()
               | Exn.Result false => NONE
-              | Exn.Exn exn => reraise exn))
+              | Exn.Exn exn => reraise exn)
+          | SOME (y, x') =>
+              if readonly then SOME y
+              else
+                let
+                  val _ = magic_immutability_test var
+                    andalso raise Fail ("Attempt to change finished variable " ^ quote name);
+                  val _ = var := x';
+                  val _ = if finish then magic_immutability_mark var else ();
+                in SOME y end)
         end;
       val res = try_change ();
       val _ = ConditionVar.broadcast cond;
     in res end);
 
+fun timed_access var time_limit f =
+  access {time_limit = time_limit, readonly = false, finish = false} var f;
+
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
+fun readonly_access var f =
+  the (access {time_limit = K NONE, readonly = true, finish = false} var
+    (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))));
+
 
 (* unconditional change *)
 
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
+fun assign var f =
+  the (access {time_limit = K NONE, readonly = false, finish = true} var
+    (fn x => SOME ((), f x)));
+
 end;
diff -r d1c9bf0f8ae8 -r e66b41782cb5 src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 22 09:50:29 2009 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 22 15:19:44 2009 +0200
@@ -20,8 +20,13 @@
 
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
+fun readonly_access var f =
+  guarded_access var (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x)));
+
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
+val assign = change;
+
 end;
 end;
diff -r d1c9bf0f8ae8 -r e66b41782cb5 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 22 09:50:29 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 22 15:19:44 2009 +0200
@@ -128,3 +128,12 @@
         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
       in Exn.release res end;
 
+
+(* magic immutability -- for internal use only! *)
+
+fun magic_immutability_mark (r: 'a Unsynchronized.ref) =
+  ignore (RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r);
+
+fun magic_immutability_test (r: 'a Unsynchronized.ref) =
+  Word8.andb (0wx40, RunCall.run_call1 RuntimeCalls.POLY_SYS_get_flags r) = 0w0;
+
diff -r d1c9bf0f8ae8 -r e66b41782cb5 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Oct 22 09:50:29 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Oct 22 15:19:44 2009 +0200
@@ -66,6 +66,10 @@
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
 
 (*dummy implementation*)
+fun magic_immutability_test _ = false;
+fun magic_immutability_mark _ = ();
+
+(*dummy implementation*)
 fun profile (n: int) f x = f x;
 
 (*dummy implementation*)
@@ -177,8 +181,6 @@
 
 val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
 
-
-(*Convert a process ID to a decimal string (chiefly for tracing)*)
 fun process_id pid =
   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));