core / system.random - mathlib docs

std_gen.has_repr = {repr := λ (_x : std_gen), std_gen.has_repr._match_1 _x}
std_gen.has_repr._match_1 {s1 := s1, s2 := s2} = "⟨" ++ to_string s1 ++ ", " ++ to_string s2 ++ "⟩"

def std_next :

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})

def std_split :

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)

@[protected, instance]

Equations

def mk_std_gen (s : ℕ := 0) :

Return a standard number generator.

Equations

mk_std_gen s = let q : ℕ := 0 := s / 2147483562, s1 : ℕ := 0 := s % 2147483562, s2 : ℕ := 0 := q % 2147483398 in {s1 := s1 + 1, s2 := s2 + 1}

def rand_nat {gen : Type u} [random_gen gen] (g : gen) (lo hi : ℕ) :

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')

def rand_bool {gen : Type u} [random_gen gen] (g : gen) :

Generate a random Boolean.

Equations