git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/libs/effects/Effect/Random.idr
66 lines 2.6 kB history raw
1module Effect.Random
3import Effects
4import Data.Vect
6%access public export
8{-
9 - This code implements a 'Linear Congruential Generator' as described here
10 - https://en.wikipedia.org/wiki/Linear_congruential_generator
11 -
12 - Looking at the wiki page for 'linear congruential generator' it looks like the
13 - parameters used by Idris come from the 'Numerical Recipes' books. The web page
14 - does not give any known issues with these parameters, however another example is
15 - known to have this bug: "If Xn is even then Xn+1 will be odd, and vice versa-the
16 - lowest bit oscillates at each step." So although the 'Numerical Recipes' parameters
17 - are not listed with this issue they do have it. Some of the implementations do not
18 - use the lower significant bits so divBigInt v 2 has been added to do this.
19 -}
21data Random : Effect where
22 GetRandom : sig Random Integer Integer
23 SetSeed : Integer -> sig Random () Integer
25implementation Handler Random m where
26 handle seed GetRandom k
27 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
28 k seed' seed'
29 handle seed (SetSeed n) k = k () n
31RND : EFFECT
32RND = MkEff Integer Random
34||| Generates a random Integer in a given range
35rndInt : Integer -> Integer -> Eff Integer [RND]
36rndInt lower upper = do v <- call $ GetRandom
37 pure (((divBigInt v 2) `prim__sremBigInt` (upper - lower)) + lower)
38 -- divBigInt v 2 is required to prevent low bit alternating between
39 -- 0 and 1 (odd and even)
41||| Generate a random number in Fin (S `k`)
42|||
43||| Note that rndFin k takes values 0, 1, ..., k.
44rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
45rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast (S k))
46 pure (toFin (divBigInt v 2))
47 where toFin : Integer -> Fin (S k)
48 toFin x = case integerToFin x (S k) of
49 Just v => v
50 Nothing => toFin (assert_smaller x (x - cast (S k)))
51 -- divBigInt v 2 is required to prevent low bit alternating between
52 -- 0 and 1 (odd and even)
54||| Select a random element from a vector
55rndSelect' : Vect (S k) a -> Eff a [RND]
56rndSelect' {k} xs = pure (Vect.index !(rndFin k) xs)
58||| Select a random element from a list, or Nothing if the list is empty
59rndSelect : List a -> Eff (Maybe a) [RND]
60rndSelect [] = pure Nothing
61rndSelect (x::xs) = pure (Just !(rndSelect' (x::(fromList xs))))
63||| Sets the random seed
64srand : Integer -> Eff () [RND]
65srand n = call $ SetSeed n