src/Pure/General/random.ML
author wenzelm
Wed, 07 Aug 2024 12:50:22 +0200
changeset 80657 c6dca9d3af4e
parent 62585 5d4ed917450d
permissions -rw-r--r--
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);

(*  Title:      Pure/General/random.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Pseudo random numbers.
*)

signature RANDOM =
sig
  val random: unit -> real
  exception RANDOM
  val random_range: int -> int -> int
end;

structure Random: RANDOM =
struct

fun rmod x y = x - y * Real.realFloor (x / y);

local
  val a = 16807.0;
  val m = 2147483647.0;
  val random_seed = Synchronized.var "random_seed" 1.0;
in

fun random () =
  Synchronized.change_result random_seed
    (fn r => let val r' = rmod (a * r) m in (r', r') end);

end;

exception RANDOM;

fun random_range l h =
  if h < l orelse l < 0 then raise RANDOM
  else l + Real.floor (rmod (random ()) (real (h - l + 1)));

end;