@@ -16,10 +16,14 @@ 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))
24rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
28rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
25 return (toFin v)
29 return (toFin v)
@@ -28,6 +32,7 @@ rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
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+||| Sets the random seed
31srand : Integer -> { [RND] } Eff m ()
36srand : Integer -> { [RND] } Eff m ()
32srand n = setSeed n
37srand n = setSeed n