PRNG

rng.u

-- splittable RNG type
ability Random where
  nat : Nat
  split : {Random} (forall g a. '{Random,g} a ->{g} a)

{{ ``Random.natIn i j`` generates a {type Nat} between ''i'' and ''j'', 
   not including ''j''.

   If ''j'' is less than or equal to ''i'', throws an error.

   # Examples
   
   ```
   Random.mmix 384 '(List.replicate 5 '(natIn 5 15))
   ```

   ```
   Random.mmix 37 '(natIn 8 3)
   ```
}}
Random.natIn : Nat -> Nat ->{Random} Nat
Random.natIn start stopExclusive = 
  if start < stopExclusive then 
    Random.nat `mod` Nat.drop stopExclusive start + start
  else bug ("Random.natIn start must be < stop", start, stopExclusive)

Random.boolean : '{Random} Boolean
Random.boolean _ = Nat.popCount Random.nat >= 32

> mmix 38 '(List.replicate 10 Random.boolean)

Random.lcg.handler : Nat -> Nat -> Nat -> Nat -> Request {Random} a -> a
Random.lcg.handler modulus a c = 
  update = if modulus `Nat.eq` 0 then (seed -> a * seed + c)
           else (seed -> (a * seed + c) `mod` modulus)
  go : Nat -> Request {Random} x -> x
  go seed = cases
    { a } -> a
    { Random.nat -> resume } -> 
      seed' = update seed
      handle resume seed' with go seed'  
    { Random.split -> resume } -> 
      seed' = Nat.complement (update seed) `Nat.xor` seed
      seed'' = update seed'
      handle resume (r -> handle !r with go seed') 
      with go seed''
  go

{{ 
  ``lcg modulus a c seed`` generates random numbers using 
  a [linear congruential random number generator](https://en.wikipedia.org/wiki/Linear_congruential_generator). 
  
  This function generally shouldn't be used directly. See for instance 
  {Random.mmix} which calls this function with known-good choices
  for ''a'', ''c'', and ''modulus''.
}} 
Random.lcg : Nat -> Nat -> Nat -> Nat -> '{Random,g} a ->{g} a
Random.lcg mod a c seed r = handle !r with Random.lcg.handler mod a c seed

Random.mmix : Nat -> '{Random,g} a ->{g} a
Random.mmix seed r = 
  lcg 0 6364136223846793005 1442695040888963407 seed r