0 | {- Tian Z (ecburx@burx.vip) -}
 1 |
 2 | module IdrisGL.Random
 3 |
 4 | import Data.Fin
 5 |
 6 | {- 
 7 |     FFI 
 8 | -}
 9 |
10 | frgn : String -> String
11 | frgn func = "C:" ++ func ++ ",random"
12 |
13 | --
14 |
15 | %foreign frgn "randomInt"
16 | prim_randomInt : Int -> Int -> Int
17 |
18 | ||| An unsafe, predictable and limited random integer generator, in range [lower, upper].
19 | ||| Switch <lower> and <upper> if <upper> is LOWER than <lower>.
20 | |||
21 | ||| This function is only for users who want to easily render random picture elements.
22 | ||| Please don't use it for precise calculations.
23 | ||| No random built-in functions been found in idris2 version 0.4.
24 | |||
25 | ||| @ lower Lower bound.
26 | ||| @ upper Upper bound.
27 | export
28 | randomInt : (lower : Int) -> (upper : Int) -> Int
29 | randomInt lower upper = prim_randomInt lower upper
30 |
31 | ||| An unsafe, predictable and limited random natrual number generator, in range [lower, upper].
32 | ||| Switch <lower> and <upper> if <upper> is LOWER than <lower>.
33 | |||
34 | ||| This function is only for users who want to easily render random picture elements.
35 | ||| Please don't use it for precise calculations.
36 | ||| No random built-in functions been found in idris2 version 0.4.
37 | |||
38 | ||| @ lower Lower bound.
39 | ||| @ upper Upper bound.
40 | export
41 | randomNat : (lower : Nat) -> (upper : Nat) -> Nat
42 | randomNat lower upper = integerToNat . cast $ prim_randomInt (cast lower) (cast upper)
43 |
44 | ||| An unsafe, predictable and limited random (Fin upper) generator, in range [lower, upper].
45 | ||| Switch <lower> and <upper> if <upper> is LOWER than <lower>.
46 | |||
47 | ||| This function is only for users who want to easily render random picture elements.
48 | ||| Please don't use it for precise calculations.
49 | ||| No random built-in functions been found in idris2 version 0.4.
50 | |||
51 | ||| @ lower Lower bound.
52 | ||| @ upper Upper bound.
53 | export
54 | randomFin : (lower : Nat) -> (upper : Nat) -> Maybe $ Fin upper
55 | randomFin lower upper = natToFin (randomNat lower upper) upper
56 |
57 | export
58 | randomPick : List a -> Maybe a
59 | randomPick Nil = Nothing
60 | randomPick l   =
61 |     let i : Nat := randomNat 0 (minus (length l) 1)
62 |     in  randomPick' i l
63 |     where randomPick' : Nat -> List a -> Maybe a
64 |           randomPick' _ Nil     = Nothing
65 |           randomPick' 0 (x::xs) = Just x
66 |           randomPick' i (x::xs) = randomPick' (minus i 1) xs