
  0 | module Evince.Random
  1 | 
  2 | import Data.Vect
  3 | import Data.List
  4 | 
  5 | %default total
  6 | 
  7 | -- Minimal LCG (Numerical Recipes constants)
  8 | lcg : Nat -> Nat
  9 | lcg s = cast {to = Nat} $ (cast {to = Integer} s * 1664525 + 1013904223) `mod` 4294967296
 10 | 
 11 | -- Fisher-Yates shuffle on a Vect, driven by LCG.
 12 | shuffleVect : {n : Nat} -> Nat -> Vect n a -> Vect n a
 13 | shuffleVect {n = 0}     _    xs = xs
 14 | shuffleVect {n = 1}     _    xs = xs
 15 | shuffleVect {n = S k}   seed xs =
 16 |   let i     = restrict k (cast seed)
 17 |       xs'   = swapFin FZ i xs
 18 |       seed' = lcg seed
 19 |   in head xs' :: shuffleVect seed' (tail xs')
 20 |   where
 21 |     swapFin : Fin (S k) -> Fin (S k) -> Vect (S k) a -> Vect (S k) a
 22 |     swapFin i j v =
 23 |       let vi = index i v
 24 |           vj = index j v
 25 |       in replaceAt i vj (replaceAt j vi v)
 26 | 
 27 | ||| Advance a seed to the next value in the pseudo-random sequence.
 28 | export
 29 | nextSeed : Nat -> Nat
 30 | nextSeed = lcg
 31 | 
 32 | ||| Shuffle a list using a seed value.
 33 | export
 34 | shuffle : Nat -> List a -> List a
 35 | shuffle seed xs =
 36 |   let v = fromList xs
 37 |   in toList (shuffleVect seed v)
 38 |