git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/effects/Effect/Random.idr
49 lines 1.6 kB history raw
1module Effect.Random
3import Effects
4import Data.Vect
6%access public export
8data Random : Effect where
9 GetRandom : sig Random Integer Integer
10 SetSeed : Integer -> sig Random () Integer
12implementation Handler Random m where
13 handle seed GetRandom k
14 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
15 k seed' seed'
16 handle seed (SetSeed n) k = k () n
18RND : EFFECT
19RND = MkEff Integer Random
21||| Generates a random Integer in a given range
22rndInt : Integer -> Integer -> Eff Integer [RND]
23rndInt lower upper = do v <- call $ GetRandom
24 pure ((v `prim__sremBigInt` (upper - lower)) + lower)
26||| Generate a random number in Fin (S `k`)
27|||
28||| Note that rndFin k takes values 0, 1, ..., k.
29rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
30rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast (S k))
31 pure (toFin v)
32 where toFin : Integer -> Fin (S k)
33 toFin x = case integerToFin x (S k) of
34 Just v => v
35 Nothing => toFin (assert_smaller x (x - cast (S k)))
37||| Select a random element from a vector
38rndSelect' : Vect (S k) a -> Eff a [RND]
39rndSelect' {k} xs = pure (Vect.index !(rndFin k) xs)
41||| Select a random element from a list, or Nothing if the list is empty
42rndSelect : List a -> Eff (Maybe a) [RND]
43rndSelect [] = pure Nothing
44rndSelect (x::xs) = pure (Just !(rndSelect' (x::(fromList xs))))
46||| Sets the random seed
47srand : Integer -> Eff () [RND]
48srand n = call $ SetSeed n