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