module Cryptol.Testing.Random where
import Cryptol.Eval.Value (BV(..),Value,GenValue(..))
import qualified Cryptol.Testing.Eval as Eval
import Cryptol.TypeCheck.AST (Name,Type(..),TCon(..),TC(..),tNoUser)
import Control.Monad (forM)
import Data.List (unfoldr, genericTake)
import System.Random (RandomGen, split, random, randomR)
type Gen g = Int -> g -> (Value, g)
runOneTest :: RandomGen g
=> Value
-> [Gen g]
-> Int
-> g
-> IO (Eval.TestResult, g)
runOneTest fun argGens sz g0 = do
let (args, g1) = foldr mkArg ([], g0) argGens
mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
result <- Eval.runOneTest fun args
return (result, g1)
testableType :: RandomGen g => Type -> Maybe [Gen g]
testableType ty =
case tNoUser ty of
TCon (TC TCFun) [t1,t2] ->
do g <- randomValue t1
as <- testableType t2
return (g : as)
TCon (TC TCBit) [] -> return []
_ -> Nothing
randomValue :: RandomGen g => Type -> Maybe (Gen g)
randomValue ty =
case ty of
TCon tc ts ->
case (tc, map tNoUser ts) of
(TC TCBit, []) -> Just randomBit
(TC TCSeq, [TCon (TC TCInf) [], el]) ->
do mk <- randomValue el
return (randomStream mk)
(TC TCSeq, [TCon (TC (TCNum n)) [], TCon (TC TCBit) []]) ->
return (randomWord n)
(TC TCSeq, [TCon (TC (TCNum n)) [], el]) ->
do mk <- randomValue el
return (randomSequence n mk)
(TC (TCTuple _), els) ->
do mks <- mapM randomValue els
return (randomTuple mks)
_ -> Nothing
TVar _ -> Nothing
TUser _ _ t -> randomValue t
TRec fs -> do gs <- forM fs $ \(l,t) -> do g <- randomValue t
return (l,g)
return (randomRecord gs)
randomBit :: RandomGen g => Gen g
randomBit _ g =
let (b,g1) = random g
in (VBit b, g1)
randomWord :: RandomGen g => Integer -> Gen g
randomWord w _sz g =
let (val, g1) = randomR (0,2^w1) g
in (VWord (BV w val), g1)
randomStream :: RandomGen g => Gen g -> Gen g
randomStream mkElem sz g =
let (g1,g2) = split g
in (VStream (unfoldr (Just . mkElem sz) g1), g2)
randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
randomSequence w mkElem sz g =
let (g1,g2) = split g
in (VSeq False $ genericTake w $ unfoldr (Just . mkElem sz) g1 , g2)
randomTuple :: RandomGen g => [Gen g] -> Gen g
randomTuple gens sz = go [] gens
where
go els [] g = (VTuple (reverse els), g)
go els (mkElem : more) g =
let (v, g1) = mkElem sz g
in go (v : els) more g1
randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g
randomRecord gens sz = go [] gens
where
go els [] g = (VRecord (reverse els), g)
go els ((l,mkElem) : more) g =
let (v, g1) = mkElem sz g
in go ((l,v) : els) more g1