module Cryptol.Testing.Random where
import Cryptol.Eval.Value (BV(..),Value,GenValue(..))
import qualified Cryptol.Testing.Concrete as Conc
import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser)
import Cryptol.Utils.Ident (Ident)
import Control.Monad (forM)
import Data.List (unfoldr, genericTake)
import System.Random (RandomGen, split, random, randomR)
type Gen g = Integer -> g -> (Value, g)
runOneTest :: RandomGen g
=> Value
-> [Gen g]
-> Integer
-> g
-> IO (Conc.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 <- Conc.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 => [(Ident, 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