# HG changeset patch # User wenzelm # Date 1394812441 -3600 # Node ID 9589605bcf41811ec0c8aa085fccc25591223ce7 # Parent 8453d35e4684650e1347c27821f0c6f146455f01 prefer more robust Synchronized.var; diff -r 8453d35e4684 -r 9589605bcf41 src/HOL/Library/refute.ML --- 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 diff -r 8453d35e4684 -r 9589605bcf41 src/HOL/Mutabelle/MutabelleExtra.thy --- 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)) diff -r 8453d35e4684 -r 9589605bcf41 src/HOL/Mutabelle/mutabelle_extra.ML --- 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; diff -r 8453d35e4684 -r 9589605bcf41 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 diff -r 8453d35e4684 -r 9589605bcf41 src/HOL/Tools/sat_solver.ML --- 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) diff -r 8453d35e4684 -r 9589605bcf41 src/Pure/Isar/toplevel.ML --- 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; diff -r 8453d35e4684 -r 9589605bcf41 src/Tools/misc_legacy.ML --- 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;