-- |
-- 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
, exhaustiveTests
, randomTests
) where

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

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

import Cryptol.Backend        (Backend(..), SRational(..))
import Cryptol.Backend.FloatHelpers (floatFromBits)
import Cryptol.Backend.Monad  (runEval,Eval,EvalErrorEx(..))
import Cryptol.Backend.Concrete

import Cryptol.Eval.Type      (TValue(..))
import Cryptol.Eval.Value     (GenValue(..),SeqMap(..), WordValue(..),
                               ppValue, defaultPPOpts, finiteSeqMap, fromVFun)
import Cryptol.TypeCheck.Solver.InfNat (widthInteger)
import Cryptol.Utils.Ident    (Ident)
import Cryptol.Utils.Panic    (panic)
import Cryptol.Utils.RecordMap

type Gen g x = Integer -> g -> (SEval x (GenValue x), g)


type Value = GenValue Concrete

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

    Please note that this function assumes that the generators match
    the supplied value, otherwise we'll panic.
 -}
runOneTest :: RandomGen g
        => Value   -- ^ Function under test
        -> [Gen g Concrete] -- ^ Argument generators
        -> Integer -- ^ Size
        -> g
        -> IO (TestResult, g)
runOneTest :: 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' <- 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)
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' <- 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)
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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Value
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)
    TVNewtype Newtype
_ [Either Nat' TValue]
_ 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
  let v :: GenValue sym
v  = 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
$ \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)
seq Seq (SEval sym (GenValue sym))
xs (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v, g
g2)

{-# INLINE randomTuple #-}

-- | Generate a random tuple value.
randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym
randomTuple :: [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
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 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     -> Gen g sym
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 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 a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
          (Integer
v, g
g2)   = (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 (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 :: Gen g sym
genNormal Integer
sz g
g =
      let (Bool
sgn, g
g1) = 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 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 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 (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 :: EvalErrorEx -> IO TestResult
handle EvalErrorEx
e = TestResult -> IO TestResult
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 (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 (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 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 (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
  TVNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident TValue
tbody -> TValue -> Maybe Integer
typeSize (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)

{- | Returns all the values in a type.  Returns an empty list of values,
for types where 'typeSize' returned 'Nothing'. -}
typeValues :: TValue -> [Value]
typeValues :: TValue -> [Value]
typeValues TValue
ty =
  case TValue
ty of
    TValue
TVBit       -> [ 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 ->
      [ 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 ([SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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{} -> []
    TVNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident TValue
tbody -> TValue -> [Value]
typeValues (RecordMap Ident TValue -> TValue
TVRec RecordMap Ident TValue
tbody)

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

exhaustiveTests :: MonadIO m =>
  (Integer -> m ()) {- ^ progress callback -} ->
  Value {- ^ function under test -} ->
  [[Value]] {- ^ exhaustive set of test values -} ->
  m (TestResult, Integer)
exhaustiveTests :: (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)