0 | -- This module contains translation from the Haskell code taken from
  1 | -- https://hackage.haskell.org/package/splitmix-0.1.0.4/docs/src/System.Random.SplitMix.html
  2 | module System.Random.Pure.StdGen
  3 |
  4 | import public Data.Bits
  5 | import Data.Vect
  6 | import public Data.So
  7 |
  8 | import Deriving.Show
  9 |
 10 | import System
 11 | import System.Clock
 12 | import public System.Random.Pure
 13 |
 14 | import Text.PrettyPrint.Bernardy.Core
 15 | import Text.PrettyPrint.Bernardy.Interface
 16 |
 17 | %default total
 18 | %language ElabReflection
 19 |
 20 | ------------------------------------
 21 | --- Utilities over `Bits64` type ---
 22 | ------------------------------------
 23 |
 24 | goldenGamma : Bits64
 25 | goldenGamma = 0x9e3779b97f4a7c15
 26 |
 27 | shiftXor : Fin 64 -> Bits64 -> Bits64
 28 | shiftXor n w = w `xor` (w `shiftR` n)
 29 |
 30 | shiftXorMultiply : Fin 64 -> Bits64 -> Bits64 -> Bits64
 31 | shiftXorMultiply n k w = shiftXor n w * k
 32 |
 33 | mix64, mix64v13 : Bits64 -> Bits64
 34 | mix64    = shiftXor 33 . shiftXorMultiply 33 0xc4ceb9fe1a85ec53 . shiftXorMultiply 33 0xff51afd7ed558ccd
 35 | mix64v13 = shiftXor 31 . shiftXorMultiply 27 0x94d049bb133111eb . shiftXorMultiply 30 0xbf58476d1ce4e5b9
 36 |
 37 | mixGamma : Bits64 -> Bits64
 38 | mixGamma z0 = do
 39 |   let z1 = mix64v13 z0 .|. 1             -- force to be odd
 40 |       n  = popCount $ z1 `xor` (z1 `shiftR` 1)
 41 |   -- see: http://www.pcg-random.org/posts/bugs-in-splitmix.html
 42 |   -- let's trust the text of the paper, not the code.
 43 |   if n >= 24 then z1 else z1 `xor` 0xaaaaaaaaaaaaaaaa
 44 |
 45 | -------------------------------------------------
 46 | --- The `StdGen` type and its implementations ---
 47 | -------------------------------------------------
 48 |
 49 | export
 50 | data StdGen = MkStdGen Bits64 Bits64
 51 |
 52 | export
 53 | Eq StdGen where
 54 |   MkStdGen seed gamma == MkStdGen seed' gamma' = seed == seed' && gamma == gamma'
 55 |
 56 | export
 57 | RandomGen StdGen where
 58 |
 59 |   next $ MkStdGen seed gamma = do
 60 |     let seed' = seed + gamma
 61 |     (MkStdGen seed' gamma, mix64 seed')
 62 |
 63 |   split $ MkStdGen seed gamma = do
 64 |     let seed'  = seed + gamma
 65 |         seed'' = seed' + gamma
 66 |     (MkStdGen seed'' gamma, MkStdGen (mix64 seed') (mixGamma seed''))
 67 |
 68 |   -- idea taken from https://github.com/qfpl/hedgehog-fn/blob/2621548943ffa46c98f430cca6beeb9025ea3127/src/Hedgehog/Function/Internal.hs#L73
 69 |   variant v $ MkStdGen seed gamma = MkStdGen (seed + cast v) gamma
 70 |
 71 | export
 72 | Show StdGen where
 73 |   -- since the constructor is not public, creation of literally any value
 74 |   -- can be done through a smart-constructor, so, showing it through it.
 75 |   showPrec d $ MkStdGen s g = showCon d "rawStdGen" $ showArg s ++ showArg g
 76 |
 77 | export
 78 | Pretty StdGen where
 79 |   prettyPrec d $ MkStdGen s g = prettyCon d "rawStdGen" [prettyArg s, prettyArg g]
 80 |
 81 | export
 82 | extractRaw : StdGen -> (Bits64, Bits64)
 83 | extractRaw $ MkStdGen seed gamma = (seed, gamma)
 84 |
 85 | --- Creation of `StdGen` values ---
 86 |
 87 | export %inline
 88 | rawStdGen : (seed, gamma : Bits64) -> (0 gammaIsOdd : So $ testBit gamma 0) => StdGen
 89 | rawStdGen s g = MkStdGen s g
 90 |
 91 | ||| The most preferrable, but not invertible way for creation specific seed values
 92 | export
 93 | mkStdGen : Bits64 -> StdGen
 94 | mkStdGen s = MkStdGen (mix64 s) (mixGamma (s + goldenGamma))
 95 |
 96 | export
 97 | someStdGen : StdGen
 98 | someStdGen = rawStdGen 23462 254334222987
 99 |
100 | ||| The way of creation of a seed value based on some system entropy
101 | export
102 | initStdGen : HasIO io => io StdGen
103 | initStdGen = do
104 |   nano <- liftIO $ toNano <$> clockTime UTC
105 |   pure $ mkStdGen $ cast !time `xor` cast nano `xor` cast !getPID
106 |
107 | export %defaulthint
108 | EntropySeed : HasIO m => CanInitSeed StdGen m
109 | EntropySeed = E where [E] CanInitSeed StdGen m where initSeed = initStdGen
110 |