--- a/src/HOL/Library/refute.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/HOL/Library/refute.ML Fri Mar 14 16:54:01 2014 +0100
@@ -1073,7 +1073,7 @@
handle Option.Option =>
error ("Unknown SAT solver: " ^ quote satsolver ^
". Available solvers: " ^
- commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
+ commas (map (quote o fst) (SatSolver.get_solvers ())) ^ ".")
in
Output.urgent_message "Invoking SAT solver...";
(case solver fm of
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri Mar 14 15:41:29 2014 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri Mar 14 16:54:01 2014 +0100
@@ -37,7 +37,7 @@
ML {*
fun mutation_testing_of (name, thy) =
- (MutabelleExtra.random_seed := 1.0;
+ (MutabelleExtra.init_random 1.0;
MutabelleExtra.thms_of false thy
|> MutabelleExtra.take_random 200
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
@@ -50,7 +50,7 @@
(*
ML {*
- MutabelleExtra.random_seed := 1.0;
+ MutabelleExtra.init_random 1.0;
MutabelleExtra.thms_of true @{theory Complex_Main}
|> MutabelleExtra.take_random 1000000
|> (fn thms => List.drop (thms, 1000))
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 14 16:54:01 2014 +0100
@@ -40,15 +40,12 @@
val mutate_theorems_and_write_report :
theory -> int * int -> mtd list -> thm list -> string -> unit
-val random_seed : real Unsynchronized.ref
+val init_random : real -> unit
end;
structure MutabelleExtra : MUTABELLE_EXTRA =
struct
-(* Own seed; can't rely on the Isabelle one to stay the same *)
-val random_seed = Unsynchronized.ref 1.0;
-
(* Another Random engine *)
exception RANDOM;
@@ -56,13 +53,20 @@
fun rmod x y = x - y * Real.realFloor (x / y);
local
+ (* Own seed; can't rely on the Isabelle one to stay the same *)
+ val random_seed = Synchronized.var "random_seed" 1.0;
+
val a = 16807.0;
val m = 2147483647.0;
in
-fun random () = CRITICAL (fn () =>
- let val r = rmod (a * ! random_seed) m
- in (random_seed := r; r) end);
+fun init_random r = Synchronized.change random_seed (K r);
+
+fun random () =
+ Synchronized.change_result random_seed
+ (fn s =>
+ let val r = rmod (a * s) m
+ in (r, r) end);
end;
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 14 16:54:01 2014 +0100
@@ -573,7 +573,7 @@
let
(* use the first ML solver (to avoid startup overhead) *)
val (ml_solvers, nonml_solvers) =
- !SatSolver.solvers
+ SatSolver.get_solvers ()
|> List.partition (member (op =) ["dptsat", "dpll"] o fst)
val res =
if null nonml_solvers then
--- a/src/HOL/Tools/sat_solver.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/HOL/Tools/sat_solver.ML Fri Mar 14 16:54:01 2014 +0100
@@ -42,7 +42,7 @@
val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
(* generic solver interface *)
- val solvers : (string * solver) list Unsynchronized.ref
+ val get_solvers : unit -> (string * solver) list
val add_solver : string * solver -> unit
val invoke_solver : string -> solver (* exception Option *)
end;
@@ -348,22 +348,24 @@
end;
(* ------------------------------------------------------------------------- *)
-(* solvers: a (reference to a) table of all registered SAT solvers *)
+(* solvers: a table of all registered SAT solvers *)
(* ------------------------------------------------------------------------- *)
- val solvers = Unsynchronized.ref ([] : (string * solver) list);
+ val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
+
+ fun get_solvers () = Synchronized.value solvers;
(* ------------------------------------------------------------------------- *)
(* add_solver: updates 'solvers' by adding a new solver *)
(* ------------------------------------------------------------------------- *)
- fun add_solver (name, new_solver) = CRITICAL (fn () =>
+ fun add_solver (name, new_solver) =
+ Synchronized.change solvers (fn the_solvers =>
let
- val the_solvers = !solvers;
val _ = if AList.defined (op =) the_solvers name
then warning ("SAT solver " ^ quote name ^ " was defined before")
else ();
- in solvers := AList.update (op =) (name, new_solver) the_solvers end);
+ in AList.update (op =) (name, new_solver) the_solvers end);
(* ------------------------------------------------------------------------- *)
(* invoke_solver: returns the solver associated with the given 'name' *)
@@ -372,7 +374,7 @@
(* ------------------------------------------------------------------------- *)
fun invoke_solver name =
- (the o AList.lookup (op =) (!solvers)) name;
+ the (AList.lookup (op =) (get_solvers ()) name);
end; (* SatSolver *)
@@ -521,7 +523,7 @@
handle SatSolver.NOT_CONFIGURED => loop solvers
)
in
- loop (!SatSolver.solvers)
+ loop (SatSolver.get_solvers ())
end
in
SatSolver.add_solver ("auto", auto_solver)
--- a/src/Pure/Isar/toplevel.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Mar 14 16:54:01 2014 +0100
@@ -590,11 +590,12 @@
(* post-transition hooks *)
local
- val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+ val hooks =
+ Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list);
in
-fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = ! hooks;
+fun add_hook hook = Synchronized.change hooks (cons hook);
+fun get_hooks () = Synchronized.value hooks;
end;
--- a/src/Tools/misc_legacy.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/Tools/misc_legacy.ML Fri Mar 14 16:54:01 2014 +0100
@@ -246,10 +246,11 @@
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 = Unsynchronized.ref (0: int);
+val gensym_seed = Synchronized.var "gensym_seed" (0: int);
in
- fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
+ fun gensym pre =
+ Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
end;