-- |
-- 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, mapAccumL)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Sequence as Seq
import Data.Vector(Vector)
import qualified Data.Vector as Vector

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)
import Cryptol.Backend.WordValue (wordVal)

import Cryptol.Eval(evalEnumCon)
import Cryptol.Eval.Type      ( TValue(..), TNominalTypeValue(..), ConInfo(..)
                              , isNullaryCon )
import Cryptol.Eval.Value     ( GenValue(..), ppValue, defaultPPOpts, fromVFun, mkSeq, unsafeToFinSeq, finSeq)
import Cryptol.TypeCheck.Solver.InfNat (widthInteger, Nat' (..))
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) = ((Integer -> g -> (Eval Value, g))
 -> ([Eval Value], g) -> ([Eval Value], g))
-> ([Eval Value], g)
-> [Integer -> g -> (Eval Value, g)]
-> ([Eval Value], g)
forall a b. (a -> b -> b) -> b -> [a] -> b
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' <- CallStack -> Eval [Value] -> IO [Value]
forall a. CallStack -> Eval a -> IO a
runEval CallStack
forall a. Monoid a => a
mempty ([Eval Value] -> Eval [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Eval Value]
args)
  TestResult
result <- Value -> [Value] -> IO TestResult
evalTest Value
fun [Value]
args'
  (TestResult, g) -> IO (TestResult, g)
forall a. a -> IO a
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) = ((Integer -> g -> (Eval Value, g))
 -> ([Eval Value], g) -> ([Eval Value], g))
-> ([Eval Value], g)
-> [Integer -> g -> (Eval Value, g)]
-> ([Eval Value], g)
forall a b. (a -> b -> b) -> b -> [a] -> b
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' <- CallStack -> Eval [Value] -> IO [Value]
forall a. CallStack -> Eval a -> IO a
runEval CallStack
forall a. Monoid a => a
mempty ([Eval Value] -> Eval [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Eval Value]
args)
     Value
result <- CallStack -> Eval Value -> IO Value
forall a. CallStack -> Eval a -> IO a
runEval CallStack
forall a. Monoid a => a
mempty (Value -> [Value] -> Eval Value
go Value
fun [Value]
args')
     ([Value], Value, g) -> IO ([Value], Value, g)
forall a. a -> IO a
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' <- Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun Concrete
Concrete Value
f (Value -> Eval Value
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)
          Value -> [Value] -> Eval Value
go Value
f' [Value]
vs
     go VFun{} [] = String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Not enough arguments to function while generating tests"]
     go Value
_ (Value
_ : [Value]
_) = String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Testing.Random" [String
"Too many arguments to function while generating tests"]
     go Value
v [] = Value -> Eval Value
forall a. a -> Eval a
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 = ([([Value], Value)], g) -> [([Value], Value)]
forall a b. (a, b) -> a
fst (([([Value], Value)], g) -> [([Value], Value)])
-> IO ([([Value], Value)], g) -> IO [([Value], Value)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
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 [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)], g)
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)], g) -> IO ([([Value], Value)], g)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], g
g0)
      | 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, g
g2) <- [Integer -> g -> (Eval Value, g)]
-> g -> Int -> IO ([([Value], Value)], g)
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)], g) -> IO ([([Value], Value)], g)
forall a. a -> IO a
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, 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  <- 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 a. a -> Maybe a
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
_ :: 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 a. a -> Maybe a
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         -> 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 a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (sym -> Integer -> TValue -> Gen g sym -> Gen g sym
forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> TValue -> Gen g sym -> Gen g sym
randomSequence sym
sym Integer
n TValue
el 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 a. a -> Maybe a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> Maybe a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident 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 a. a -> Maybe a
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)

    TVNominal NominalType
_ [Either Nat' TValue]
_ TNominalTypeValue
nval ->
      case TNominalTypeValue
nval of
        TVStruct 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident 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 a. a -> Maybe a
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)
        TVEnum Vector (ConInfo TValue)
cons -> sym -> Vector (ConInfo (Gen g sym)) -> Gen g sym
forall sym g.
(Backend sym, RandomGen g) =>
sym -> Vector (ConInfo (Gen g sym)) -> Gen g sym
randomCon sym
sym (Vector (ConInfo (Gen g sym)) -> Gen g sym)
-> Maybe (Vector (ConInfo (Gen g sym))) -> Maybe (Gen g sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                          (ConInfo TValue -> Maybe (ConInfo (Gen g sym)))
-> Vector (ConInfo TValue) -> Maybe (Vector (ConInfo (Gen g sym)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ((TValue -> Maybe (Gen g sym))
-> ConInfo TValue -> Maybe (ConInfo (Gen g sym))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ConInfo a -> f (ConInfo b)
traverse (sym -> TValue -> Maybe (Gen g sym)
forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym)) Vector (ConInfo TValue)
cons
        TNominalTypeValue
TVAbstract -> Maybe (Gen g sym)
forall a. Maybe a
Nothing

    TVArray{} -> Maybe (Gen g sym)
forall a. Maybe a
Nothing
    TVFun{} -> 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 :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
randomBit sym
sym Integer
_ g
g =
  let (Bool
b,g
g1) = g -> (Bool, g)
forall g. RandomGen g => g -> (Bool, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
  in (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
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 :: forall g. RandomGen g => 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 g. RandomGen 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 :: 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 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 g. RandomGen g => (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 :: 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') = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen 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 :: 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 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 g. RandomGen g => (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 g. RandomGen g => (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 a. a -> SEval sym a
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 :: 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) = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (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 (WordValue sym -> GenValue sym
forall sym. WordValue sym -> GenValue sym
VWord (WordValue sym -> GenValue sym)
-> (SWord sym -> WordValue sym) -> SWord sym -> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal (SWord sym -> GenValue sym)
-> SEval sym (SWord sym) -> SEval sym (GenValue 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 :: 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) = g -> (g, g)
forall g. RandomGen g => g -> (g, g)
split g
g
  in (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
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) -> GenValue sym
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream (SeqMap sym (GenValue sym) -> GenValue sym)
-> SeqMap sym (GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue 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) => sym -> Integer -> TValue -> Gen g sym -> Gen g sym
randomSequence :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> Integer -> TValue -> Gen g sym -> Gen g sym
randomSequence sym
sym Integer
w TValue
elty 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)
forall a b. a -> b -> b
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
  let v :: SEval sym (GenValue sym)
v  = sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat Integer
w) TValue
elty (SeqMap sym (GenValue sym) -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i -> Seq (SEval sym (GenValue sym)) -> Int -> SEval sym (GenValue sym)
forall a. Seq a -> Int -> a
Seq.index Seq (SEval sym (GenValue sym))
xs (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
  Seq (SEval sym (GenValue sym))
-> (SEval sym (GenValue sym), g) -> (SEval sym (GenValue sym), g)
forall a b. a -> b -> b
seq Seq (SEval sym (GenValue sym))
xs (SEval sym (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 = (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
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)
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 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 :: 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) = (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 a. a -> SEval sym a
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))
forall a b. a -> b -> b
seq SEval sym (GenValue sym)
v (g
g', SEval sym (GenValue sym)
v)

-- | Generate a random constructor value belonging to an enum definition.
--
-- For the purposes of random testing, constructors with zero fields (i.e.,
-- nullary constructors) are less interesting than constructors with at least
-- one field (i.e., non-nullary constructors). For example, given
-- @enum Maybe a = Nothing | Just a@, we would like to generate more @Just@
-- values than @Nothing@ values. To ensure this, we employ the following
-- approach:
--
-- 1. If all constructors are nullary, then randomly pick one of these
--    constructors, where each constructor has an equal chance of being picked.
--
-- 2. If all constructors are non-nullary, then randomly pick one of these
--    constructors, where each constructor has an equal chance of being picked.
--    Then pick random values for each field in the constructor.
--
-- 3. Otherwise, pick a random number between 1 and 100. If the number is less
--    than or equal to 25, then randomly pick a nullary constructor. Otherwise,
--    randomly pick a non-nullary constructor. This biases the results so that
--    nullary constructors are only picked ~25% of the time.
randomCon ::
  forall sym g.
  (Backend sym, RandomGen g) =>
  sym ->
  Vector (ConInfo (Gen g sym)) ->
  Gen g sym
randomCon :: forall sym g.
(Backend sym, RandomGen g) =>
sym -> Vector (ConInfo (Gen g sym)) -> Gen g sym
randomCon sym
sym Vector (ConInfo (Gen g sym))
cons
    -- (1) from the Haddocks
  | [(Int, ConInfo (Gen g sym))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, ConInfo (Gen g sym))]
nonNullaryCons
  = Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
randomCon' Int
nullaryLen [(Int, ConInfo (Gen g sym))]
nullaryCons

    -- (2) from the Haddocks
  | [(Int, ConInfo (Gen g sym))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, ConInfo (Gen g sym))]
nullaryCons
  = Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
randomCon' Int
nonNullaryLen [(Int, ConInfo (Gen g sym))]
nonNullaryCons

    -- (3) from the Haddocks
  | Bool
otherwise
  = \Integer
sz g
g0 ->
      let (Int
x :: Int, g
g1) = (Int, Int) -> g -> (Int, g)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
100) g
g0 in
      if Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
25
         then Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
randomCon' Int
nullaryLen [(Int, ConInfo (Gen g sym))]
nullaryCons Integer
sz g
g1
         else Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
randomCon' Int
nonNullaryLen [(Int, ConInfo (Gen g sym))]
nonNullaryCons Integer
sz g
g1
  where
    (Int
nullaryLen,[(Int, ConInfo (Gen g sym))]
nullaryCons, Int
nonNullaryLen, [(Int, ConInfo (Gen g sym))]
nonNullaryCons) =
       let check :: (a, [(a, ConInfo a)], c, [(a, ConInfo a)])
-> a -> ConInfo a -> (a, [(a, ConInfo a)], c, [(a, ConInfo a)])
check (!a
nullLen,[(a, ConInfo a)]
nullary,!c
nonNullLen,[(a, ConInfo a)]
nonNullary) a
i ConInfo a
con
             | ConInfo a -> Bool
forall a. ConInfo a -> Bool
isNullaryCon ConInfo a
con = ( a
1a -> a -> a
forall a. Num a => a -> a -> a
+a
nullLen,(a
i,ConInfo a
con) (a, ConInfo a) -> [(a, ConInfo a)] -> [(a, ConInfo a)]
forall a. a -> [a] -> [a]
: [(a, ConInfo a)]
nullary
                                  , c
nonNullLen, [(a, ConInfo a)]
nonNullary)
             | Bool
otherwise        = (a
nullLen, [(a, ConInfo a)]
nullary
                                  , c
1c -> c -> c
forall a. Num a => a -> a -> a
+c
nonNullLen, (a
i,ConInfo a
con) (a, ConInfo a) -> [(a, ConInfo a)] -> [(a, ConInfo a)]
forall a. a -> [a] -> [a]
: [(a, ConInfo a)]
nonNullary)
        in ((Int, [(Int, ConInfo (Gen g sym))], Int,
  [(Int, ConInfo (Gen g sym))])
 -> Int
 -> ConInfo (Gen g sym)
 -> (Int, [(Int, ConInfo (Gen g sym))], Int,
     [(Int, ConInfo (Gen g sym))]))
-> (Int, [(Int, ConInfo (Gen g sym))], Int,
    [(Int, ConInfo (Gen g sym))])
-> Vector (ConInfo (Gen g sym))
-> (Int, [(Int, ConInfo (Gen g sym))], Int,
    [(Int, ConInfo (Gen g sym))])
forall a b. (a -> Int -> b -> a) -> a -> Vector b -> a
Vector.ifoldl' (Int, [(Int, ConInfo (Gen g sym))], Int,
 [(Int, ConInfo (Gen g sym))])
-> Int
-> ConInfo (Gen g sym)
-> (Int, [(Int, ConInfo (Gen g sym))], Int,
    [(Int, ConInfo (Gen g sym))])
forall {a} {c} {a} {a}.
(Num a, Num c) =>
(a, [(a, ConInfo a)], c, [(a, ConInfo a)])
-> a -> ConInfo a -> (a, [(a, ConInfo a)], c, [(a, ConInfo a)])
check (Int
0,[],Int
0,[]) Vector (ConInfo (Gen g sym))
cons

    randomCon' :: Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
    randomCon' :: Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym
randomCon' Int
conLen [(Int, ConInfo (Gen g sym))]
cons' Integer
sz g
g0 =
      let (Int
idx, g
g1) = (Int, Int) -> g -> (Int, g)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
0, Int
conLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) g
g0
          (Int
num, ConInfo (Gen g sym)
con) = [(Int, ConInfo (Gen g sym))]
cons' [(Int, ConInfo (Gen g sym))] -> Int -> (Int, ConInfo (Gen g sym))
forall a. HasCallStack => [a] -> Int -> a
!! Int
idx
          (g
g2, !Vector (SEval sym (GenValue sym))
flds') =
            (g -> Gen g sym -> (g, SEval sym (GenValue sym)))
-> g
-> Vector (Gen g sym)
-> (g, Vector (SEval sym (GenValue sym)))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
              (\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))
forall a b. a -> b -> b
seq SEval sym (GenValue sym)
v (g
g', SEval sym (GenValue sym)
v))
              g
g1 (ConInfo (Gen g sym) -> Vector (Gen g sym)
forall a. ConInfo a -> Vector a
conFields ConInfo (Gen g sym)
con) in
      (((Vector (SEval sym (GenValue sym)) -> GenValue sym)
-> Vector (SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ Vector (SEval sym (GenValue sym))
flds') ((Vector (SEval sym (GenValue sym)) -> GenValue sym)
 -> GenValue sym)
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Ident
-> Int
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
forall sym.
Backend sym =>
sym
-> Ident
-> Int
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
evalEnumCon sym
sym (ConInfo (Gen g sym) -> Ident
forall a. ConInfo a -> Ident
conIdent ConInfo (Gen g sym)
con) Int
num, g
g2)

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 = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
100 Integer
w)
        ( Integer
x, g
g') = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
10Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*(Integer
szInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) g
g0
     in if | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2    -> (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 -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpNaN sym
sym Integer
e Integer
p, g
g')
           | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
4    -> (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 -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpPosInf sym
sym Integer
e Integer
p, g
g')
           | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
6    -> (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 -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym (SFloat sym -> SEval sym (SFloat sym))
-> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpPosInf sym
sym Integer
e Integer
p), g
g')
           | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
8    -> (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 Rational
0, g
g')
           | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
10   -> (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 -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym (SFloat sym -> SEval sym (SFloat sym))
-> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m 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 Rational
0), g
g')
           | Integer
x Integer -> Integer -> Bool
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
4Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*(Integer
szInteger -> Integer -> Integer
forall 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 (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
sz) g
g'  -- remaining ~50%

  where
    emax :: Integer
emax = Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
e) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
    smax :: Integer
smax = Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
p) Integer -> Integer -> Integer
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) = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
p)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) g
g
       in (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 -> SWord sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
fpFromBits sym
sym Integer
e Integer
p (SWord sym -> SEval sym (SFloat sym))
-> SEval sym (SWord sym) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (Integer
eInteger -> Integer -> Integer
forall 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) = g -> (Bool, g)
forall g. RandomGen g => g -> (Bool, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
          (Integer
v, g
g2)   = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
1, Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
p) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) g
g1
       in (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
<$> ((if Bool
sgn then sym -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym else SFloat sym -> SEval sym (SFloat sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) (SFloat sym -> SEval sym (SFloat sym))
-> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
fpFromBits sym
sym Integer
e Integer
p (SWord sym -> SEval sym (SFloat sym))
-> SEval sym (SWord sym) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (Integer
eInteger -> Integer -> Integer
forall 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) = g -> (Bool, g)
forall g. RandomGen g => g -> (Bool, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
          (Integer
ex,  g
g2) = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR ((Integer
1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
emax)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
sz Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
100, (Integer
szInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
emax) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
100) g
g1
          (Integer
mag, g
g3) = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
1, Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 ((Integer
szInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
smax) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
100)) g
g2
          r :: Rational
r  = Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Integer
mag Rational -> Integer -> Rational
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (Integer
ex Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer -> Integer
widthInteger Integer
mag)
          r' :: Rational
r' = if Bool
sgn then Rational -> Rational
forall a. Num a => a -> a
negate Rational
r else Rational
r
       in (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 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 IO TestResult -> (EvalErrorEx -> IO TestResult) -> IO TestResult
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 <- CallStack -> Eval Bool -> IO Bool
forall a. CallStack -> Eval a -> IO a
runEval CallStack
forall a. Monoid a => a
mempty (Value -> [Value] -> Eval Bool
go Value
v0 [Value]
vs0)
      if Bool
result
        then TestResult -> IO TestResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
Pass
        else TestResult -> IO TestResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Value] -> TestResult
FailFalse [Value]
vs0)
    handle :: EvalErrorEx -> IO TestResult
handle EvalErrorEx
e = TestResult -> IO TestResult
forall a. a -> IO a
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' <- Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun Concrete
Concrete Value
f (Value -> Eval Value
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)
                              Value -> [Value] -> Eval Bool
go Value
f' [Value]
vs
    go VFun{}   []       = 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 a. a -> Eval a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 :: 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 <- 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 a. a -> Maybe a
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 a. a -> Maybe a
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]],
   [Integer -> g -> (Eval Value, g)])
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 Integer
e Integer
p -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
p))
  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 a. Num a => [a] -> a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TValue -> Maybe Integer
typeSize [TValue]
els
  TVRec RecordMap Ident TValue
fs -> RecordMap Ident Integer -> Integer
forall a. Num a => RecordMap Ident a -> a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse TValue -> Maybe Integer
typeSize RecordMap Ident TValue
fs
  TVFun{} -> Maybe Integer
forall a. Maybe a
Nothing
  TVNominal NominalType
_ [Either Nat' TValue]
_ TNominalTypeValue
nv ->
    case TNominalTypeValue
nv of
      TVStruct RecordMap Ident TValue
tbody -> TValue -> Maybe Integer
typeSize (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)
      TVEnum Vector (ConInfo TValue)
cons -> Vector Integer -> Integer
forall a. Num a => Vector a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Vector Integer -> Integer)
-> Maybe (Vector Integer) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ConInfo TValue -> Maybe Integer)
-> Vector (ConInfo TValue) -> Maybe (Vector Integer)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
mapM (Vector TValue -> Maybe Integer
conSize (Vector TValue -> Maybe Integer)
-> (ConInfo TValue -> Vector TValue)
-> ConInfo TValue
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConInfo TValue -> Vector TValue
forall a. ConInfo a -> Vector a
conFields) Vector (ConInfo TValue)
cons
        where conSize :: Vector TValue -> Maybe Integer
conSize = (TValue -> Maybe Integer -> Maybe Integer)
-> Maybe Integer -> Vector TValue -> Maybe Integer
forall a b. (a -> b -> b) -> b -> Vector a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\TValue
t Maybe Integer
sz -> (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
(*) (TValue -> Maybe Integer
typeSize TValue
t) Maybe Integer
sz) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1)
      TNominalTypeValue
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 Integer
e Integer
p -> [ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
VFloat (Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p Integer
v) | Integer
v <- [Integer
0 .. Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
p) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1] ]
    TVArray{}   -> []
    TVStream{}  -> []
    TVSeq Integer
n TValue
TVBit ->
      [ WordValue Concrete -> Value
forall sym. WordValue sym -> GenValue sym
VWord (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 ->
      [ Concrete -> Integer -> FinSeq Concrete -> Value
forall sym.
Backend sym =>
sym -> Integer -> FinSeq sym -> GenValue sym
finSeq Concrete
Concrete Integer
n ([SEval Concrete Value] -> FinSeq Concrete
forall sym. Backend sym => [SEval sym (GenValue sym)] -> FinSeq sym
unsafeToFinSeq ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
xs)) -- safe, since the TVBit case is covered above
      | [Value]
xs <- [[Value]] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 a. a -> Eval a
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall a. a -> Eval a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse TValue -> [Value]
typeValues RecordMap Ident TValue
fs
      ]
    TVFun{} -> []
    TVNominal NominalType
_ [Either Nat' TValue]
_ TNominalTypeValue
nv ->
      case TNominalTypeValue
nv of
        TVStruct RecordMap Ident TValue
tbody -> TValue -> [Value]
typeValues (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)
        TVEnum Vector (ConInfo TValue)
cons ->
          [ SInteger Concrete -> IntMap (ConValue Concrete) -> Value
forall sym. SInteger sym -> IntMap (ConValue sym) -> GenValue sym
VEnum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tag) (Int -> ConInfo (Eval Value) -> IntMap (ConInfo (Eval Value))
forall a. Int -> a -> IntMap a
IntMap.singleton Int
tag ConInfo (Eval Value)
con')
          | (Int
tag,ConInfo TValue
con) <- [Int] -> [ConInfo TValue] -> [(Int, ConInfo TValue)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (Vector (ConInfo TValue) -> [ConInfo TValue]
forall a. Vector a -> [a]
Vector.toList Vector (ConInfo TValue)
cons)
          , Vector Value
vs        <- (TValue -> [Value]) -> Vector TValue -> [Vector Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
mapM TValue -> [Value]
typeValues (ConInfo TValue -> Vector TValue
forall a. ConInfo a -> Vector a
conFields ConInfo TValue
con)
          , let con' :: ConInfo (Eval Value)
con' = ConInfo TValue
con { conFields = pure <$> vs }
          ]
        TNominalTypeValue
TVAbstract -> []

--------------------------------------------------------------------------------
-- 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 [] = (TestResult, Integer) -> m (TestResult, Integer)
forall a. a -> m a
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 a. IO a -> m a
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 a. a -> m a
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 = ((TestResult, Integer), g) -> (TestResult, Integer)
forall a b. (a, b) -> a
fst (((TestResult, Integer), g) -> (TestResult, Integer))
-> m ((TestResult, Integer), g) -> m (TestResult, Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m ((TestResult, Integer), g)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
maxTests = ((TestResult, Integer), g) -> m ((TestResult, Integer), g)
forall a. a -> m a
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' = 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 a. IO a -> m a
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), g)
go (Integer
testNumInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) g
g'
           TestResult
failure -> ((TestResult, Integer), g) -> m ((TestResult, Integer), g)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TestResult
failure, Integer
testNum), g
g)