wenzelm@53164: (*  Title:      Tools/Spec_Check/random.ML
bulwahn@52248:     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
bulwahn@52248:     Author:     Christopher League
bulwahn@52248: 
bulwahn@52248: Random number engine.
bulwahn@52248: *)
bulwahn@52248: 
bulwahn@52248: signature RANDOM =
bulwahn@52248: sig
bulwahn@52248:   type rand
bulwahn@52248:   val new : unit -> rand
bulwahn@52248:   val range : int * int -> rand -> int * rand
bulwahn@52248:   val split : rand -> rand * rand
bulwahn@52248: end
bulwahn@52248: 
bulwahn@52248: structure Random : RANDOM  =
bulwahn@52248: struct
bulwahn@52248: 
bulwahn@52248: type rand = real
bulwahn@52248: 
bulwahn@52248: val a = 16807.0
bulwahn@52248: val m = 2147483647.0
bulwahn@52248: 
bulwahn@52248: fun nextrand seed =
bulwahn@52248:   let
bulwahn@52248:     val t = a * seed
bulwahn@52248:   in
bulwahn@52248:     t - m * real(floor(t/m))
bulwahn@52248:   end
bulwahn@52248: 
bulwahn@52248: val new = nextrand o Time.toReal o Time.now
bulwahn@52248: 
bulwahn@52248: fun range (min, max) =
bulwahn@52248:   if min > max then raise Domain (* TODO: raise its own error *)
bulwahn@52248:   else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
bulwahn@52248: 
bulwahn@52248: fun split r =
bulwahn@52248:   let
bulwahn@52248:     val r = r / a
bulwahn@52248:     val r0 = real(floor r)
bulwahn@52248:     val r1 = r - r0
bulwahn@52248:   in
bulwahn@52248:     (nextrand r0, nextrand r1)
bulwahn@52248:   end
bulwahn@52248: 
bulwahn@52248: end