Basic random number generator support based on the one available on the Haskell library

class RandomGen (g : Type u) : Type u

Interface for random number generators.

• range : g → Nat × Nat

  range returns the range of values returned by the generator.

• next : g → Nat × g

  next operation returns a natural number that is uniformly distributed the range returned by range (including both end points), and a new generator.

• split : g → g × g

  The 'split' operation allows one to obtain two distinct random number generators. This is very useful in functional programs (for example, when passing a random number generator down to recursive calls).

structure StdGen : Type

"Standard" random number generator.

• s1 : Nat
• s2 : Nat

def mkStdGen (s : Nat := 0) : StdGen

Returns a standard number generator.

Equations

• mkStdGen s = { s1 := s % 2147483562 + 1, s2 := s / 2147483562 % 2147483398 + 1 }

instance instInhabitedStdGen : Inhabited StdGen

Equations

• instInhabitedStdGen = { default := mkStdGen }

def stdRange : Nat × Nat

The range of values returned by StdGen

Equations

• stdRange = (1, 2147483562)

instance instReprStdGen : Repr StdGen

Equations

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

def stdNext : StdGen → Nat × StdGen

The next value from a StdGen, paired with an updated generator state.

Equations

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

def stdSplit : StdGen → StdGen × StdGen

Splits a StdGen into two separate states.

Equations

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

instance instRandomGenStdGen : RandomGen StdGen

Equations

• instRandomGenStdGen = { range := fun (x : StdGen) => stdRange, next := stdNext, split := stdSplit }

def randNat {gen : Type u} [RandomGen gen] (g : gen) (lo hi : Nat) : Nat × gen

Generates 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} [RandomGen gen] (g : gen) : Bool × gen

Generates a random Boolean.

Equations

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

opaque IO.stdGenRef : Ref StdGen

def IO.setRandSeed (n : Nat) : BaseIO Unit

Seeds the random number generator state used by IO.rand.

Equations

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

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

Returns a pseudorandom number between lo and hi, using and updating a saved random generator state.

This state can be seeded using IO.setRandSeed.

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