@@ -16,18 +16,32 @@ using (m : Type -> Type)
16RND : EFFECT
16RND : EFFECT
17RND = MkEff Integer Random
17RND = MkEff Integer Random
19+||| Generates a random Integer in a given range
19rndInt : Integer -> Integer -> { [RND] } Eff m Integer
20rndInt : Integer -> Integer -> { [RND] } Eff m Integer
20rndInt lower upper = do v <- getRandom
21rndInt lower upper = do v <- getRandom
21 return (v `prim__sremBigInt` (upper - lower) + lower)
22 return (v `prim__sremBigInt` (upper - lower) + lower)
24+||| Generate a random number in Fin (S `k`)
26+||| Note that rndFin k takes values 0, 1, ..., k.
23rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
27rndFin : (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))
25 return (toFin v)
29 return (toFin v)
26 where toFin : Integer -> Fin (S k)
30 where toFin : Integer -> Fin (S k)
27 toFin x = case integerToFin x (S k) of
31 toFin x = case integerToFin x (S k) of
28 Just v => v
32 Just v => v
29 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
36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a
37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
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))))
44+||| Sets the random seed
31srand : Integer -> { [RND] } Eff m ()
45srand : Integer -> { [RND] } Eff m ()
32srand n = setSeed n
46srand n = setSeed n