-- | Replay seeds
--
-- We need a seed/gamma pair to initialize a splitmix PRNG. This is however a
-- pretty low level implementation detail that I'd prefer not be be directly
-- visible. We therefore provide a thin layer on top, which provides an
-- "encoded" replay seed. This has the additional benefits that the length of
-- the replay seed is always the same (unlike just writing a 'Word64'), and we
-- could in principle at some point support other kinds of PRNGs.
module Test.Falsify.Internal.Driver.ReplaySeed (
    ReplaySeed(..)
  , parseReplaySeed
  , splitmixReplaySeed
  ) where

import Data.String
import Data.Word
import Data.Binary
import System.Random.SplitMix

import qualified Data.ByteString.Base16.Lazy as Lazy.Base16
import qualified Data.ByteString.Lazy.Char8  as Lazy.Char8

-- | Replay seed
--
-- By default, when we falsify a property we start with a PRNG initialized using
-- a random seed (produced using the system entropy; this relies on
-- 'System.Random.SplitMix.initSMGen' in @splitmix@). When a property /fails/,
-- we will report the exact seed used, so that the user can re-run the exact
-- same test again, if desired.
--
-- The definition of t'ReplaySeed' is part of @falsify's@ public API, to make it
-- possible to use custom drivers.
data ReplaySeed = ReplaySeed{
      ReplaySeed -> Word64
replaySeed  :: Word64 -- ^ Seed
    , ReplaySeed -> Word64
replayGamma :: Word64 -- ^ Gamma (must be odd)
    }

splitmixReplaySeed :: SMGen -> ReplaySeed
splitmixReplaySeed :: SMGen -> ReplaySeed
splitmixReplaySeed = (Word64 -> Word64 -> ReplaySeed) -> (Word64, Word64) -> ReplaySeed
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Word64 -> Word64 -> ReplaySeed
ReplaySeed ((Word64, Word64) -> ReplaySeed)
-> (SMGen -> (Word64, Word64)) -> SMGen -> ReplaySeed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMGen -> (Word64, Word64)
unseedSMGen

instance Binary ReplaySeed where
  put :: ReplaySeed -> Put
put ReplaySeed{Word64
replaySeed :: ReplaySeed -> Word64
replaySeed :: Word64
replaySeed, Word64
replayGamma :: ReplaySeed -> Word64
replayGamma :: Word64
replayGamma} = do
      Word8 -> Put
putWord8 Word8
1
      Word64 -> Put
forall t. Binary t => t -> Put
put Word64
replaySeed
      Word64 -> Put
forall t. Binary t => t -> Put
put Word64
replayGamma

  get :: Get ReplaySeed
get = do
      Word8
tag <- Get Word8
getWord8
      case Word8
tag of
        Word8
1 -> do Word64
replaySeed  <- Get Word64
forall t. Binary t => Get t
get
                Word64
replayGamma <- Get Word64
forall t. Binary t => Get t
get
                if Word64 -> Bool
forall a. Integral a => a -> Bool
odd Word64
replayGamma
                  then ReplaySeed -> Get ReplaySeed
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ReplaySeed -> Get ReplaySeed) -> ReplaySeed -> Get ReplaySeed
forall a b. (a -> b) -> a -> b
$ ReplaySeed{Word64
replaySeed :: Word64
replaySeed :: Word64
replaySeed, Word64
replayGamma :: Word64
replayGamma :: Word64
replayGamma}
                  else String -> Get ReplaySeed
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get ReplaySeed) -> String -> Get ReplaySeed
forall a b. (a -> b) -> a -> b
$ String
"ReplaySeed: expected odd gamma for splitmix"
        Word8
n -> String -> Get ReplaySeed
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get ReplaySeed) -> String -> Get ReplaySeed
forall a b. (a -> b) -> a -> b
$ String
"ReplaySeed: invalid tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word8 -> String
forall a. Show a => a -> String
show Word8
n

instance Show ReplaySeed where
  show :: ReplaySeed -> String
show = ByteString -> String
Lazy.Char8.unpack (ByteString -> String)
-> (ReplaySeed -> ByteString) -> ReplaySeed -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.Base16.encode (ByteString -> ByteString)
-> (ReplaySeed -> ByteString) -> ReplaySeed -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReplaySeed -> ByteString
forall a. Binary a => a -> ByteString
encode

instance IsString ReplaySeed where
  fromString :: String -> ReplaySeed
fromString = Either String ReplaySeed -> ReplaySeed
aux (Either String ReplaySeed -> ReplaySeed)
-> (String -> Either String ReplaySeed) -> String -> ReplaySeed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String ReplaySeed
parseReplaySeed
    where
      aux :: Either String ReplaySeed -> ReplaySeed
      aux :: Either String ReplaySeed -> ReplaySeed
aux (Left  String
err)  = String -> ReplaySeed
forall a. HasCallStack => String -> a
error (String -> ReplaySeed) -> String -> ReplaySeed
forall a b. (a -> b) -> a -> b
$ String
"ReplaySeed: invalid seed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
      aux (Right ReplaySeed
seed) = ReplaySeed
seed

-- | Parse t'ReplaySeed'
--
-- Returns 'Left' an error message if parsing failed.
parseReplaySeed :: String -> Either String ReplaySeed
parseReplaySeed :: String -> Either String ReplaySeed
parseReplaySeed String
str = do
    ByteString
raw <- case ByteString -> Either String ByteString
Lazy.Base16.decode (String -> ByteString
Lazy.Char8.pack String
str) of
             Left String
err -> String -> Either String ByteString
forall a b. a -> Either a b
Left String
err
             Right ByteString
x  -> ByteString -> Either String ByteString
forall a b. b -> Either a b
Right ByteString
x
    case ByteString
-> Either
     (ByteString, ByteOffset, String)
     (ByteString, ByteOffset, ReplaySeed)
forall a.
Binary a =>
ByteString
-> Either
     (ByteString, ByteOffset, String) (ByteString, ByteOffset, a)
decodeOrFail ByteString
raw of
      Left  (ByteString
_, ByteOffset
_, String
err) -> String -> Either String ReplaySeed
forall a b. a -> Either a b
Left String
err
      Right (ByteString
_, ByteOffset
_, ReplaySeed
x)   -> ReplaySeed -> Either String ReplaySeed
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return ReplaySeed
x