separate module Random;
authorwenzelm
Mon Dec 22 14:33:53 2014 +0100 (2014-12-22)
changeset 59172d1c500e0a722
parent 59171 75ec7271b426
child 59173 cdcbda56b05b
separate module Random;
proper Synchronized.var;
src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/Pure/Concurrent/random.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Sun Dec 21 22:49:40 2014 +0100
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Dec 22 14:33:53 2014 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val save_result : (string * term) -> unit
     1.5    val set_compiled_rewriter : (term -> term) -> unit
     1.6    val list_nth : 'a list * int -> 'a
     1.7 -  val dump_output : (string option) Unsynchronized.ref 
     1.8 +  val dump_output : string option Unsynchronized.ref 
     1.9  end
    1.10  
    1.11  structure AM_SML : AM_SML = struct
    1.12 @@ -490,7 +490,7 @@
    1.13  fun compile rules = 
    1.14      let
    1.15          val guid = get_guid ()
    1.16 -        val code = Real.toString (random ())
    1.17 +        val code = Real.toString (Random.random ())
    1.18          val name = "AMSML_"^guid
    1.19          val (inlinetab, source) = sml_prog name code rules
    1.20          val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 21 22:49:40 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 22 14:33:53 2014 +0100
     2.3 @@ -1434,7 +1434,7 @@
     2.4                val max_isar = 1000 * max_dependencies
     2.5  
     2.6                fun priority_of th =
     2.7 -                random_range 0 max_isar +
     2.8 +                Random.random_range 0 max_isar +
     2.9                  (case try (Graph.get_node access_G) (nickname_of_thm th) of
    2.10                    SOME (Isar_Proof, _, deps) => ~100 * length deps
    2.11                  | SOME (Automatic_Proof, _, _) => 2 * max_isar
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Dec 21 22:49:40 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Dec 22 14:33:53 2014 +0100
     3.3 @@ -351,10 +351,9 @@
     3.4        with_cleanup clean_up run () |> tap export
     3.5  
     3.6      val important_message =
     3.7 -      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
     3.8 -        extract_important_message output
     3.9 -      else
    3.10 -        ""
    3.11 +      if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
    3.12 +      then extract_important_message output
    3.13 +      else ""
    3.14  
    3.15      val (used_facts, preferred_methss, message) =
    3.16        (case outcome of
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Concurrent/random.ML	Mon Dec 22 14:33:53 2014 +0100
     4.3 @@ -0,0 +1,38 @@
     4.4 +(*  Title:      Pure/Confurrent/random.ML
     4.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.6 +
     4.7 +Pseudo random numbers.
     4.8 +*)
     4.9 +
    4.10 +signature RANDOM =
    4.11 +sig
    4.12 +  val random: unit -> real
    4.13 +  exception RANDOM
    4.14 +  val random_range: int -> int -> int
    4.15 +end;
    4.16 +
    4.17 +structure Random: RANDOM =
    4.18 +struct
    4.19 +
    4.20 +fun rmod x y = x - y * Real.realFloor (x / y);
    4.21 +
    4.22 +local
    4.23 +  val a = 16807.0;
    4.24 +  val m = 2147483647.0;
    4.25 +  val random_seed = Synchronized.var "random_seed" 1.0;
    4.26 +in
    4.27 +
    4.28 +fun random () =
    4.29 +  Synchronized.change_result random_seed
    4.30 +    (fn r => let val r' = rmod (a * r) m in (r', r') end);
    4.31 +
    4.32 +end;
    4.33 +
    4.34 +exception RANDOM;
    4.35 +
    4.36 +fun random_range l h =
    4.37 +  if h < l orelse l < 0 then raise RANDOM
    4.38 +  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    4.39 +
    4.40 +end;
    4.41 +
     5.1 --- a/src/Pure/ROOT	Sun Dec 21 22:49:40 2014 +0100
     5.2 +++ b/src/Pure/ROOT	Mon Dec 22 14:33:53 2014 +0100
     5.3 @@ -62,6 +62,7 @@
     5.4      "Concurrent/par_exn.ML"
     5.5      "Concurrent/par_list.ML"
     5.6      "Concurrent/par_list_sequential.ML"
     5.7 +    "Concurrent/random.ML"
     5.8      "Concurrent/simple_thread.ML"
     5.9      "Concurrent/single_assignment.ML"
    5.10      "Concurrent/single_assignment_sequential.ML"
     6.1 --- a/src/Pure/ROOT.ML	Sun Dec 21 22:49:40 2014 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Mon Dec 22 14:33:53 2014 +0100
     6.3 @@ -22,6 +22,7 @@
     6.4  if Multithreading.available then ()
     6.5  else use "Concurrent/synchronized_sequential.ML";
     6.6  use "Concurrent/counter.ML";
     6.7 +use "Concurrent/random.ML";
     6.8  
     6.9  use "General/properties.ML";
    6.10  use "General/output.ML";
     7.1 --- a/src/Pure/library.ML	Sun Dec 21 22:49:40 2014 +0100
     7.2 +++ b/src/Pure/library.ML	Mon Dec 22 14:33:53 2014 +0100
     7.3 @@ -199,11 +199,6 @@
     7.4    val untag_list: (int * 'a) list -> 'a list
     7.5    val order_list: (int * 'a) list -> 'a list
     7.6  
     7.7 -  (*random numbers*)
     7.8 -  exception RANDOM
     7.9 -  val random: unit -> real
    7.10 -  val random_range: int -> int -> int
    7.11 -
    7.12    (*misc*)
    7.13    val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
    7.14    val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) ->
    7.15 @@ -985,30 +980,6 @@
    7.16  
    7.17  
    7.18  
    7.19 -(** random numbers **)
    7.20 -
    7.21 -exception RANDOM;
    7.22 -
    7.23 -fun rmod x y = x - y * Real.realFloor (x / y);
    7.24 -
    7.25 -local
    7.26 -  val a = 16807.0;
    7.27 -  val m = 2147483647.0;
    7.28 -  val random_seed = Unsynchronized.ref 1.0;
    7.29 -in
    7.30 -
    7.31 -fun random () = CRITICAL (fn () =>
    7.32 -  let val r = rmod (a * ! random_seed) m
    7.33 -  in (random_seed := r; r) end);
    7.34 -
    7.35 -end;
    7.36 -
    7.37 -fun random_range l h =
    7.38 -  if h < l orelse l < 0 then raise RANDOM
    7.39 -  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    7.40 -
    7.41 -
    7.42 -
    7.43  (** misc **)
    7.44  
    7.45  fun divide_and_conquer decomp x =