libs/effects/Effect/Random.idr · Idris-dev

git.iko.soy/Idris-dev

on ec2a48a help sign in

49 lines 1.6 kB history raw

1module Effect.Random

3import Effects

4import Data.Vect

5import Data.Fin

7data Random : Effect where

8 getRandom : { Integer } Random Integer

9 setSeed : Integer -> { Integer } Random ()

11using (m : Type -> Type)

12 instance 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 -> { [RND] } Eff Integer

23rndInt lower upper = do v <- call $ getRandom

24 return ((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) -> { [RND] } Eff (Fin (S k))

30rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

31 return (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 -> { [RND] } Eff a

39rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

41||| Select a random element from a list, or Nothing if the list is empty

42rndSelect : List a -> { [RND] } Eff (Maybe a)

43rndSelect [] = return Nothing

44rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

46||| Sets the random seed

47srand : Integer -> { [RND] } Eff ()

48srand n = call $ setSeed n