# HG changeset patch # User wenzelm # Date 1265490108 -3600 # Node ID a725ff6ead264a8a5d15c5f35eccc10b3f37551e # Parent f3d49165889316df39adfdaec77f5a6e6752665d explicit representation of single-assignment variables; diff -r f3d491658893 -r a725ff6ead26 src/Pure/Concurrent/single_assignment.ML --- /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; + diff -r f3d491658893 -r a725ff6ead26 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; + diff -r f3d491658893 -r a725ff6ead26 src/Pure/IsaMakefile --- 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 \ diff -r f3d491658893 -r a725ff6ead26 src/Pure/ML-Systems/polyml_common.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; - diff -r f3d491658893 -r a725ff6ead26 src/Pure/ML-Systems/single_assignment.ML --- /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; diff -r f3d491658893 -r a725ff6ead26 src/Pure/ML-Systems/single_assignment_polyml.ML --- /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; diff -r f3d491658893 -r a725ff6ead26 src/Pure/ML-Systems/smlnj.ML --- 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*) diff -r f3d491658893 -r a725ff6ead26 src/Pure/ROOT.ML --- 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";