@@ -32,6 +32,15 @@ rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
3232 Just v => v
3333 Nothing => toFin (assert_smaller x (x - cast (S k)))
3434
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))
39+
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)
43+
3544||| Sets the random seed
3645srand : Integer -> { [RND] } Eff m ()
3746srand n = setSeed n