@[class]
Instances
Equations
- std_next {s1 := s1, s2 := s2} = let k : ℤ := ↑s1 / 53668, s1' : ℤ := 40014 * (↑s1 - k * 53668) - k * 12211, s1'' : ℤ := ite (s1' < 0) (s1' + 2147483563) s1', k' : ℤ := ↑s2 / 52774, s2' : ℤ := 40692 * (↑s2 - k' * 52774) - k' * 3791, s2'' : ℤ := ite (s2' < 0) (s2' + 2147483399) s2', z : ℤ := s1'' - s2'', z' : ℤ := ite (z < 1) (z + 2147483562) (z % 2147483562) in (z'.to_nat, {s1 := s1''.to_nat, s2 := s2''.to_nat})
Equations
- std_split {s1 := s1, s2 := s2} = let new_s1 : ℕ := ite (s1 = 2147483562) 1 (s1 + 1), new_s2 : ℕ := ite (s2 = 1) 2147483398 (s2 - 1), new_g : std_gen := (std_next {s1 := s1, s2 := s2}).snd, left_g : std_gen := {s1 := new_s1, s2 := new_g.s2}, right_g : std_gen := {s1 := new_g.s1, s2 := new_s2} in (left_g, right_g)
@[instance]
Generate a random natural number in the interval [lo, hi].
Equations
- rand_nat g lo hi = let lo' : ℕ := ite (lo > hi) hi lo, hi' : ℕ := ite (lo > hi) lo hi in rand_nat._match_2 g lo' hi' (random_gen.range g)
- rand_nat._match_2 g lo' hi' (gen_lo, gen_hi) = let gen_mag : ℕ := gen_hi - gen_lo + 1, q : ℕ := 1000, k : ℕ := hi' - lo' + 1, tgt_mag : ℕ := k * q in rand_nat._match_1 lo' k (rand_nat_aux gen_lo gen_mag _ tgt_mag 0 g)
- rand_nat._match_1 lo' k (v, g') = let v' : ℕ := lo' + v % k in (v', g')
Generate a random Boolean.
Equations
- rand_bool g = rand_bool._match_1 (rand_nat g 0 1)
- rand_bool._match_1 (v, g') = (decidable.to_bool (v = 1) (nat.decidable_eq v 1), g')