@@ -16,18 +16,32 @@ using (m : Type -> Type)
1616RND : EFFECT
1717RND = MkEff Integer Random
1818
19+||| Generates a random Integer in a given range
1920rndInt : Integer -> Integer -> { [RND] } Eff m Integer
2021rndInt lower upper = do v <- getRandom
2122 return (v `prim__sremBigInt` (upper - lower) + lower)
2223
24+||| Generate a random number in Fin (S `k`)
25+|||
26+||| Note that rndFin k takes values 0, 1, ..., k.
2327rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
24−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)
28+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
2529 return (toFin v)
2630 where toFin : Integer -> Fin (S k)
2731 toFin x = case integerToFin x (S k) of
2832 Just v => v
2933 Nothing => toFin (assert_smaller x (x - cast (S k)))
3034
35+||| Select a random element from a vector
36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a
37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
38+
39+||| Select a random element from a list, or Nothing if the list is empty
40+rndSelect : List a -> { [RND] } Eff IO (Maybe a)
41+rndSelect [] = return Nothing
42+rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
43+
44+||| Sets the random seed
3145srand : Integer -> { [RND] } Eff m ()
3246srand n = setSeed n
3347