7data Random : Effect where
8 getRandom : sig Random Integer Integer
9 setSeed : Integer -> sig Random () Integer
11instance Handler Random m where
12 handle seed getRandom k
13 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
15 handle seed (setSeed n) k = k () n
18RND = MkEff Integer Random
20||| Generates a random Integer in a given range
21rndInt : Integer -> Integer -> Eff Integer [RND]
22rndInt lower upper = do v <- call $ getRandom
23 return ((v `prim__sremBigInt` (upper - lower)) + lower)
25||| Generate a random number in Fin (S `k`)
27||| Note that rndFin k takes values 0, 1, ..., k.
28rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
29rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
31 where toFin : Integer -> Fin (S k)
32 toFin x = case integerToFin x (S k) of
34 Nothing => toFin (assert_smaller x (x - cast (S k)))
36||| Select a random element from a vector
37rndSelect' : Vect (S k) a -> Eff a [RND]
38rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
40||| Select a random element from a list, or Nothing if the list is empty
41rndSelect : List a -> Eff (Maybe a) [RND]
42rndSelect [] = return Nothing
43rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
45||| Sets the random seed
46srand : Integer -> Eff () [RND]
47srand n = call $ setSeed n
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list