@@ -32,6 +32,15 @@ rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
32 Just v => v
32 Just v => v
33 Nothing => toFin (assert_smaller x (x - cast (S k)))
33 Nothing => toFin (assert_smaller x (x - cast (S k)))
35+||| Select a random element from a vector, or Nothing if the vector is empty
36+rndSelect' : Vect n a -> { [RND] } Eff IO (Maybe a)
37+rndSelect' {n=Z} _ = return Nothing
38+rndSelect' {n=(S k)} xs = return (Just (Vect.index !(rndFin k) xs))
40+||| Select a random element from a list, or Nothing if the list is empty
41+rndSelect : List a -> { [RND] } Eff IO (Maybe a)
42+rndSelect l = rndSelect' (fromList l)
35||| Sets the random seed
44||| Sets the random seed
36srand : Integer -> { [RND] } Eff m ()
45srand : Integer -> { [RND] } Eff m ()
37srand n = setSeed n
46srand n = setSeed n