Documentation

Init.Data.Random

class RandomGen (g : Type u) :

Type u

range : g → Nat × Nat
next : g → Nat × g
split : g → g × g

Instances

instRandomGenStdGen

structure StdGen:

Type

s1 : Nat
s2 : Nat

instance instInhabitedStdGen:

Inhabited StdGen

Equations

instInhabitedStdGen = { default := { s1 := 0, s2 := 0 } }

Equations

stdRange = (1, 2147483562)

instance instReprStdGen:

Equations

One or more equations did not get rendered due to their size.

StdGen → Nat × StdGen

Equations

One or more equations did not get rendered due to their size.

StdGen → StdGen × StdGen

Equations

One or more equations did not get rendered due to their size.

instance instRandomGenStdGen:

RandomGen StdGen

Equations

instRandomGenStdGen = { range := fun x => stdRange, next := stdNext, split := stdSplit }

def mkStdGen (s : optParam Nat 0) :

Return a standard number generator.

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

Generate a random natural number in the interval [lo, hi].

Equations

One or more equations did not get rendered due to their size.

def randBool {gen : Type u} [inst : RandomGen gen] (g : gen) :

Generate a random Boolean.

Equations

randBool g = match randNat g 0 1 with | (v, g') => (decide (v = 1), g')

opaque IO.stdGenRef:

def IO.setRandSeed (n : Nat) :

Equations

IO.setRandSeed n = ST.Ref.set IO.stdGenRef (mkStdGen n)

def IO.rand (lo : Nat) (hi : Nat) :

Equations

IO.rand lo hi = do let gen ← ST.Ref.get IO.stdGenRef match randNat gen lo hi with | (r, gen) => do ST.Ref.set IO.stdGenRef gen pure r