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