-- |
-- 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 RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
module Cryptol.Testing.Random
( Gen
, randomValue
, dumpableType
, testableType
, TestReport(..)
, TestResult(..)
, isPass
, returnTests
, exhaustiveTests
, randomTests
) where

import qualified Control.Exception as X
import Control.Monad          (join, liftM2)
import Control.Monad.IO.Class (MonadIO(..))
import Data.Ratio             ((%))
import Data.List              (unfoldr, genericTake, genericIndex, genericReplicate)
import qualified Data.Sequence as Seq

import System.Random          (RandomGen, split, random, randomR)

import Cryptol.Backend        (Backend(..), SRational(..))
import Cryptol.Backend.Monad  (runEval,Eval,EvalError(..))
import Cryptol.Backend.Concrete

import Cryptol.Eval.Type      (TValue(..))
import Cryptol.Eval.Value     (GenValue(..),SeqMap(..), WordValue(..),
                               ppValue, defaultPPOpts, finiteSeqMap)
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 :: 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) = ((Integer -> g -> (Eval Value, g))
 -> ([Eval Value], g) -> ([Eval Value], g))
-> ([Eval Value], g)
-> [Integer -> g -> (Eval Value, g)]
-> ([Eval Value], g)
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) [Integer -> g -> (Eval Value, g)]
[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
aEval Value -> [Eval Value] -> [Eval Value]
forall a. a -> [a] -> [a]
:[Eval Value]
as, g
g')
  [Value]
args' <- Eval [Value] -> IO [Value]
forall a. Eval a -> IO a
runEval ([Eval Value] -> Eval [Value]
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'
  (TestResult, g) -> IO (TestResult, g)
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 :: 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) = ((Integer -> g -> (Eval Value, g))
 -> ([Eval Value], g) -> ([Eval Value], g))
-> ([Eval Value], g)
-> [Integer -> g -> (Eval Value, g)]
-> ([Eval Value], g)
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) [Integer -> g -> (Eval Value, g)]
[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
aEval Value -> [Eval Value] -> [Eval Value]
forall a. a -> [a] -> [a]
:[Eval Value]
as, g
g')
     [Value]
args' <- Eval [Value] -> IO [Value]
forall a. Eval a -> IO a
runEval ([Eval Value] -> Eval [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Eval Value]
args)
     Value
result <- Eval Value -> IO Value
forall a. Eval a -> IO a
runEval (Value -> [Value] -> SEval Concrete Value
forall sym.
Monad (SEval sym) =>
GenValue sym -> [GenValue sym] -> SEval sym (GenValue sym)
go Value
fun [Value]
args')
     ([Value], Value, g) -> IO ([Value], Value, g)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Value]
args', Value
result, g
g1)
   where
     go :: GenValue sym -> [GenValue sym] -> SEval sym (GenValue sym)
go (VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f) (GenValue sym
v : [GenValue sym]
vs) = SEval sym (SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (GenValue sym -> [GenValue sym] -> SEval sym (GenValue sym)
go (GenValue sym -> [GenValue sym] -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym ([GenValue sym] -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v)) SEval sym ([GenValue sym] -> SEval sym (GenValue sym))
-> SEval sym [GenValue sym] -> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [GenValue sym] -> SEval sym [GenValue sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [GenValue sym]
vs)
     go (VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_) [] = String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Not enough arguments to function while generating tests"]
     go GenValue sym
_ (GenValue sym
_ : [GenValue sym]
_) = String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Too many arguments to function while generating tests"]
     go GenValue sym
v [] = GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
v


-- | 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)] -- ^ A list of pairs of random arguments and computed outputs
returnTests :: g -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
returnTests g
g [Gen g Concrete]
gens Value
fun Int
num = [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO [([Value], Value)]
go [Integer -> g -> (Eval Value, g)]
[Gen g Concrete]
gens g
g Int
0
  where
    go :: [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO [([Value], Value)]
go [Integer -> g -> (Eval Value, g)]
args g
g0 Int
n
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
num = [([Value], Value)] -> IO [([Value], Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      | Bool
otherwise =
        do let sz :: Integer
sz = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Int -> Int
forall a. Integral a => a -> a -> a
div (Int
100 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)) Int
num)
           ([Value]
inputs, Value
output, g
g1) <- Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
forall g.
RandomGen g =>
Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
returnOneTest Value
fun [Integer -> g -> (Eval Value, g)]
[Gen g Concrete]
args Integer
sz g
g0
           [([Value], Value)]
more <- [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO [([Value], Value)]
go [Integer -> g -> (Eval Value, g)]
args g
g1 (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
           [([Value], Value)] -> IO [([Value], Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value]
inputs, Value
output) ([Value], Value) -> [([Value], Value)] -> [([Value], Value)]
forall a. a -> [a] -> [a]
: [([Value], Value)]
more)

{- | Given a (function) type, compute generators for the function's
arguments. -}
dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
dumpableType :: TValue -> Maybe [Gen g Concrete]
dumpableType (TVFun TValue
t1 TValue
t2) =
   do Integer -> g -> (Eval Value, g)
g  <- Concrete -> TValue -> Maybe (Gen g Concrete)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue Concrete
Concrete TValue
t1
      [Integer -> g -> (Eval Value, g)]
as <- TValue -> Maybe [Gen g Concrete]
forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
dumpableType TValue
t2
      [Integer -> g -> (Eval Value, g)]
-> Maybe [Integer -> g -> (Eval Value, g)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> g -> (Eval Value, g)
g (Integer -> g -> (Eval Value, g))
-> [Integer -> g -> (Eval Value, g)]
-> [Integer -> g -> (Eval Value, g)]
forall a. a -> [a] -> [a]
: [Integer -> g -> (Eval Value, g)]
as)
dumpableType TValue
ty =
   do (_ :: Gen g Concrete) <- Concrete -> TValue -> Maybe (Gen g Concrete)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue Concrete
Concrete TValue
ty
      [Integer -> g -> (Eval Value, g)]
-> Maybe [Integer -> g -> (Eval Value, g)]
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 :: sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
ty =
  case TValue
ty of
    TValue
TVBit         -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Gen g sym
forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit sym
sym)
    TValue
TVInteger     -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Gen g sym
forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomInteger sym
sym)
    TValue
TVRational    -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Gen g sym
forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomRational sym
sym)
    TVIntMod Integer
m    -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Integer -> Gen g sym
forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> Gen g sym
randomIntMod sym
sym Integer
m)
    TVFloat Integer
e Integer
p   -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Integer -> Integer -> Gen g sym
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 -> Gen g sym -> Maybe (Gen g sym)
forall a. a -> Maybe a
Just (sym -> Integer -> Gen g sym
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 <- sym -> TValue -> Maybe (Gen g sym)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
el
            Gen g sym -> Maybe (Gen g sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Gen g sym -> Gen g sym
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 <- sym -> TValue -> Maybe (Gen g sym)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
el
            Gen g sym -> Maybe (Gen g sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Gen g sym -> Gen g sym
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 <- (TValue -> Maybe (Gen g sym)) -> [TValue] -> Maybe [Gen g sym]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym -> TValue -> Maybe (Gen g sym)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym) [TValue]
els
            Gen g sym -> Maybe (Gen g sym)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Gen g sym] -> Gen g sym
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 <- (TValue -> Maybe (Gen g sym))
-> RecordMap Ident TValue -> Maybe (RecordMap Ident (Gen g sym))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> TValue -> Maybe (Gen g sym)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym) RecordMap Ident TValue
fs
            Gen g sym -> Maybe (Gen g sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident (Gen g sym) -> Gen g sym
forall sym g.
(Backend sym, RandomGen g) =>
RecordMap Ident (Gen g sym) -> Gen g sym
randomRecord RecordMap Ident (Gen g sym)
gs)

    TVArray{} -> Maybe (Gen g sym)
forall a. Maybe a
Nothing
    TVFun{} -> Maybe (Gen g sym)
forall a. Maybe a
Nothing
    TVAbstract{} -> Maybe (Gen g sym)
forall a. Maybe a
Nothing

{-# INLINE randomBit #-}

-- | Generate a random bit value.
randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit :: sym -> Gen g sym
randomBit sym
sym Integer
_ g
g =
  let (Bool
b,g
g1) = g -> (Bool, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
  in (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (sym -> Bool -> SBit sym
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 :: Int -> Int -> g -> (Int, g)
randomSize Int
k Int
n g
g
  | Int
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = (Int
n, g
g')
  | Bool
otherwise = Int -> Int -> g -> (Int, g)
forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
k (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) g
g'
  where (Int
p, g
g') = (Int, Int) -> g -> (Int, 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 :: sym -> Gen g sym
randomInteger sym
sym Integer
w g
g =
  let (Int
n, g
g1) = if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
100 then (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w, g
g) else Int -> Int -> g -> (Int, g)
forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
8 Int
100 g
g
      (Integer
i, g
g2) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (- Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n, Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n) g
g1
  in (SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> SEval sym (SInteger sym)
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 :: sym -> Integer -> Gen g sym
randomIntMod sym
sym Integer
modulus Integer
_ g
g =
  let (Integer
i, g
g') = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
modulusInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) g
g
  in (SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> SEval sym (SInteger sym)
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 :: sym -> Gen g sym
randomRational sym
sym Integer
w g
g =
  let (Int
sz, g
g1) = if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
100 then (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w, g
g) else Int -> Int -> g -> (Int, g)
forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
8 Int
100 g
g
      (Integer
n, g
g2) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (- Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz, Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz) g
g1
      (Integer
d, g
g3) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR ( Integer
1, Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
sz) g
g2
   in (do SInteger sym
n' <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
n
          SInteger sym
d' <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
d
          GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SInteger sym -> SInteger sym -> SRational sym
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 :: sym -> Integer -> Gen g sym
randomWord sym
sym Integer
w Integer
_sz g
g =
   let (Integer
val, g
g1) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0,Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) g
g
   in (GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SEval sym (SWord sym)
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 :: Gen g sym -> Gen g sym
randomStream Gen g sym
mkElem Integer
sz g
g =
  let (g
g1,g
g2) = g -> (g, g)
forall g. RandomGen g => g -> (g, g)
split g
g
  in (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> Integer -> SEval sym (GenValue sym)
forall i a. Integral i => [a] -> i -> a
genericIndex ((g -> Maybe (SEval sym (GenValue sym), g))
-> g -> [SEval sym (GenValue sym)]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr ((SEval sym (GenValue sym), g)
-> Maybe (SEval sym (GenValue sym), g)
forall a. a -> Maybe a
Just ((SEval sym (GenValue sym), g)
 -> Maybe (SEval sym (GenValue sym), g))
-> (g -> (SEval sym (GenValue sym), g))
-> g
-> Maybe (SEval sym (GenValue sym), g)
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 :: Integer -> Gen g sym -> Gen g sym
randomSequence Integer
w Gen g sym
mkElem Integer
sz g
g0 = do
  let (g
g1,g
g2) = g -> (g, g)
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 SEval sym (GenValue sym)
-> Maybe (SEval sym (GenValue sym), g)
-> Maybe (SEval sym (GenValue sym), g)
seq SEval sym (GenValue sym)
x ((SEval sym (GenValue sym), g)
-> Maybe (SEval sym (GenValue sym), g)
forall a. a -> Maybe a
Just (SEval sym (GenValue sym)
x, g
g'))
  let xs :: Seq (SEval sym (GenValue sym))
xs = [SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym))
forall a. [a] -> Seq a
Seq.fromList ([SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym))
forall a b. (a -> b) -> a -> b
$ Integer -> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
w ([SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)])
-> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> a -> b
$ (g -> Maybe (SEval sym (GenValue sym), g))
-> g -> [SEval sym (GenValue sym)]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr g -> Maybe (SEval sym (GenValue sym), g)
f g
g1
  Seq (SEval sym (GenValue sym))
-> (SEval sym (GenValue sym), g) -> (SEval sym (GenValue sym), g)
seq Seq (SEval sym (GenValue sym))
xs (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
w (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ (Seq (SEval sym (GenValue sym)) -> Int -> SEval sym (GenValue sym)
forall a. Seq a -> Int -> a
Seq.index Seq (SEval sym (GenValue sym))
xs (Int -> SEval sym (GenValue sym))
-> (Integer -> Int) -> Integer -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger), g
g2)

{-# INLINE randomTuple #-}

-- | Generate a random tuple value.
randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym
randomTuple :: [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 = (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ([SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
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 SEval sym (GenValue sym)
-> (SEval sym (GenValue sym), g) -> (SEval sym (GenValue sym), g)
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 SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
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 :: 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) = (g -> Gen g sym -> (g, SEval sym (GenValue sym)))
-> g
-> RecordMap Ident (Gen g sym)
-> (g, RecordMap Ident (SEval sym (GenValue sym)))
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 (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
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 SEval sym (GenValue sym)
-> (g, SEval sym (GenValue sym)) -> (g, SEval sym (GenValue sym))
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 :: sym -> Integer -> Integer -> Gen g sym
randomFloat sym
sym Integer
e Integer
p Integer
w g
g =
  ( SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p (Integer
nu Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
de)
  , g
g3
  )
  where
  -- XXX: we never generat NaN
  -- XXX: Not sure that we need such big integers, we should probably
  -- use `e` and `p` as a guide.
  (Int
n,  g
g1) = if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
100 then (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w, g
g) else Int -> Int -> g -> (Int, g)
forall g. RandomGen g => Int -> Int -> g -> (Int, g)
randomSize Int
8 Int
100 g
g
  (Integer
nu, g
g2) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (- Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n, Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n) g
g1
  (Integer
de, g
g3) = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
1, Integer
256Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n) g
g2





-- | 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 EvalError [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 IO TestResult -> (EvalError -> IO TestResult) -> IO TestResult
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` EvalError -> IO TestResult
handle
  where
    run :: IO TestResult
run = do
      Bool
result <- Eval Bool -> IO Bool
forall a. Eval a -> IO a
runEval (Value -> [Value] -> Eval Bool
go Value
v0 [Value]
vs0)
      if Bool
result
        then TestResult -> IO TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
Pass
        else TestResult -> IO TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Value] -> TestResult
FailFalse [Value]
vs0)
    handle :: EvalError -> IO TestResult
handle EvalError
e = TestResult -> IO TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return (EvalError -> [Value] -> TestResult
FailError EvalError
e [Value]
vs0)

    go :: Value -> [Value] -> Eval Bool
    go :: Value -> [Value] -> Eval Bool
go (VFun SEval Concrete Value -> SEval Concrete Value
f) (Value
v : [Value]
vs) = Eval (Eval Bool) -> Eval Bool
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Value -> [Value] -> Eval Bool
go (Value -> [Value] -> Eval Bool)
-> Eval Value -> Eval ([Value] -> Eval Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval Concrete Value -> SEval Concrete Value
f (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)) Eval ([Value] -> Eval Bool) -> Eval [Value] -> Eval (Eval Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Value] -> Eval [Value]
forall (m :: * -> *) a. Monad m => a -> m a
return [Value]
vs)
    go (VFun SEval Concrete Value -> SEval Concrete Value
_) []       = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Not enough arguments while applying function"
                           []
    go (VBit SBit Concrete
b) []       = Bool -> Eval Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
SBit Concrete
b
    go Value
v [Value]
vs              = do Doc
vdoc    <- Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue Concrete
Concrete PPOpts
defaultPPOpts Value
v
                              [Doc]
vsdocs  <- (Value -> Eval Doc) -> [Value] -> Eval [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue Concrete
Concrete PPOpts
defaultPPOpts) [Value]
vs
                              String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Type error while running test" ([String] -> Eval Bool) -> [String] -> Eval Bool
forall a b. (a -> b) -> a -> b
$
                               [ String
"Function:"
                               , Doc -> String
forall a. Show a => a -> String
show Doc
vdoc
                               , String
"Arguments:"
                               ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
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 :: 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 <- Concrete -> TValue -> Maybe (Gen g Concrete)
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) <- TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
forall g.
RandomGen g =>
TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType TValue
t2
      let tot' :: Maybe Integer
tot' = (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) Maybe Integer
sz Maybe Integer
tot
      let vss' :: [[Value]]
vss' = [ Value
v Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
vs | Value
v <- TValue -> [Value]
typeValues TValue
t1, [Value]
vs <- [[Value]]
vss ]
      (Maybe Integer, [TValue], [[Value]],
 [Integer -> g -> (Eval Value, g)])
-> Maybe
     (Maybe Integer, [TValue], [[Value]],
      [Integer -> g -> (Eval Value, g)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
tot', TValue
t1TValue -> [TValue] -> [TValue]
forall a. a -> [a] -> [a]
:[TValue]
ts, [[Value]]
vss', Integer -> g -> (Eval Value, g)
g(Integer -> g -> (Eval Value, g))
-> [Integer -> g -> (Eval Value, g)]
-> [Integer -> g -> (Eval Value, g)]
forall a. a -> [a] -> [a]
:[Integer -> g -> (Eval Value, g)]
gs)
testableType TValue
TVBit = (Maybe Integer, [TValue], [[Value]],
 [Integer -> g -> (Eval Value, g)])
-> Maybe
     (Maybe Integer, [TValue], [[Value]],
      [Integer -> g -> (Eval Value, g)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1, [], [[]], [])
testableType TValue
_ = Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
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 -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2
  TValue
TVInteger -> Maybe Integer
forall a. Maybe a
Nothing
  TValue
TVRational -> Maybe Integer
forall a. Maybe a
Nothing
  TVIntMod Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
  TVFloat{} -> Maybe Integer
forall a. Maybe a
Nothing -- TODO?
  TVArray{} -> Maybe Integer
forall a. Maybe a
Nothing
  TVStream{} -> Maybe Integer
forall a. Maybe a
Nothing
  TVSeq Integer
n TValue
el -> (Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe Integer
typeSize TValue
el
  TVTuple [TValue]
els -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe Integer) -> [TValue] -> Maybe [Integer]
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 -> RecordMap Ident Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product (RecordMap Ident Integer -> Integer)
-> Maybe (RecordMap Ident Integer) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe Integer)
-> RecordMap Ident TValue -> Maybe (RecordMap Ident Integer)
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{} -> Maybe Integer
forall a. Maybe a
Nothing
  TVAbstract{} -> Maybe Integer
forall a. Maybe a
Nothing

{- | 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      -> [ SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit Bool
SBit Concrete
False, SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit Bool
SBit Concrete
True ]
    TValue
TVInteger  -> []
    TValue
TVRational -> []
    TVIntMod Integer
n -> [ SInteger Concrete -> Value
forall sym. SInteger sym -> GenValue sym
VInteger Integer
SInteger Concrete
x | Integer
x <- [ Integer
0 .. (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) ] ]
    TVFloat{}  -> [] -- TODO?
    TVArray{}  -> []
    TVStream{} -> []
    TVSeq Integer
n TValue
TVBit ->
      [ Integer -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
n (WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord Concrete -> WordValue Concrete
forall sym. SWord sym -> WordValue sym
WordVal (Integer -> Integer -> BV
BV Integer
n Integer
x)))
      | Integer
x <- [ Integer
0 .. Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 ]
      ]
    TVSeq Integer
n TValue
el ->
      [ Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n (Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
xs))
      | [Value]
xs <- [[Value]] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> [Value] -> [[Value]]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (TValue -> [Value]
typeValues TValue
el))
      ]
    TVTuple [TValue]
ts ->
      [ [SEval Concrete Value] -> Value
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
xs)
      | [Value]
xs <- [[Value]] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((TValue -> [Value]) -> [TValue] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> [Value]
typeValues [TValue]
ts)
      ]
    TVRec RecordMap Ident TValue
fs ->
      [ RecordMap Ident (SEval Concrete Value) -> Value
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord ((Value -> Eval Value)
-> RecordMap Ident Value -> RecordMap Ident (Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure RecordMap Ident Value
xs)
      | RecordMap Ident Value
xs <- (TValue -> [Value])
-> RecordMap Ident TValue -> [RecordMap Ident Value]
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{} -> []

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

data TestReport = TestReport {
    TestReport -> TestResult
reportResult :: TestResult
  , TestReport -> String
reportProp :: String -- ^ The property as entered by the user
  , TestReport -> Integer
reportTestsRun :: Integer
  , TestReport -> Maybe Integer
reportTestsPossible :: Maybe Integer
  }

exhaustiveTests :: MonadIO m =>
  (Integer -> m ()) {- ^ progress callback -} ->
  Value {- ^ function under test -} ->
  [[Value]] {- ^ exhaustive set of test values -} ->
  m (TestResult, Integer)
exhaustiveTests :: (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 [] = (TestResult, Integer) -> m (TestResult, Integer)
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 <- IO TestResult -> m TestResult
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
testNumInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) [[Value]]
vss
         TestResult
failure -> (TestResult, Integer) -> m (TestResult, Integer)
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 :: (Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m (TestResult, Integer)
randomTests Integer -> m ()
ppProgress Integer
maxTests Value
val [Gen g Concrete]
gens = Integer -> g -> m (TestResult, Integer)
go Integer
0
  where
  go :: Integer -> g -> m (TestResult, Integer)
go !Integer
testNum g
g
    | Integer
testNum Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
maxTests = (TestResult, Integer) -> m (TestResult, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
Pass, Integer
testNum)
    | Bool
otherwise =
      do Integer -> m ()
ppProgress Integer
testNum
         let sz' :: Integer
sz' = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
100 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
testNum)) Integer
maxTests
         (TestResult
res, g
g') <- IO (TestResult, g) -> m (TestResult, g)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
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)
go (Integer
testNumInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) g
g'
           TestResult
failure -> (TestResult, Integer) -> m (TestResult, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
failure, Integer
testNum)