--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/single_assignment.ML Sat Feb 06 22:01:48 2010 +0100
@@ -0,0 +1,57 @@
+(* Title: Pure/Concurrent/single_assignment.ML
+ Author: Makarius
+
+Single-assignment variables with locking/signalling.
+*)
+
+signature SINGLE_ASSIGNMENT =
+sig
+ type 'a var
+ val var: string -> 'a var
+ val peek: 'a var -> 'a option
+ val await: 'a var -> 'a
+ val assign: 'a var -> 'a -> unit
+end;
+
+structure Single_Assignment: SINGLE_ASSIGNMENT =
+struct
+
+abstype 'a var = Var of
+ {name: string,
+ lock: Mutex.mutex,
+ cond: ConditionVar.conditionVar,
+ var: 'a SingleAssignment.saref}
+with
+
+fun var name = Var
+ {name = name,
+ lock = Mutex.mutex (),
+ cond = ConditionVar.conditionVar (),
+ var = SingleAssignment.saref ()};
+
+fun peek (Var {var, ...}) = SingleAssignment.savalue var;
+
+fun await (v as Var {name, lock, cond, var}) =
+ SimpleThread.synchronized name lock (fn () =>
+ let
+ fun wait () =
+ (case peek v of
+ NONE =>
+ (case Multithreading.sync_wait NONE NONE cond lock of
+ Exn.Result _ => wait ()
+ | Exn.Exn exn => reraise exn)
+ | SOME x => x);
+ in wait () end);
+
+fun assign (v as Var {name, lock, cond, var}) x =
+ SimpleThread.synchronized name lock (fn () =>
+ (case peek v of
+ SOME _ => raise Fail ("Duplicate assignment to variable " ^ quote name)
+ | NONE =>
+ uninterruptible (fn _ => fn () =>
+ (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
+
+end;
+
+end;
+
--- /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;
+
--- a/src/Pure/IsaMakefile Sat Feb 06 20:57:07 2010 +0100
+++ b/src/Pure/IsaMakefile Sat Feb 06 22:01:48 2010 +0100
@@ -29,7 +29,9 @@
ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
ML-Systems/polyml-5.2.ML ML-Systems/polyml-5.2.1.ML \
ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML \
+ ML-Systems/single_assignment.ML \
+ ML-Systems/single_assignment_polyml.ML ML-Systems/smlnj.ML \
ML-Systems/thread_dummy.ML ML-Systems/timing.ML \
ML-Systems/time_limit.ML ML-Systems/universal.ML \
ML-Systems/unsynchronized.ML
@@ -46,17 +48,18 @@
Concurrent/future.ML Concurrent/lazy.ML \
Concurrent/lazy_sequential.ML Concurrent/mailbox.ML \
Concurrent/par_list.ML Concurrent/par_list_sequential.ML \
- Concurrent/simple_thread.ML Concurrent/synchronized.ML \
- Concurrent/synchronized_sequential.ML Concurrent/task_queue.ML \
- General/alist.ML General/antiquote.ML General/balanced_tree.ML \
- General/basics.ML General/binding.ML General/buffer.ML \
- General/exn.ML General/file.ML General/graph.ML General/heap.ML \
- General/integer.ML General/long_name.ML General/markup.ML \
- General/name_space.ML General/ord_list.ML General/output.ML \
- General/path.ML General/position.ML General/pretty.ML \
- General/print_mode.ML General/properties.ML General/queue.ML \
- General/same.ML General/scan.ML General/secure.ML General/seq.ML \
- General/source.ML General/stack.ML General/symbol.ML \
+ Concurrent/simple_thread.ML Concurrent/single_assignment.ML \
+ Concurrent/single_assignment_sequential.ML \
+ Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \
+ Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \
+ General/balanced_tree.ML General/basics.ML General/binding.ML \
+ General/buffer.ML General/exn.ML General/file.ML General/graph.ML \
+ General/heap.ML General/integer.ML General/long_name.ML \
+ General/markup.ML General/name_space.ML General/ord_list.ML \
+ General/output.ML General/path.ML General/position.ML \
+ General/pretty.ML General/print_mode.ML General/properties.ML \
+ General/queue.ML General/same.ML General/scan.ML General/secure.ML \
+ General/seq.ML General/source.ML General/stack.ML General/symbol.ML \
General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Feb 06 20:57:07 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Feb 06 22:01:48 2010 +0100
@@ -6,6 +6,7 @@
exception Interrupt = SML90.Interrupt;
use "General/exn.ML";
+use "ML-Systems/single_assignment_polyml.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/timing.ML";
@@ -131,12 +132,3 @@
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;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/single_assignment.ML Sat Feb 06 22:01:48 2010 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/ML-Systems/single_assignment.ML
+ Author: Makarius
+
+References with single assignment. Unsynchronized!
+*)
+
+signature SINGLE_ASSIGNMENT =
+sig
+ type 'a saref
+ exception Locked
+ val saref: unit -> 'a saref
+ val savalue: 'a saref -> 'a option
+ val saset: 'a saref * 'a -> unit
+end;
+
+structure SingleAssignment: SINGLE_ASSIGNMENT =
+struct
+
+exception Locked;
+
+abstype 'a saref = SARef of 'a option ref
+with
+
+fun saref () = SARef (ref NONE);
+
+fun savalue (SARef r) = ! r;
+
+fun saset (SARef (r as ref NONE), x) = r := SOME x
+ | saset _ = raise Locked;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/single_assignment_polyml.ML Sat Feb 06 22:01:48 2010 +0100
@@ -0,0 +1,35 @@
+(* Title: Pure/ML-Systems/single_assignment_polyml.ML
+ Author: Makarius
+
+References with single assignment. Unsynchronized! Emulates
+structure SingleAssignment from Poly/ML 5.4.
+*)
+
+signature SINGLE_ASSIGNMENT =
+sig
+ type 'a saref
+ exception Locked
+ val saref: unit -> 'a saref
+ val savalue: 'a saref -> 'a option
+ val saset: 'a saref * 'a -> unit
+end;
+
+structure SingleAssignment: SINGLE_ASSIGNMENT =
+struct
+
+exception Locked;
+
+abstype 'a saref = SARef of 'a option ref
+with
+
+fun saref () = SARef (ref NONE);
+
+fun savalue (SARef r) = ! r;
+
+fun saset (SARef (r as ref NONE), x) =
+ (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
+ | saset _ = raise Locked;
+
+end;
+
+end;
--- a/src/Pure/ML-Systems/smlnj.ML Sat Feb 06 20:57:07 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Feb 06 22:01:48 2010 +0100
@@ -10,6 +10,7 @@
use "ML-Systems/unsynchronized.ML";
use "ML-Systems/overloading_smlnj.ML";
use "General/exn.ML";
+use "ML-Systems/single_assignment.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
@@ -66,10 +67,6 @@
(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*)
--- a/src/Pure/ROOT.ML Sat Feb 06 20:57:07 2010 +0100
+++ b/src/Pure/ROOT.ML Sat Feb 06 22:01:48 2010 +0100
@@ -57,6 +57,10 @@
use "Concurrent/simple_thread.ML";
+use "Concurrent/single_assignment.ML";
+if Multithreading.available then ()
+else use "Concurrent/single_assignment_sequential.ML";
+
use "Concurrent/synchronized.ML";
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";