src/Tools/random_word.ML
author wenzelm
Sat, 28 Feb 2009 14:09:58 +0100
changeset 30161 c26e515f1c29
parent 25742 1051ef9d87c4
child 32740 9dd0a2f83429
permissions -rw-r--r--
removed Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/random_word.ML
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     3
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     4
Simple generator for pseudo-random numbers, using unboxed word
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     5
arithmetic only.  Unprotected concurrency introduces some true
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     6
randomness.
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     7
*)
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     8
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
     9
signature RANDOM_WORD =
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    10
sig
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    11
  val max_word: word
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    12
  val step: word -> word
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    13
  val next_word: unit -> word
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    14
  val next_bool: unit -> bool
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    15
  val next_int: int -> int -> int
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    16
  val next_real: unit -> real
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    17
  val pick_any: 'a list -> 'a
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    18
  val pick_weighted: (int * 'a) list -> 'a
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    19
end;
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    20
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    21
structure RandomWord: RANDOM_WORD =
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    22
struct
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    23
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    24
(* random words: 0w0 <= result <= max_word *)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    25
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    26
(*minimum length of unboxed words on all supported ML platforms*)
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    27
val _ = Word.wordSize >= 30
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    28
  orelse raise Fail ("Bad platform word size");
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    29
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    30
val max_word = 0wx3FFFFFFF;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    31
val top_bit = 0wx20000000;
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    32
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    33
(*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    34
  see http://random.mat.sbg.ac.at/~charly/server/server.html*)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    35
val a = 0w777138309;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    36
fun step x = Word.andb (a * x + 0w1, max_word);
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    37
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    38
local val rand = ref 0w1
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    39
in fun next_word () = (change rand step; ! rand) end;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    40
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    41
(*NB: higher bits are more random than lower ones*)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    42
fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    43
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    44
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    45
(* random integers: i <= result <= j *)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    46
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    47
val max_int = Word.toInt max_word;
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    48
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    49
fun next_int i j =
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    50
  let val k = j - i in
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    51
    if k < 0 orelse k > max_int then raise Fail ("next_int: out of range")
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    52
    else if k < max_int then i + Word.toInt (Word.mod (next_word (), Word.fromInt (k + 1)))
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    53
    else i + Word.toInt (next_word ())
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    54
  end;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    55
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    56
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    57
(* random reals: 0.0 <= result < 1.0 *)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    58
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    59
val scaling = real max_int + 1.0;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    60
fun next_real () = real (Word.toInt (next_word ())) / scaling;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    61
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    62
25742
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    63
(* random list elements *)
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    64
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    65
fun pick_any [] = raise Empty
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    66
  | pick_any xs = nth xs (next_int 0 (length xs - 1));
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    67
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    68
fun pick_weighted xs =
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    69
  let
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    70
    val total = fold (fn (k, _) => fn i =>
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    71
      if k < 0 then raise Fail ("Bad weight: " ^ string_of_int k) else k + i) xs 0;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    72
    fun pick n ((k, x) :: xs) =
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    73
        if n <= k then x else pick (n - k) xs
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    74
      | pick _ [] = raise Empty;
1051ef9d87c4 added int/real/list operations;
wenzelm
parents: 25728
diff changeset
    75
  in if total = 0 then raise Empty else pick (next_int 1 total) xs end;
25728
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    76
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    77
end;
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff changeset
    78