git.iko.soy/Idris-dev
on dd09721 help sign in
Idris-dev/libs/effects/Effect/Random.idr
33 lines 1.0 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' = (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
19rndInt : Integer -> Integer -> { [RND] } Eff m Integer
20rndInt lower upper = do v <- getRandom
21 return (v `prim__sremBigInt` (upper - lower) + lower)
23rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
24rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)
25 return (toFin v)
26 where toFin : Integer -> Fin (S k)
27 toFin x = case integerToFin x (S k) of
28 Just v => v
29 Nothing => toFin (assert_smaller x (x - cast (S k)))
31srand : Integer -> { [RND] } Eff m ()
32srand n = setSeed n