git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/contrib/Control/ST/Random.idr
42 lines 1.5 kB history raw
1module Control.ST.Random
3import Control.ST
4import Data.Vect
6%access public export
8Random : Type
9Random = State Integer
11getRandom : (rnd : Var) -> ST m Integer [rnd ::: Random]
12getRandom rnd =
13 do
14 st <- read rnd
15 let st' = assert_total ((1664525 * st + 1013904223) `prim__sremBigInt` (pow 2 32))
16 write rnd st'
17 pure st'
19||| Generates a random Integer in a given range
20rndInt : (rnd : Var) -> Integer -> Integer -> ST m Integer [rnd ::: Random]
21rndInt rnd lower upper = do v <- getRandom rnd
22 pure $ assert_total ((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 : (rnd : Var) -> (k : Nat) -> ST m (Fin (S k)) [rnd ::: Random]
28rndFin rnd k = do let v = assert_total $ !(getRandom rnd) `prim__sremBigInt` (cast (S k))
29 pure (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' : (rnd : Var) -> Vect (S k) a -> ST m a [rnd ::: Random]
37rndSelect' {k} rnd xs = pure (Vect.index !(rndFin rnd k) xs)
39||| Select a random element from a non-empty list
40rndSelect : (rnd : Var) -> (xs : List a) -> {auto ok : NonEmpty xs} -> ST m a [rnd ::: Random]
41rndSelect rnd (x::xs) {ok=NonEmpty} = pure ( !(rndSelect' rnd (x::(fromList xs))))
42rndSelect rnd [] {ok=NonEmpty} impossible