clarified files;
authorwenzelm
Thu Mar 10 09:56:29 2016 +0100 (2016-03-10)
changeset 625855d4ed917450d
parent 62584 6cd36a0d2a28
child 62586 a522a5692832
clarified files;
src/Pure/Concurrent/random.ML
src/Pure/General/random.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Concurrent/random.ML	Thu Mar 10 09:50:53 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,38 +0,0 @@
     1.4 -(*  Title:      Pure/Concurrent/random.ML
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -
     1.7 -Pseudo random numbers.
     1.8 -*)
     1.9 -
    1.10 -signature RANDOM =
    1.11 -sig
    1.12 -  val random: unit -> real
    1.13 -  exception RANDOM
    1.14 -  val random_range: int -> int -> int
    1.15 -end;
    1.16 -
    1.17 -structure Random: RANDOM =
    1.18 -struct
    1.19 -
    1.20 -fun rmod x y = x - y * Real.realFloor (x / y);
    1.21 -
    1.22 -local
    1.23 -  val a = 16807.0;
    1.24 -  val m = 2147483647.0;
    1.25 -  val random_seed = Synchronized.var "random_seed" 1.0;
    1.26 -in
    1.27 -
    1.28 -fun random () =
    1.29 -  Synchronized.change_result random_seed
    1.30 -    (fn r => let val r' = rmod (a * r) m in (r', r') end);
    1.31 -
    1.32 -end;
    1.33 -
    1.34 -exception RANDOM;
    1.35 -
    1.36 -fun random_range l h =
    1.37 -  if h < l orelse l < 0 then raise RANDOM
    1.38 -  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    1.39 -
    1.40 -end;
    1.41 -
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/random.ML	Thu Mar 10 09:56:29 2016 +0100
     2.3 @@ -0,0 +1,38 @@
     2.4 +(*  Title:      Pure/General/random.ML
     2.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.6 +
     2.7 +Pseudo random numbers.
     2.8 +*)
     2.9 +
    2.10 +signature RANDOM =
    2.11 +sig
    2.12 +  val random: unit -> real
    2.13 +  exception RANDOM
    2.14 +  val random_range: int -> int -> int
    2.15 +end;
    2.16 +
    2.17 +structure Random: RANDOM =
    2.18 +struct
    2.19 +
    2.20 +fun rmod x y = x - y * Real.realFloor (x / y);
    2.21 +
    2.22 +local
    2.23 +  val a = 16807.0;
    2.24 +  val m = 2147483647.0;
    2.25 +  val random_seed = Synchronized.var "random_seed" 1.0;
    2.26 +in
    2.27 +
    2.28 +fun random () =
    2.29 +  Synchronized.change_result random_seed
    2.30 +    (fn r => let val r' = rmod (a * r) m in (r', r') end);
    2.31 +
    2.32 +end;
    2.33 +
    2.34 +exception RANDOM;
    2.35 +
    2.36 +fun random_range l h =
    2.37 +  if h < l orelse l < 0 then raise RANDOM
    2.38 +  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    2.39 +
    2.40 +end;
    2.41 +
     3.1 --- a/src/Pure/ROOT	Thu Mar 10 09:50:53 2016 +0100
     3.2 +++ b/src/Pure/ROOT	Thu Mar 10 09:56:29 2016 +0100
     3.3 @@ -12,7 +12,6 @@
     3.4      "Concurrent/multithreading.ML"
     3.5      "Concurrent/par_exn.ML"
     3.6      "Concurrent/par_list.ML"
     3.7 -    "Concurrent/random.ML"
     3.8      "Concurrent/single_assignment.ML"
     3.9      "Concurrent/standard_thread.ML"
    3.10      "Concurrent/synchronized.ML"
    3.11 @@ -45,6 +44,7 @@
    3.12      "General/print_mode.ML"
    3.13      "General/properties.ML"
    3.14      "General/queue.ML"
    3.15 +    "General/random.ML"
    3.16      "General/same.ML"
    3.17      "General/scan.ML"
    3.18      "General/secure.ML"
     4.1 --- a/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Thu Mar 10 09:56:29 2016 +0100
     4.3 @@ -107,8 +107,8 @@
     4.4  
     4.5  use "Concurrent/synchronized.ML";
     4.6  use "Concurrent/counter.ML";
     4.7 -use "Concurrent/random.ML";
     4.8  
     4.9 +use "General/random.ML";
    4.10  use "General/properties.ML";
    4.11  use "General/output.ML";
    4.12  use "PIDE/markup.ML";