Raw ML references as unsynchronized state variables.
authorwenzelm
Tue Sep 29 11:48:32 2009 +0200 (2009-09-29)
changeset 3273776fa673eee8b
parent 32736 f126e68d003d
child 32738 15bb09ca0378
Raw ML references as unsynchronized state variables.
src/Pure/IsaMakefile
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/unsynchronized.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Sep 28 23:51:13 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Sep 29 11:48:32 2009 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
     1.5    ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
     1.6    ML-Systems/timing.ML ML-Systems/time_limit.ML				\
     1.7 -  ML-Systems/universal.ML
     1.8 +  ML-Systems/universal.ML ML-Systems/unsynchronized.ML
     1.9  
    1.10  RAW: $(OUT)/RAW
    1.11  
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Mon Sep 28 23:51:13 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Tue Sep 29 11:48:32 2009 +0200
     2.3 @@ -41,6 +41,7 @@
     2.4  fun reraise exn = raise exn;
     2.5  
     2.6  use "ML-Systems/exn.ML";
     2.7 +use "ML-Systems/unsynchronized.ML";
     2.8  use "ML-Systems/universal.ML";
     2.9  use "ML-Systems/thread_dummy.ML";
    2.10  use "ML-Systems/multithreading.ML";
     3.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Mon Sep 28 23:51:13 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Sep 29 11:48:32 2009 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  exception Interrupt = SML90.Interrupt;
     3.5  
     3.6  use "ML-Systems/exn.ML";
     3.7 +use "ML-Systems/unsynchronized.ML";
     3.8  use "ML-Systems/multithreading.ML";
     3.9  use "ML-Systems/time_limit.ML";
    3.10  use "ML-Systems/timing.ML";
    3.11 @@ -50,7 +51,7 @@
    3.12  (* print depth *)
    3.13  
    3.14  local
    3.15 -  val depth = ref 10;
    3.16 +  val depth = Unsynchronized.ref 10;
    3.17  in
    3.18    fun get_print_depth () = ! depth;
    3.19    fun print_depth n = (depth := n; PolyML.print_depth n);
     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Sep 28 23:51:13 2009 +0200
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Sep 29 11:48:32 2009 +0200
     4.3 @@ -9,6 +9,7 @@
     4.4  use "ML-Systems/proper_int.ML";
     4.5  use "ML-Systems/overloading_smlnj.ML";
     4.6  use "ML-Systems/exn.ML";
     4.7 +use "ML-Systems/unsynchronized.ML";
     4.8  use "ML-Systems/universal.ML";
     4.9  use "ML-Systems/thread_dummy.ML";
    4.10  use "ML-Systems/multithreading.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML-Systems/unsynchronized.ML	Tue Sep 29 11:48:32 2009 +0200
     5.3 @@ -0,0 +1,25 @@
     5.4 +(*  Title:      Pure/ML-Systems/unsynchronized.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Raw ML references as unsynchronized state variables.
     5.8 +*)
     5.9 +
    5.10 +structure Unsynchronized =
    5.11 +struct
    5.12 +
    5.13 +datatype ref = datatype ref;
    5.14 +
    5.15 +val op := = op :=;
    5.16 +val ! = !;
    5.17 +
    5.18 +fun set flag = (flag := true; true);
    5.19 +fun reset flag = (flag := false; false);
    5.20 +fun toggle flag = (flag := not (! flag); ! flag);
    5.21 +
    5.22 +fun change r f = r := f (! r);
    5.23 +fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
    5.24 +
    5.25 +fun inc i = (i := ! i + (1: int); ! i);
    5.26 +fun dec i = (i := ! i - (1: int); ! i);
    5.27 +
    5.28 +end;
     6.1 --- a/src/Pure/library.ML	Mon Sep 28 23:51:13 2009 +0200
     6.2 +++ b/src/Pure/library.ML	Tue Sep 29 11:48:32 2009 +0200
     6.3 @@ -57,13 +57,8 @@
     6.4    val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
     6.5    val exists: ('a -> bool) -> 'a list -> bool
     6.6    val forall: ('a -> bool) -> 'a list -> bool
     6.7 -  val set: bool ref -> bool
     6.8 -  val reset: bool ref -> bool
     6.9 -  val toggle: bool ref -> bool
    6.10 -  val change: 'a ref -> ('a -> 'a) -> unit
    6.11 -  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
    6.12 -  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    6.13 -  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    6.14 +  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    6.15 +  val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    6.16    val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    6.17  
    6.18    (*lists*)
    6.19 @@ -123,8 +118,6 @@
    6.20    val suffixes: 'a list -> 'a list list
    6.21  
    6.22    (*integers*)
    6.23 -  val inc: int ref -> int
    6.24 -  val dec: int ref -> int
    6.25    val upto: int * int -> int list
    6.26    val downto: int * int -> int list
    6.27    val radixpand: int * int -> int list
    6.28 @@ -326,13 +319,6 @@
    6.29  
    6.30  (* flags *)
    6.31  
    6.32 -fun set flag = (flag := true; true);
    6.33 -fun reset flag = (flag := false; false);
    6.34 -fun toggle flag = (flag := not (! flag); ! flag);
    6.35 -
    6.36 -fun change r f = r := f (! r);
    6.37 -fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
    6.38 -
    6.39  (*temporarily set flag during execution*)
    6.40  fun setmp_noncritical flag value f x =
    6.41    uninterruptible (fn restore_attributes => fn () =>
    6.42 @@ -643,10 +629,6 @@
    6.43  
    6.44  (** integers **)
    6.45  
    6.46 -fun inc i = (i := ! i + (1: int); ! i);
    6.47 -fun dec i = (i := ! i - (1: int); ! i);
    6.48 -
    6.49 -
    6.50  (* lists of integers *)
    6.51  
    6.52  (*make the list [from, from + 1, ..., to]*)
    6.53 @@ -1055,7 +1037,7 @@
    6.54  local
    6.55    val a = 16807.0;
    6.56    val m = 2147483647.0;
    6.57 -  val random_seed = ref 1.0;
    6.58 +  val random_seed = Unsynchronized.ref 1.0;
    6.59  in
    6.60  
    6.61  fun random () = CRITICAL (fn () =>
    6.62 @@ -1121,17 +1103,18 @@
    6.63  val char_vec = Vector.tabulate (62, gensym_char);
    6.64  fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
    6.65  
    6.66 -val gensym_seed = ref (0: int);
    6.67 +val gensym_seed = Unsynchronized.ref (0: int);
    6.68  
    6.69  in
    6.70 -  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
    6.71 +  fun gensym pre =
    6.72 +    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
    6.73  end;
    6.74  
    6.75  
    6.76  (* stamps and serial numbers *)
    6.77  
    6.78 -type stamp = unit ref;
    6.79 -val stamp: unit -> stamp = ref;
    6.80 +type stamp = unit Unsynchronized.ref;
    6.81 +val stamp: unit -> stamp = Unsynchronized.ref;
    6.82  
    6.83  type serial = int;
    6.84  val serial = Multithreading.serial;