Documentation

Init.Data.Random

class RandomGen (g : Type u) :
Type u
Instances
structure StdGen :
Type
Equations
Equations
Equations
Equations
  • stdNext x = match x with | { s1 := s1, s2 := s2 } => let s1 := Int.ofNat s1; let s2 := Int.ofNat s2; let k := s1 / 53668; let s1' := 40014 * (s1 - k * 53668) - k * 12211; let s1'' := if s1' < 0 then s1' + 2147483563 else s1'; let k' := s2 / 52774; let s2' := 40692 * (s2 - k' * 52774) - k' * 3791; let s2'' := if s2' < 0 then s2' + 2147483399 else s2'; let z := s1'' - s2''; let z' := if z < 1 then z + 2147483562 else z % 2147483562; (Int.toNat z', { s1 := Int.toNat s1'', s2 := Int.toNat s2'' })
Equations
  • stdSplit x = match x with | g@h:{ s1 := s1, s2 := s2 } => let newS1 := if s1 = 2147483562 then 1 else s1 + 1; let newS2 := if s2 = 1 then 2147483398 else s2 - 1; let newG := (stdNext g).snd; let leftG := { s1 := newS1, s2 := newG.s2 }; let rightG := { s1 := newG.s1, s2 := newS2 }; (leftG, rightG)
Equations
def mkStdGen (s : optParam Nat 0) :
Equations
  • mkStdGen s = let q := s / 2147483562; let s1 := s % 2147483562; let s2 := q % 2147483398; { s1 := s1 + 1, s2 := s2 + 1 }
def randNat {gen : Type u} [inst : RandomGen gen] (g : gen) (lo : Nat) (hi : Nat) :
Nat × gen
Equations
  • randNat g lo hi = let lo' := if lo > hi then hi else lo; let hi' := if lo > hi then lo else hi; let x := RandomGen.range g; match x with | (genLo, genHi) => let genMag := genHi - genLo + 1; let q := 1000; let k := hi' - lo' + 1; let tgtMag := k * q; let x := randNatAux genLo genMag tgtMag (0, g); match x with | (v, g') => let v' := lo' + v % k; (v', g')
def randBool {gen : Type u} [inst : RandomGen gen] (g : gen) :
Bool × gen
Equations
def IO.rand (lo : Nat) (hi : Nat) :
Equations