
  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 idx = seed `mod` (S k)
 17 |       i   = restrict k (cast idx)
 18 |       xs' = swapFin FZ i xs
 19 |       seed' = lcg seed
 20 |   in head xs' :: shuffleVect seed' (tail xs')
 21 |   where
 22 |     swapFin : Fin (S k) -> Fin (S k) -> Vect (S k) a -> Vect (S k) a
 23 |     swapFin i j v =
 24 |       let vi = index i v
 25 |           vj = index j v
 26 |       in replaceAt i vj (replaceAt j vi v)
 27 | 
 28 | ||| Shuffle a list using a seed value.
 29 | export
 30 | shuffle : Nat -> List a -> List a
 31 | shuffle seed xs =
 32 |   let v = fromList xs
 33 |   in toList (shuffleVect seed v)
 34 |