# HG changeset patch # User wenzelm # Date 1254217712 -7200 # Node ID 76fa673eee8b09645e7ba24a584d8e62ea53039a # Parent f126e68d003d74128f3d7394052fea905a7bf42a Raw ML references as unsynchronized state variables. diff -r f126e68d003d -r 76fa673eee8b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Sep 28 23:51:13 2009 +0200 +++ b/src/Pure/IsaMakefile Tue Sep 29 11:48:32 2009 +0200 @@ -32,7 +32,7 @@ ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ ML-Systems/timing.ML ML-Systems/time_limit.ML \ - ML-Systems/universal.ML + ML-Systems/universal.ML ML-Systems/unsynchronized.ML RAW: $(OUT)/RAW diff -r f126e68d003d -r 76fa673eee8b src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Mon Sep 28 23:51:13 2009 +0200 +++ b/src/Pure/ML-Systems/mosml.ML Tue Sep 29 11:48:32 2009 +0200 @@ -41,6 +41,7 @@ fun reraise exn = raise exn; use "ML-Systems/exn.ML"; +use "ML-Systems/unsynchronized.ML"; use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; diff -r f126e68d003d -r 76fa673eee8b src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Mon Sep 28 23:51:13 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 11:48:32 2009 +0200 @@ -6,6 +6,7 @@ exception Interrupt = SML90.Interrupt; use "ML-Systems/exn.ML"; +use "ML-Systems/unsynchronized.ML"; use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; use "ML-Systems/timing.ML"; @@ -50,7 +51,7 @@ (* print depth *) local - val depth = ref 10; + val depth = Unsynchronized.ref 10; in fun get_print_depth () = ! depth; fun print_depth n = (depth := n; PolyML.print_depth n); diff -r f126e68d003d -r 76fa673eee8b src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Mon Sep 28 23:51:13 2009 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Tue Sep 29 11:48:32 2009 +0200 @@ -9,6 +9,7 @@ use "ML-Systems/proper_int.ML"; use "ML-Systems/overloading_smlnj.ML"; use "ML-Systems/exn.ML"; +use "ML-Systems/unsynchronized.ML"; use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; diff -r f126e68d003d -r 76fa673eee8b src/Pure/ML-Systems/unsynchronized.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/unsynchronized.ML Tue Sep 29 11:48:32 2009 +0200 @@ -0,0 +1,25 @@ +(* Title: Pure/ML-Systems/unsynchronized.ML + Author: Makarius + +Raw ML references as unsynchronized state variables. +*) + +structure Unsynchronized = +struct + +datatype ref = datatype ref; + +val op := = op :=; +val ! = !; + +fun set flag = (flag := true; true); +fun reset flag = (flag := false; false); +fun toggle flag = (flag := not (! flag); ! flag); + +fun change r f = r := f (! r); +fun change_result r f = let val (x, y) = f (! r) in r := y; x end; + +fun inc i = (i := ! i + (1: int); ! i); +fun dec i = (i := ! i - (1: int); ! i); + +end; diff -r f126e68d003d -r 76fa673eee8b src/Pure/library.ML --- a/src/Pure/library.ML Mon Sep 28 23:51:13 2009 +0200 +++ b/src/Pure/library.ML Tue Sep 29 11:48:32 2009 +0200 @@ -57,13 +57,8 @@ val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool val exists: ('a -> bool) -> 'a list -> bool val forall: ('a -> bool) -> 'a list -> bool - val set: bool ref -> bool - val reset: bool ref -> bool - val toggle: bool ref -> bool - val change: 'a ref -> ('a -> 'a) -> unit - val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b - val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c - val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c + val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c + val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c (*lists*) @@ -123,8 +118,6 @@ val suffixes: 'a list -> 'a list list (*integers*) - val inc: int ref -> int - val dec: int ref -> int val upto: int * int -> int list val downto: int * int -> int list val radixpand: int * int -> int list @@ -326,13 +319,6 @@ (* flags *) -fun set flag = (flag := true; true); -fun reset flag = (flag := false; false); -fun toggle flag = (flag := not (! flag); ! flag); - -fun change r f = r := f (! r); -fun change_result r f = let val (x, y) = f (! r) in r := y; x end; - (*temporarily set flag during execution*) fun setmp_noncritical flag value f x = uninterruptible (fn restore_attributes => fn () => @@ -643,10 +629,6 @@ (** integers **) -fun inc i = (i := ! i + (1: int); ! i); -fun dec i = (i := ! i - (1: int); ! i); - - (* lists of integers *) (*make the list [from, from + 1, ..., to]*) @@ -1055,7 +1037,7 @@ local val a = 16807.0; val m = 2147483647.0; - val random_seed = ref 1.0; + val random_seed = Unsynchronized.ref 1.0; in fun random () = CRITICAL (fn () => @@ -1121,17 +1103,18 @@ val char_vec = Vector.tabulate (62, gensym_char); fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); -val gensym_seed = ref (0: int); +val gensym_seed = Unsynchronized.ref (0: int); in - fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed)); + fun gensym pre = + pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed)); end; (* stamps and serial numbers *) -type stamp = unit ref; -val stamp: unit -> stamp = ref; +type stamp = unit Unsynchronized.ref; +val stamp: unit -> stamp = Unsynchronized.ref; type serial = int; val serial = Multithreading.serial;