src/Tools/Spec_Check/random.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 53164 beb4ee344c22
permissions -rw-r--r--
more strict AFP properties;
wenzelm@53164
     1
(*  Title:      Tools/Spec_Check/random.ML
bulwahn@52248
     2
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
bulwahn@52248
     3
    Author:     Christopher League
bulwahn@52248
     4
bulwahn@52248
     5
Random number engine.
bulwahn@52248
     6
*)
bulwahn@52248
     7
bulwahn@52248
     8
signature RANDOM =
bulwahn@52248
     9
sig
bulwahn@52248
    10
  type rand
bulwahn@52248
    11
  val new : unit -> rand
bulwahn@52248
    12
  val range : int * int -> rand -> int * rand
bulwahn@52248
    13
  val split : rand -> rand * rand
bulwahn@52248
    14
end
bulwahn@52248
    15
bulwahn@52248
    16
structure Random : RANDOM  =
bulwahn@52248
    17
struct
bulwahn@52248
    18
bulwahn@52248
    19
type rand = real
bulwahn@52248
    20
bulwahn@52248
    21
val a = 16807.0
bulwahn@52248
    22
val m = 2147483647.0
bulwahn@52248
    23
bulwahn@52248
    24
fun nextrand seed =
bulwahn@52248
    25
  let
bulwahn@52248
    26
    val t = a * seed
bulwahn@52248
    27
  in
bulwahn@52248
    28
    t - m * real(floor(t/m))
bulwahn@52248
    29
  end
bulwahn@52248
    30
bulwahn@52248
    31
val new = nextrand o Time.toReal o Time.now
bulwahn@52248
    32
bulwahn@52248
    33
fun range (min, max) =
bulwahn@52248
    34
  if min > max then raise Domain (* TODO: raise its own error *)
bulwahn@52248
    35
  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
bulwahn@52248
    36
bulwahn@52248
    37
fun split r =
bulwahn@52248
    38
  let
bulwahn@52248
    39
    val r = r / a
bulwahn@52248
    40
    val r0 = real(floor r)
bulwahn@52248
    41
    val r1 = r - r0
bulwahn@52248
    42
  in
bulwahn@52248
    43
    (nextrand r0, nextrand r1)
bulwahn@52248
    44
  end
bulwahn@52248
    45
bulwahn@52248
    46
end