-- |
-- Module      :  Cryptol.Testing.Random
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module generates random values for Cryptol types.

{-# 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

{- | Apply a testable value to some randomly-generated arguments.
     Returns @Nothing@ if the function returned @True@, or
     @Just counterexample@ if it returned @False@.

    Please note that this function assumes that the generators match
    the supplied value, otherwise we'll panic.
 -}
runOneTest :: RandomGen g
        => Value   -- ^ Function under test
        -> [Gen g Concrete] -- ^ Argument generators
        -> Integer -- ^ Size
        -> 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    -- ^ Function to be used to calculate tests
           -> [Gen g Concrete] -- ^ Argument generators
           -> Integer -- ^ Size
           -> g -- ^ Initial random state
           -> IO ([Value], Value, g) -- ^ Arguments, result, and new random state
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 -- ^ The random generator state
         -> [Gen g Concrete] -- ^ Generators for the function arguments
         -> Value -- ^ The function itself
         -> Int -- ^ How many tests?
         -> IO [([Value], Value)] -- ^ A list of pairs of random arguments and computed outputs
                                       --   as well as the new state of the RNG
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

-- | Return a collection of random tests.
returnTests' :: RandomGen g
         => g -- ^ The random generator state
         -> [Gen g Concrete] -- ^ Generators for the function arguments
         -> Value -- ^ The function itself
         -> Int -- ^ How many tests?
         -> IO ([([Value], Value)], g) -- ^ A list of pairs of random arguments and computed outputs
                                       --   as well as the new state of the RNG
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)

{- | Given a (function) type, compute generators for the function's
arguments. -}
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)
  #-}

{- | A generator for values of the given type.  This fails if we are
given a type that lacks a suitable random value generator. -}
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 #-}

-- | Generate a random bit value.
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 #-}

-- | Generate a random integer value. The size parameter is assumed to
-- vary between 1 and 100, and we use it to generate smaller numbers
-- first.
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 #-}

-- | Generate a random word of the given length (i.e., a value of type @[w]@)
-- The size parameter is assumed to vary between 1 and 100, and we use
-- it to generate smaller numbers first.
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 #-}

-- | Generate a random infinite stream value.
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 #-}

{- | Generate a random sequence.  This should be used for sequences
other than bits.  For sequences of bits use "randomWord". -}
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 #-}

-- | Generate a random tuple value.
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 #-}

-- | Generate a random record value.
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 {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  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'  -- about 10% of the time
           | 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'     -- about 40%
           | Bool
otherwise     -> Integer -> g -> (SEval sym (GenValue sym), g)
genNormal (forall a. Integral a => a -> Integer
toInteger Integer
sz) g
g'  -- remaining ~50%

  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

    -- generates floats uniformly chosen from among all bitpatterns
    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)

    -- generates floats corresponding to subnormal values.  These are
    -- values with 0 biased exponent and nonzero mantissa.
    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)

    -- generates floats where the exponent and mantissa are scaled by the size
    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)


-- | A test result is either a pass, a failure due to evaluating to
-- @False@, or a failure due to an exception raised during evaluation
data TestResult
  = Pass
  | FailFalse [Value]
  | FailError EvalErrorEx [Value]

isPass :: TestResult -> Bool
isPass :: TestResult -> Bool
isPass TestResult
Pass = Bool
True
isPass TestResult
_    = Bool
False

-- | Apply a testable value to some arguments.
-- Note that this function assumes that the values come from a call to
-- `testableType` (i.e., things are type-correct). We run in the IO
-- monad in order to catch any @EvalError@s.
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

{- | Given a (function) type, compute data necessary for
     random or exhaustive testing.

     The first returned component is a count of the number of
     possible input test vectors, if the input types are finite.
     The second component is a list of all the types of the function
     inputs.  The third component is a list of all input test vectors
     for exhaustive testing.  This will be empty unless the
     input types are finite.  The final argument is a list of generators
     for the inputs of the function.

     This function will return @Nothing@ if the input type does not
     eventually return @Bit@, or if we cannot compute a generator
     for one of the inputs.
-}
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

{- | Given a fully-evaluated type, try to compute the number of values in it.
Returns `Nothing` for infinite types, user-defined types, polymorphic types,
and, currently, function spaces.  Of course, we can easily compute the
sizes of function spaces, but we can't easily enumerate their inhabitants. -}
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)

{- | Returns all the values in a type.  Returns an empty list of values,
for types where 'typeSize' returned 'Nothing'. -}
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)

--------------------------------------------------------------------------------
-- Driver function

exhaustiveTests :: MonadIO m =>
  (Integer -> m ()) {- ^ progress callback -} ->
  Value {- ^ function under test -} ->
  [[Value]] {- ^ exhaustive set of test values -} ->
  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 ()) {- ^ progress callback -} ->
  Integer {- ^ Maximum number of tests to run -} ->
  Value {- ^ function under test -} ->
  [Gen g Concrete] {- ^ input value generators -} ->
  g {- ^ Inital random generator -} ->
  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 ()) {- ^ progress callback -} ->
  Integer {- ^ Maximum number of tests to run -} ->
  Value {- ^ function under test -} ->
  [Gen g Concrete] {- ^ input value generators -} ->
  g {- ^ Inital random generator -} ->
  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)