git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/oldeffects/Effect/Random.idr
47 lines 1.6 kB history raw
1module Effect.Random
3import Effects
5data Random : Effect where
6 getRandom : { Integer } Random Integer
7 setSeed : Integer -> { Integer } Random ()
9using (m : Type -> Type)
10 instance Handler Random m where
11 handle seed getRandom k
12 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
13 k seed' seed'
14 handle seed (setSeed n) k = k () n
16RND : EFFECT
17RND = MkEff Integer Random
19||| Generates a random Integer in a given range
20rndInt : Integer -> Integer -> { [RND] } Eff m Integer
21rndInt lower upper = do v <- call $ getRandom
22 return (v `prim__sremBigInt` (upper - lower) + lower)
24||| Generate a random number in Fin (S `k`)
25|||
26||| Note that rndFin k takes values 0, 1, ..., k.
27rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
28rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
29 return (toFin v)
30 where toFin : Integer -> Fin (S k)
31 toFin x = case integerToFin x (S k) of
32 Just v => v
33 Nothing => toFin (assert_smaller x (x - cast (S k)))
35||| Select a random element from a vector
36rndSelect' : Vect (S k) a -> { [RND] } Eff IO a
37rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
39||| Select a random element from a list, or Nothing if the list is empty
40rndSelect : List a -> { [RND] } Eff IO (Maybe a)
41rndSelect [] = return Nothing
42rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
44||| Sets the random seed
45srand : Integer -> { [RND] } Eff m ()
46srand n = call $ setSeed n