{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
module Cryptol.Testing.Random
( Gen
, randomValue
, dumpableType
, testableType
, TestResult(..)
, isPass
, returnTests
, returnTests'
, exhaustiveTests
, randomTests
, randomTests'
) where
import qualified Control.Exception as X
import Control.Monad (liftM2)
import Control.Monad.IO.Class (MonadIO(..))
import Data.Bits
import Data.List (unfoldr, genericTake, genericIndex, genericReplicate)
import qualified Data.Sequence as Seq
import System.Random.TF.Gen
import System.Random.TF.Instances
import Cryptol.Backend (Backend(..), SRational(..))
import Cryptol.Backend.FloatHelpers (floatFromBits)
import Cryptol.Backend.Monad (runEval,Eval,EvalErrorEx(..))
import Cryptol.Backend.Concrete
import Cryptol.Backend.SeqMap (indexSeqMap, finiteSeqMap)
import Cryptol.Backend.WordValue (wordVal)
import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Value (GenValue(..), ppValue, defaultPPOpts, fromVFun)
import Cryptol.TypeCheck.Solver.InfNat (widthInteger)
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.RecordMap
type Gen g x = Integer -> g -> (SEval x (GenValue x), g)
type Value = GenValue Concrete
runOneTest :: RandomGen g
=> Value
-> [Gen g Concrete]
-> Integer
-> g
-> IO (TestResult, g)
runOneTest :: forall g.
RandomGen g =>
Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
runOneTest Value
fun [Gen g Concrete]
argGens Integer
sz g
g0 = do
let ([Eval Value]
args, g
g1) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Integer -> g -> (Eval Value, g))
-> ([Eval Value], g) -> ([Eval Value], g)
mkArg ([], g
g0) [Gen g Concrete]
argGens
mkArg :: (Integer -> g -> (Eval Value, g))
-> ([Eval Value], g) -> ([Eval Value], g)
mkArg Integer -> g -> (Eval Value, g)
argGen ([Eval Value]
as, g
g) = let (Eval Value
a, g
g') = Integer -> g -> (Eval Value, g)
argGen Integer
sz g
g in (Eval Value
aforall a. a -> [a] -> [a]
:[Eval Value]
as, g
g')
[Value]
args' <- forall a. CallStack -> Eval a -> IO a
runEval forall a. Monoid a => a
mempty (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Eval Value]
args)
TestResult
result <- Value -> [Value] -> IO TestResult
evalTest Value
fun [Value]
args'
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
result, g
g1)
returnOneTest :: RandomGen g
=> Value
-> [Gen g Concrete]
-> Integer
-> g
-> IO ([Value], Value, g)
returnOneTest :: forall g.
RandomGen g =>
Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
returnOneTest Value
fun [Gen g Concrete]
argGens Integer
sz g
g0 =
do let ([Eval Value]
args, g
g1) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Integer -> g -> (Eval Value, g))
-> ([Eval Value], g) -> ([Eval Value], g)
mkArg ([], g
g0) [Gen g Concrete]
argGens
mkArg :: (Integer -> g -> (Eval Value, g))
-> ([Eval Value], g) -> ([Eval Value], g)
mkArg Integer -> g -> (Eval Value, g)
argGen ([Eval Value]
as, g
g) = let (Eval Value
a, g
g') = Integer -> g -> (Eval Value, g)
argGen Integer
sz g
g in (Eval Value
aforall a. a -> [a] -> [a]
:[Eval Value]
as, g
g')
[Value]
args' <- forall a. CallStack -> Eval a -> IO a
runEval forall a. Monoid a => a
mempty (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Eval Value]
args)
Value
result <- forall a. CallStack -> Eval a -> IO a
runEval forall a. Monoid a => a
mempty (Value -> [Value] -> Eval Value
go Value
fun [Value]
args')
forall (m :: * -> *) a. Monad m => a -> m a
return ([Value]
args', Value
result, g
g1)
where
go :: Value -> [Value] -> Eval Value
go f :: Value
f@VFun{} (Value
v : [Value]
vs) =
do Value
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun Concrete
Concrete Value
f (forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)
Value -> [Value] -> Eval Value
go Value
f' [Value]
vs
go VFun{} [] = forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Not enough arguments to function while generating tests"]
go Value
_ (Value
_ : [Value]
_) = forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Too many arguments to function while generating tests"]
go Value
v [] = forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
returnTests :: RandomGen g
=> g
-> [Gen g Concrete]
-> Value
-> Int
-> IO [([Value], Value)]
returnTests :: forall g.
RandomGen g =>
g -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
returnTests g
g [Gen g Concrete]
gens Value
fun Int
num = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall g.
RandomGen g =>
g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
returnTests' g
g [Gen g Concrete]
gens Value
fun Int
num
returnTests' :: RandomGen g
=> g
-> [Gen g Concrete]
-> Value
-> Int
-> IO ([([Value], Value)], g)
returnTests' :: forall g.
RandomGen g =>
g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
returnTests' g
g [Gen g Concrete]
gens Value
fun Int
num = [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO ([([Value], Value)], g)
go [Gen g Concrete]
gens g
g Int
0
where
go :: [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO ([([Value], Value)], g)
go [Integer -> g -> (Eval Value, g)]
args g
g0 Int
n
| Int
n forall a. Ord a => a -> a -> Bool
>= Int
num = forall (m :: * -> *) a. Monad m => a -> m a
return ([], g
g0)
| Bool
otherwise =
do let sz :: Integer
sz = forall a. Integral a => a -> Integer
toInteger (forall a. Integral a => a -> a -> a
div (Int
100 forall a. Num a => a -> a -> a
* (Int
1 forall a. Num a => a -> a -> a
+ Int
n)) Int
num)
([Value]
inputs, Value
output, g
g1) <- forall g.
RandomGen g =>
Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
returnOneTest Value
fun [Integer -> g -> (Eval Value, g)]
args Integer
sz g
g0
([([Value], Value)]
more, g
g2) <- [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO ([([Value], Value)], g)
go [Integer -> g -> (Eval Value, g)]
args g
g1 (Int
n forall a. Num a => a -> a -> a
+ Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value]
inputs, Value
output) forall a. a -> [a] -> [a]
: [([Value], Value)]
more, g
g2)
dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
dumpableType (TVFun TValue
t1 TValue
t2) =
do Integer -> g -> (Eval Value, g)
g <- forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue Concrete
Concrete TValue
t1
[Integer -> g -> (Eval Value, g)]
as <- forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
dumpableType TValue
t2
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> g -> (Eval Value, g)
g forall a. a -> [a] -> [a]
: [Integer -> g -> (Eval Value, g)]
as)
dumpableType TValue
ty =
do (Gen g Concrete
_ :: Gen g Concrete) <- forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue Concrete
Concrete TValue
ty
forall (m :: * -> *) a. Monad m => a -> m a
return []
{-# SPECIALIZE randomValue ::
RandomGen g => Concrete -> TValue -> Maybe (Gen g Concrete)
#-}
randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym)
randomValue :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
ty =
case TValue
ty of
TValue
TVBit -> forall a. a -> Maybe a
Just (forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit sym
sym)
TValue
TVInteger -> forall a. a -> Maybe a
Just (forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomInteger sym
sym)
TValue
TVRational -> forall a. a -> Maybe a
Just (forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomRational sym
sym)
TVIntMod Integer
m -> forall a. a -> Maybe a
Just (forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Gen g sym
randomIntMod sym
sym Integer
m)
TVFloat Integer
e Integer
p -> forall a. a -> Maybe a
Just (forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Integer -> Gen g sym
randomFloat sym
sym Integer
e Integer
p)
TVSeq Integer
n TValue
TVBit -> forall a. a -> Maybe a
Just (forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Gen g sym
randomWord sym
sym Integer
n)
TVSeq Integer
n TValue
el ->
do Gen g sym
mk <- forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
el
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym g.
(Backend sym, RandomGen g) =>
Integer -> Gen g sym -> Gen g sym
randomSequence Integer
n Gen g sym
mk)
TVStream TValue
el ->
do Gen g sym
mk <- forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
el
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym g. (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
randomStream Gen g sym
mk)
TVTuple [TValue]
els ->
do [Gen g sym]
mks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym) [TValue]
els
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym g.
(Backend sym, RandomGen g) =>
[Gen g sym] -> Gen g sym
randomTuple [Gen g sym]
mks)
TVRec RecordMap Ident TValue
fs ->
do RecordMap Ident (Gen g sym)
gs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym) RecordMap Ident TValue
fs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym g.
(Backend sym, RandomGen g) =>
RecordMap Ident (Gen g sym) -> Gen g sym
randomRecord RecordMap Ident (Gen g sym)
gs)
TVNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident TValue
fs ->
do RecordMap Ident (Gen g sym)
gs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym) RecordMap Ident TValue
fs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym g.
(Backend sym, RandomGen g) =>
RecordMap Ident (Gen g sym) -> Gen g sym
randomRecord RecordMap Ident (Gen g sym)
gs)
TVArray{} -> forall a. Maybe a
Nothing
TVFun{} -> forall a. Maybe a
Nothing
TVAbstract{} -> forall a. Maybe a
Nothing
{-# INLINE randomBit #-}
randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit sym
sym Integer
_ g
g =
let (Bool
b,g
g1) = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
in (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SBit sym -> GenValue sym
VBit (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
b)), g
g1)
{-# INLINE randomSize #-}
randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)
randomSize :: forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
k Int
n g
g
| Int
p forall a. Eq a => a -> a -> Bool
== Int
1 = (Int
n, g
g')
| Bool
otherwise = forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
k (Int
n forall a. Num a => a -> a -> a
+ Int
1) g
g'
where (Int
p, g
g') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
k) g
g
{-# INLINE randomInteger #-}
randomInteger :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomInteger :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomInteger sym
sym Integer
w g
g =
let (Int
n, g
g1) = if Integer
w forall a. Ord a => a -> a -> Bool
< Integer
100 then (forall a. Num a => Integer -> a
fromInteger Integer
w, g
g) else forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
8 Int
100 g
g
(Integer
i, g
g2) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (- Integer
256forall a b. (Num a, Integral b) => a -> b -> a
^Int
n, Integer
256forall a b. (Num a, Integral b) => a -> b -> a
^Int
n) g
g1
in (forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i, g
g2)
{-# INLINE randomIntMod #-}
randomIntMod :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
randomIntMod :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Gen g sym
randomIntMod sym
sym Integer
modulus Integer
_ g
g =
let (Integer
i, g
g') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
modulusforall a. Num a => a -> a -> a
-Integer
1) g
g
in (forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i, g
g')
{-# INLINE randomRational #-}
randomRational :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomRational :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomRational sym
sym Integer
w g
g =
let (Int
sz, g
g1) = if Integer
w forall a. Ord a => a -> a -> Bool
< Integer
100 then (forall a. Num a => Integer -> a
fromInteger Integer
w, g
g) else forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
8 Int
100 g
g
(Integer
n, g
g2) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (- Integer
256forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz, Integer
256forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz) g
g1
(Integer
d, g
g3) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR ( Integer
1, Integer
256forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz) g
g2
in (do SInteger sym
n' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
n
SInteger sym
d' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
d
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SRational sym -> GenValue sym
VRational (forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
n' SInteger sym
d'))
, g
g3)
{-# INLINE randomWord #-}
randomWord :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
randomWord :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Gen g sym
randomWord sym
sym Integer
w Integer
_sz g
g =
let (Integer
val, g
g1) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0,Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
wforall a. Num a => a -> a -> a
-Integer
1) g
g
in (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
w Integer
val, g
g1)
{-# INLINE randomStream #-}
randomStream :: (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
randomStream :: forall sym g. (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
randomStream Gen g sym
mkElem Integer
sz g
g =
let (g
g1,g
g2) = forall g. RandomGen g => g -> (g, g)
split g
g
in (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => [a] -> i -> a
genericIndex (forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen g sym
mkElem Integer
sz) g
g1), g
g2)
{-# INLINE randomSequence #-}
randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym
randomSequence :: forall sym g.
(Backend sym, RandomGen g) =>
Integer -> Gen g sym -> Gen g sym
randomSequence Integer
w Gen g sym
mkElem Integer
sz g
g0 = do
let (g
g1,g
g2) = forall g. RandomGen g => g -> (g, g)
split g
g0
let f :: g -> Maybe (SEval sym (GenValue sym), g)
f g
g = let (SEval sym (GenValue sym)
x,g
g') = Gen g sym
mkElem Integer
sz g
g
in seq :: forall a b. a -> b -> b
seq SEval sym (GenValue sym)
x (forall a. a -> Maybe a
Just (SEval sym (GenValue sym)
x, g
g'))
let xs :: Seq (SEval sym (GenValue sym))
xs = forall a. [a] -> Seq a
Seq.fromList forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
w forall a b. (a -> b) -> a -> b
$ forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr g -> Maybe (SEval sym (GenValue sym), g)
f g
g1
let v :: GenValue sym
v = forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall a. Seq a -> Int -> a
Seq.index Seq (SEval sym (GenValue sym))
xs (forall a. Num a => Integer -> a
fromInteger Integer
i)
seq :: forall a b. a -> b -> b
seq Seq (SEval sym (GenValue sym))
xs (forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v, g
g2)
{-# INLINE randomTuple #-}
randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym
randomTuple :: forall sym g.
(Backend sym, RandomGen g) =>
[Gen g sym] -> Gen g sym
randomTuple [Gen g sym]
gens Integer
sz = [SEval sym (GenValue sym)]
-> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
go [] [Gen g sym]
gens
where
go :: [SEval sym (GenValue sym)]
-> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
go [SEval sym (GenValue sym)]
els [] g
g = (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a. [a] -> [a]
reverse [SEval sym (GenValue sym)]
els), g
g)
go [SEval sym (GenValue sym)]
els (Gen g sym
mkElem : [Gen g sym]
more) g
g =
let (SEval sym (GenValue sym)
v, g
g1) = Gen g sym
mkElem Integer
sz g
g
in seq :: forall a b. a -> b -> b
seq SEval sym (GenValue sym)
v ([SEval sym (GenValue sym)]
-> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
go (SEval sym (GenValue sym)
v forall a. a -> [a] -> [a]
: [SEval sym (GenValue sym)]
els) [Gen g sym]
more g
g1)
{-# INLINE randomRecord #-}
randomRecord :: (Backend sym, RandomGen g) => RecordMap Ident (Gen g sym) -> Gen g sym
randomRecord :: forall sym g.
(Backend sym, RandomGen g) =>
RecordMap Ident (Gen g sym) -> Gen g sym
randomRecord RecordMap Ident (Gen g sym)
gens Integer
sz g
g0 =
let (g
g', RecordMap Ident (SEval sym (GenValue sym))
m) = forall a b c k.
(a -> b -> (a, c)) -> a -> RecordMap k b -> (a, RecordMap k c)
recordMapAccum g -> Gen g sym -> (g, SEval sym (GenValue sym))
mk g
g0 RecordMap Ident (Gen g sym)
gens in (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
m, g
g')
where
mk :: g -> Gen g sym -> (g, SEval sym (GenValue sym))
mk g
g Gen g sym
gen =
let (SEval sym (GenValue sym)
v, g
g') = Gen g sym
gen Integer
sz g
g
in seq :: forall a b. a -> b -> b
seq SEval sym (GenValue sym)
v (g
g', SEval sym (GenValue sym)
v)
randomFloat ::
(Backend sym, RandomGen g) =>
sym ->
Integer ->
Integer ->
Gen g sym
randomFloat :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Integer -> Gen g sym
randomFloat sym
sym Integer
e Integer
p Integer
w g
g0 =
let sz :: Integer
sz = forall a. Ord a => a -> a -> a
max Integer
0 (forall a. Ord a => a -> a -> a
min Integer
100 Integer
w)
( Integer
x, g
g') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
10forall a. Num a => a -> a -> a
*(Integer
szforall a. Num a => a -> a -> a
+Integer
1)) g
g0
in if | Integer
x forall a. Ord a => a -> a -> Bool
< Integer
2 -> (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpNaN sym
sym Integer
e Integer
p, g
g')
| Integer
x forall a. Ord a => a -> a -> Bool
< Integer
4 -> (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpPosInf sym
sym Integer
e Integer
p, g
g')
| Integer
x forall a. Ord a => a -> a -> Bool
< Integer
6 -> (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpPosInf sym
sym Integer
e Integer
p), g
g')
| Integer
x forall a. Ord a => a -> a -> Bool
< Integer
8 -> (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
0, g
g')
| Integer
x forall a. Ord a => a -> a -> Bool
< Integer
10 -> (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
0), g
g')
| Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
sz -> g -> (SEval sym (GenValue sym), g)
genSubnormal g
g'
| Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
4forall a. Num a => a -> a -> a
*(Integer
szforall a. Num a => a -> a -> a
+Integer
1) -> g -> (SEval sym (GenValue sym), g)
genBinary g
g'
| Bool
otherwise -> Integer -> g -> (SEval sym (GenValue sym), g)
genNormal (forall a. Integral a => a -> Integer
toInteger Integer
sz) g
g'
where
emax :: Integer
emax = forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger Integer
e) forall a. Num a => a -> a -> a
- Integer
1
smax :: Integer
smax = forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger Integer
p) forall a. Num a => a -> a -> a
- Integer
1
genBinary :: g -> (SEval sym (GenValue sym), g)
genBinary g
g =
let (Integer
v, g
g1) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger (Integer
eforall a. Num a => a -> a -> a
+Integer
p)) forall a. Num a => a -> a -> a
- Integer
1) g
g
in (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
fpFromBits sym
sym Integer
e Integer
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (Integer
eforall a. Num a => a -> a -> a
+Integer
p) Integer
v), g
g1)
genSubnormal :: g -> (SEval sym (GenValue sym), g)
genSubnormal g
g =
let (Bool
sgn, g
g1) = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
(Integer
v, g
g2) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
1, forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger Integer
p) forall a. Num a => a -> a -> a
- Integer
1) g
g1
in (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((if Bool
sgn then forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym else forall (f :: * -> *) a. Applicative f => a -> f a
pure) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
fpFromBits sym
sym Integer
e Integer
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (Integer
eforall a. Num a => a -> a -> a
+Integer
p) Integer
v), g
g2)
genNormal :: Integer -> g -> (SEval sym (GenValue sym), g)
genNormal Integer
sz g
g =
let (Bool
sgn, g
g1) = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
(Integer
ex, g
g2) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR ((Integer
1forall a. Num a => a -> a -> a
-Integer
emax)forall a. Num a => a -> a -> a
*Integer
sz forall a. Integral a => a -> a -> a
`div` Integer
100, (Integer
szforall a. Num a => a -> a -> a
*Integer
emax) forall a. Integral a => a -> a -> a
`div` Integer
100) g
g1
(Integer
mag, g
g3) = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
1, forall a. Ord a => a -> a -> a
max Integer
1 ((Integer
szforall a. Num a => a -> a -> a
*Integer
smax) forall a. Integral a => a -> a -> a
`div` Integer
100)) g
g2
r :: Rational
r = forall a. Num a => Integer -> a
fromInteger Integer
mag forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (Integer
ex forall a. Num a => a -> a -> a
- Integer -> Integer
widthInteger Integer
mag)
r' :: Rational
r' = if Bool
sgn then forall a. Num a => a -> a
negate Rational
r else Rational
r
in (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
r', g
g3)
data TestResult
= Pass
| FailFalse [Value]
| FailError EvalErrorEx [Value]
isPass :: TestResult -> Bool
isPass :: TestResult -> Bool
isPass TestResult
Pass = Bool
True
isPass TestResult
_ = Bool
False
evalTest :: Value -> [Value] -> IO TestResult
evalTest :: Value -> [Value] -> IO TestResult
evalTest Value
v0 [Value]
vs0 = IO TestResult
run forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` EvalErrorEx -> IO TestResult
handle
where
run :: IO TestResult
run = do
Bool
result <- forall a. CallStack -> Eval a -> IO a
runEval forall a. Monoid a => a
mempty (Value -> [Value] -> Eval Bool
go Value
v0 [Value]
vs0)
if Bool
result
then forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
Pass
else forall (m :: * -> *) a. Monad m => a -> m a
return ([Value] -> TestResult
FailFalse [Value]
vs0)
handle :: EvalErrorEx -> IO TestResult
handle EvalErrorEx
e = forall (m :: * -> *) a. Monad m => a -> m a
return (EvalErrorEx -> [Value] -> TestResult
FailError EvalErrorEx
e [Value]
vs0)
go :: Value -> [Value] -> Eval Bool
go :: Value -> [Value] -> Eval Bool
go f :: Value
f@VFun{} (Value
v : [Value]
vs) = do Value
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun Concrete
Concrete Value
f (forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)
Value -> [Value] -> Eval Bool
go Value
f' [Value]
vs
go VFun{} [] = forall a. HasCallStack => String -> [String] -> a
panic String
"Not enough arguments while applying function"
[]
go (VBit SBit Concrete
b) [] = forall (m :: * -> *) a. Monad m => a -> m a
return SBit Concrete
b
go Value
v [Value]
vs = do Doc
vdoc <- forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue Concrete
Concrete PPOpts
defaultPPOpts Value
v
[Doc]
vsdocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue Concrete
Concrete PPOpts
defaultPPOpts) [Value]
vs
forall a. HasCallStack => String -> [String] -> a
panic String
"Type error while running test" forall a b. (a -> b) -> a -> b
$
[ String
"Function:"
, forall a. Show a => a -> String
show Doc
vdoc
, String
"Arguments:"
] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Doc]
vsdocs
testableType :: RandomGen g =>
TValue ->
Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType :: forall g.
RandomGen g =>
TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType (TVFun TValue
t1 TValue
t2) =
do let sz :: Maybe Integer
sz = TValue -> Maybe Integer
typeSize TValue
t1
Integer -> g -> (Eval Value, g)
g <- forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue Concrete
Concrete TValue
t1
(Maybe Integer
tot,[TValue]
ts,[[Value]]
vss,[Integer -> g -> (Eval Value, g)]
gs) <- forall g.
RandomGen g =>
TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType TValue
t2
let tot' :: Maybe Integer
tot' = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Num a => a -> a -> a
(*) Maybe Integer
sz Maybe Integer
tot
let vss' :: [[Value]]
vss' = [ Value
v forall a. a -> [a] -> [a]
: [Value]
vs | Value
v <- TValue -> [Value]
typeValues TValue
t1, [Value]
vs <- [[Value]]
vss ]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
tot', TValue
t1forall a. a -> [a] -> [a]
:[TValue]
ts, [[Value]]
vss', Integer -> g -> (Eval Value, g)
gforall a. a -> [a] -> [a]
:[Integer -> g -> (Eval Value, g)]
gs)
testableType TValue
TVBit = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Integer
1, [], [[]], [])
testableType TValue
_ = forall a. Maybe a
Nothing
typeSize :: TValue -> Maybe Integer
typeSize :: TValue -> Maybe Integer
typeSize TValue
ty = case TValue
ty of
TValue
TVBit -> forall a. a -> Maybe a
Just Integer
2
TValue
TVInteger -> forall a. Maybe a
Nothing
TValue
TVRational -> forall a. Maybe a
Nothing
TVIntMod Integer
n -> forall a. a -> Maybe a
Just Integer
n
TVFloat Integer
e Integer
p -> forall a. a -> Maybe a
Just (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
eforall a. Num a => a -> a -> a
+Integer
p))
TVArray{} -> forall a. Maybe a
Nothing
TVStream{} -> forall a. Maybe a
Nothing
TVSeq Integer
n TValue
el -> (forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe Integer
typeSize TValue
el
TVTuple [TValue]
els -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TValue -> Maybe Integer
typeSize [TValue]
els
TVRec RecordMap Ident TValue
fs -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TValue -> Maybe Integer
typeSize RecordMap Ident TValue
fs
TVFun{} -> forall a. Maybe a
Nothing
TVAbstract{} -> forall a. Maybe a
Nothing
TVNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident TValue
tbody -> TValue -> Maybe Integer
typeSize (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)
typeValues :: TValue -> [Value]
typeValues :: TValue -> [Value]
typeValues TValue
ty =
case TValue
ty of
TValue
TVBit -> [ forall sym. SBit sym -> GenValue sym
VBit Bool
False, forall sym. SBit sym -> GenValue sym
VBit Bool
True ]
TValue
TVInteger -> []
TValue
TVRational -> []
TVIntMod Integer
n -> [ forall sym. SInteger sym -> GenValue sym
VInteger Integer
x | Integer
x <- [ Integer
0 .. (Integer
nforall a. Num a => a -> a -> a
-Integer
1) ] ]
TVFloat Integer
e Integer
p -> [ forall sym. SFloat sym -> GenValue sym
VFloat (Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p Integer
v) | Integer
v <- [Integer
0 .. Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
eforall a. Num a => a -> a -> a
+Integer
p) forall a. Num a => a -> a -> a
- Integer
1] ]
TVArray{} -> []
TVStream{} -> []
TVSeq Integer
n TValue
TVBit ->
[ forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n (forall sym. SWord sym -> WordValue sym
wordVal (Integer -> Integer -> BV
BV Integer
n Integer
x))
| Integer
x <- [ Integer
0 .. Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
n forall a. Num a => a -> a -> a
- Integer
1 ]
]
TVSeq Integer
n TValue
el ->
[ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n (forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap Concrete
Concrete (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
xs))
| [Value]
xs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (TValue -> [Value]
typeValues TValue
el))
]
TVTuple [TValue]
ts ->
[ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
xs)
| [Value]
xs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map TValue -> [Value]
typeValues [TValue]
ts)
]
TVRec RecordMap Ident TValue
fs ->
[ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure RecordMap Ident Value
xs)
| RecordMap Ident Value
xs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TValue -> [Value]
typeValues RecordMap Ident TValue
fs
]
TVFun{} -> []
TVAbstract{} -> []
TVNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident TValue
tbody -> TValue -> [Value]
typeValues (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)
exhaustiveTests :: MonadIO m =>
(Integer -> m ()) ->
Value ->
[[Value]] ->
m (TestResult, Integer)
exhaustiveTests :: forall (m :: * -> *).
MonadIO m =>
(Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
exhaustiveTests Integer -> m ()
ppProgress Value
val = Integer -> [[Value]] -> m (TestResult, Integer)
go Integer
0
where
go :: Integer -> [[Value]] -> m (TestResult, Integer)
go !Integer
testNum [] = forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
Pass, Integer
testNum)
go !Integer
testNum ([Value]
vs:[[Value]]
vss) =
do Integer -> m ()
ppProgress Integer
testNum
TestResult
res <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Value -> [Value] -> IO TestResult
evalTest Value
val [Value]
vs)
case TestResult
res of
TestResult
Pass -> Integer -> [[Value]] -> m (TestResult, Integer)
go (Integer
testNumforall a. Num a => a -> a -> a
+Integer
1) [[Value]]
vss
TestResult
failure -> forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
failure, Integer
testNum)
randomTests :: (MonadIO m, RandomGen g) =>
(Integer -> m ()) ->
Integer ->
Value ->
[Gen g Concrete] ->
g ->
m (TestResult, Integer)
randomTests :: forall (m :: * -> *) g.
(MonadIO m, RandomGen g) =>
(Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m (TestResult, Integer)
randomTests Integer -> m ()
ppProgress Integer
maxTests Value
val [Gen g Concrete]
gens g
g = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) g.
(MonadIO m, RandomGen g) =>
(Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m ((TestResult, Integer), g)
randomTests' Integer -> m ()
ppProgress Integer
maxTests Value
val [Gen g Concrete]
gens g
g
randomTests' :: (MonadIO m, RandomGen g) =>
(Integer -> m ()) ->
Integer ->
Value ->
[Gen g Concrete] ->
g ->
m ((TestResult, Integer), g)
randomTests' :: forall (m :: * -> *) g.
(MonadIO m, RandomGen g) =>
(Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m ((TestResult, Integer), g)
randomTests' Integer -> m ()
ppProgress Integer
maxTests Value
val [Gen g Concrete]
gens = Integer -> g -> m ((TestResult, Integer), g)
go Integer
0
where
go :: Integer -> g -> m ((TestResult, Integer), g)
go !Integer
testNum g
g
| Integer
testNum forall a. Ord a => a -> a -> Bool
>= Integer
maxTests = forall (m :: * -> *) a. Monad m => a -> m a
return ((TestResult
Pass, Integer
testNum), g
g)
| Bool
otherwise =
do Integer -> m ()
ppProgress Integer
testNum
let sz' :: Integer
sz' = forall a. Integral a => a -> a -> a
div (Integer
100 forall a. Num a => a -> a -> a
* (Integer
1 forall a. Num a => a -> a -> a
+ Integer
testNum)) Integer
maxTests
(TestResult
res, g
g') <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall g.
RandomGen g =>
Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
runOneTest Value
val [Gen g Concrete]
gens Integer
sz' g
g)
case TestResult
res of
TestResult
Pass -> Integer -> g -> m ((TestResult, Integer), g)
go (Integer
testNumforall a. Num a => a -> a -> a
+Integer
1) g
g'
TestResult
failure -> forall (m :: * -> *) a. Monad m => a -> m a
return ((TestResult
failure, Integer
testNum), g
g)