Add System.Random
Unified · Split
| @@ -0,0 +1,68 @@ | |||
| 1 | module System.Random | ||
| 2 | |||
| 3 | import Data.Fin | ||
| 4 | import Data.Vect | ||
| 5 | import Data.List | ||
| 6 | |||
| 7 | public export | ||
| 8 | interface Random a where | ||
| 9 | randomIO : IO a | ||
| 10 | |||
| 11 | -- Takes a range (lo, hi), and returns a random value uniformly | ||
| 12 | -- distributed in the closed interval [lo, hi]. It is unspecified what | ||
| 13 | -- happens if lo > hi. | ||
| 14 | randomRIO : (a, a) -> IO a | ||
| 15 | |||
| 16 | prim_randomInt : Int -> IO Int | ||
| 17 | prim_randomInt upperBound = schemeCall Int "blodwen-random" [upperBound] | ||
| 18 | |||
| 19 | public export | ||
| 20 | Random Int where | ||
| 21 | -- Generate a random value within [-2^31, 2^31-1]. | ||
| 22 | randomIO = | ||
| 23 | let maxInt = shiftL 1 31 - 1 | ||
| 24 | minInt = negate $ shiftL 1 31 | ||
| 25 | range = maxInt - minInt | ||
| 26 | in map (+ minInt) $ prim_randomInt range | ||
| 27 | |||
| 28 | -- Generate a random value within [lo, hi]. | ||
| 29 | randomRIO (lo, hi) = | ||
| 30 | let range = hi - lo + 1 | ||
| 31 | in map (+ lo) $ prim_randomInt range | ||
| 32 | |||
| 33 | prim_randomDouble : IO Double | ||
| 34 | prim_randomDouble = schemeCall Double "blodwen-random" [] | ||
| 35 | |||
| 36 | public export | ||
| 37 | Random Double where | ||
| 38 | -- Generate a random value within [0, 1]. | ||
| 39 | randomIO = prim_randomDouble | ||
| 40 | |||
| 41 | -- Generate a random value within [lo, hi]. | ||
| 42 | randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) prim_randomDouble | ||
| 43 | |||
| 44 | ||| Sets the random seed | ||
| 45 | export | ||
| 46 | srand : Integer -> IO () | ||
| 47 | srand n = schemeCall () "blodwen-random-seed" [n] | ||
| 48 | |||
| 49 | ||| Generate a random number in Fin (S `k`) | ||
| 50 | ||| | ||
| 51 | ||| Note that rndFin k takes values 0, 1, ..., k. | ||
| 52 | public export | ||
| 53 | rndFin : (n : Nat) -> IO (Fin (S n)) | ||
| 54 | rndFin 0 = pure FZ | ||
| 55 | rndFin (S k) = do | ||
| 56 | let intBound = the Int (cast (S k)) | ||
| 57 | randomInt <- randomRIO (0, intBound) | ||
| 58 | pure $ restrict (S k) (cast randomInt) | ||
| 59 | |||
| 60 | ||| Select a random element from a vector | ||
| 61 | public export | ||
| 62 | rndSelect' : {k : Nat} -> Vect (S k) a -> IO a | ||
| 63 | rndSelect' {k} xs = pure $ Vect.index !(rndFin k) xs | ||
| 64 | |||
| 65 | ||| Select a random element from a non-empty list | ||
| 66 | public export | ||
| 67 | rndSelect : (elems : List a) -> {auto prf : NonEmpty elems} -> IO a | ||
| 68 | rndSelect (x :: xs) {prf = IsNonEmpty} = rndSelect' $ fromList (x :: xs) | ||
| @@ -14,6 +14,7 @@ modules = Syntax.WithProof, · 13 unmodified lines | |||
| 14 | Text.Lexer, | 14 | Text.Lexer, |
| 15 | Text.Parser.Core, | 15 | Text.Parser.Core, |
| 16 | Text.Lexer.Core, | 16 | Text.Lexer.Core, |
| 17 | System.Random, | ||
| 17 | Language.JSON, | 18 | Language.JSON, |
| 18 | Language.JSON.Data, | 19 | Language.JSON.Data, |
| 19 | Language.JSON.Lexer, | 20 | Language.JSON.Lexer, |
| @@ -39,6 +39,7 @@ schHeader libs · 38 unmodified lines | |||
| 39 | "(require rnrs/bytevectors-6)\n" ++ -- for buffers | 39 | "(require rnrs/bytevectors-6)\n" ++ -- for buffers |
| 40 | "(require rnrs/io/ports-6)\n" ++ -- for file handling | 40 | "(require rnrs/io/ports-6)\n" ++ -- for file handling |
| 41 | "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C | 41 | "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C |
| 42 | "(require racket/date)\n" ++ -- for date | ||
| 42 | libs ++ | 43 | libs ++ |
| 43 | "(let ()\n" | 44 | "(let ()\n" |
| 44 | 45 | ||
| @@ -69,6 +69,7 @@ updatePaths · 68 unmodified lines | |||
| 69 | defs <- get Ctxt | 69 | defs <- get Ctxt |
| 70 | addPkgDir "prelude" | 70 | addPkgDir "prelude" |
| 71 | addPkgDir "base" | 71 | addPkgDir "base" |
| 72 | addPkgDir "contrib" | ||
| 72 | addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++ | 73 | addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++ |
| 73 | "idris2-" ++ showVersion False version ++ dirSep ++ "support") | 74 | "idris2-" ++ showVersion False version ++ dirSep ++ "support") |
| 74 | addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++ | 75 | addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++ |
| @@ -254,3 +254,28 @@ · 253 unmodified lines | |||
| 254 | 254 | ||
| 255 | (define (blodwen-system cmd) | 255 | (define (blodwen-system cmd) |
| 256 | (system cmd)) | 256 | (system cmd)) |
| 257 | |||
| 258 | ;; Randoms | ||
| 259 | (define random-seed-register 0) | ||
| 260 | (define (initialize-random-seed-once) | ||
| 261 | (if (= (virtual-register random-seed-register) 0) | ||
| 262 | (let ([seed (time-nanosecond (current-time))]) | ||
| 263 | (set-virtual-register! random-seed-register seed) | ||
| 264 | (random-seed seed)))) | ||
| 265 | |||
| 266 | (define (blodwen-random-seed seed) | ||
| 267 | (set-virtual-register! random-seed-register seed) | ||
| 268 | (random-seed seed)) | ||
| 269 | (define blodwen-random | ||
| 270 | (case-lambda | ||
| 271 | ;; no argument, pick a real value from [0, 1.0) | ||
| 272 | [() (begin | ||
| 273 | (initialize-random-seed-once) | ||
| 274 | (random 1.0))] | ||
| 275 | ;; single argument k, pick an integral value from [0, k) | ||
| 276 | [(k) | ||
| 277 | (begin | ||
| 278 | (initialize-random-seed-once) | ||
| 279 | (if (> k 0) | ||
| 280 | (random k) | ||
| 281 | (assertion-violationf 'blodwen-random "invalid range argument ~a" k)))])) | ||
| @@ -254,3 +254,16 @@ · 253 unmodified lines | |||
| 254 | (if (system cmd) | 254 | (if (system cmd) |
| 255 | 0 | 255 | 0 |
| 256 | 1)) | 256 | 1)) |
| 257 | |||
| 258 | ;; Randoms | ||
| 259 | (random-seed (date*-nanosecond (current-date))) ; initialize random seed | ||
| 260 | |||
| 261 | (define (blodwen-random-seed s) (random-seed s)) | ||
| 262 | (define blodwen-random | ||
| 263 | (case-lambda | ||
| 264 | ;; no argument, pick a real value from [0, 1.0) | ||
| 265 | [() (random)] | ||
| 266 | ;; single argument k, pick an integral value from [0, k) | ||
| 267 | [(k) (if (> k 0) | ||
| 268 | (random k) | ||
| 269 | (raise 'blodwen-random-invalid-range-argument))])) | ||