0 | module System.Random
 1 |
 2 | import Data.Fin
 3 | import Data.Vect
 4 | import Data.List
 5 |
 6 | public export
 7 | interface Random a where
 8 |   randomIO : HasIO io => io a
 9 |
10 |   ||| Takes a range (lo, hi), and returns a random value uniformly
11 |   ||| distributed in the closed interval [lo, hi]. It is unspecified what
12 |   ||| happens if lo > hi.
13 |   randomRIO : HasIO io => (a, a) -> io a
14 |
15 | %foreign "scheme:blodwen-random"
16 |          "javascript:lambda:(max)=>Math.floor(Math.random() * max)"
17 | prim__randomBits32 : Bits32 -> PrimIO Bits32
18 |
19 | randomBits32 : Bits32 -> IO Bits32
20 | randomBits32 upperBound = fromPrim (prim__randomBits32 upperBound)
21 |
22 | public export
23 | Random Int32 where
24 |   -- Generate a random value within [-2^31, 2^31-1].
25 |   randomIO = do
26 |     let maxInt : Bits32    = 2147483647 -- shiftL 1 31 - 1
27 |         negMinInt : Bits32 = 2147483648 -- negate $ shiftL 1 31
28 |         magnitude : Bits32 = maxInt + negMinInt
29 |     bits32 <- liftIO $ randomBits32 magnitude
30 |     let int : Integer = cast bits32
31 |     pure . cast $ int - (cast negMinInt)
32 |
33 |   -- Generate a random value within [lo, hi].
34 |   randomRIO (lo, hi) =
35 |     let range : Integer = (cast hi) - (cast lo) + 1
36 |      in pure . cast $ !(liftIO . randomBits32 $ cast range) + cast lo
37 |
38 | %foreign "scheme:blodwen-random"
39 |          "javascript:lambda:()=>Math.random()"
40 | prim__randomDouble : PrimIO Double
41 |
42 | randomDouble : IO Double
43 | randomDouble = fromPrim prim__randomDouble
44 |
45 | public export
46 | Random Double where
47 |   -- Generate a random value within [0, 1].
48 |   randomIO = liftIO randomDouble
49 |
50 |   -- Generate a random value within [lo, hi].
51 |   randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) (liftIO randomDouble)
52 |
53 | %foreign "scheme:blodwen-random-seed"
54 | prim__srand : Bits64 -> PrimIO ()
55 |
56 | ||| Sets the random seed
57 | export
58 | srand : Bits64 -> IO ()
59 | srand n = fromPrim (prim__srand n)
60 |
61 | ||| Generate a random number in Fin (S `k`)
62 | |||
63 | ||| Note that rndFin k takes values 0, 1, ..., k.
64 | public export
65 | rndFin : HasIO io => (n : Nat) -> io (Fin (S n))
66 | rndFin 0 = pure FZ
67 | rndFin (S k) = do
68 |   let intBound = the Int32 (cast (S k))
69 |   randomInt <- randomRIO (0, intBound)
70 |   pure $ restrict (S k) (cast randomInt)
71 |
72 | ||| Select a random element from a vector
73 | public export
74 | rndSelect' : HasIO io => {k : Nat} -> Vect (S k) a -> io a
75 | rndSelect' xs = pure $ Vect.index !(rndFin k) xs
76 |
77 | ||| Select a random element from a non-empty list
78 | public export
79 | rndSelect : HasIO io => (elems : List a) -> (0 _ : NonEmpty elems) => io a
80 | rndSelect (x :: xs) = rndSelect' $ fromList (x :: xs)
81 |
82 |