-- Testing conjectures using QuickCheck.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-}
module QuickSpec.Internal.Testing.QuickCheck where

import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Prop
import Test.QuickCheck
import Test.QuickCheck.Gen
import Test.QuickCheck.Random
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.Reader
import Data.List
import System.Random hiding (uniform)
import QuickSpec.Internal.Terminal
import Data.Lens.Light

data Config =
  Config {
    Config -> Int
cfg_num_tests :: Int,
    Config -> Int
cfg_max_test_size :: Int,
    Config -> Maybe QCGen
cfg_fixed_seed :: Maybe QCGen}
  deriving Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show

lens_num_tests :: Lens Config Int
lens_num_tests = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_num_tests (\Int
x Config
y -> Config
y { cfg_num_tests :: Int
cfg_num_tests = Int
x })
lens_max_test_size :: Lens Config Int
lens_max_test_size = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_test_size (\Int
x Config
y -> Config
y { cfg_max_test_size :: Int
cfg_max_test_size = Int
x })
lens_fixed_seed :: Lens Config (Maybe QCGen)
lens_fixed_seed = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Maybe QCGen
cfg_fixed_seed (\Maybe QCGen
x Config
y -> Config
y { cfg_fixed_seed :: Maybe QCGen
cfg_fixed_seed = Maybe QCGen
x })

data Environment testcase term result =
  Environment {
    forall testcase term result.
Environment testcase term result -> Config
env_config :: Config,
    forall testcase term result.
Environment testcase term result -> [testcase]
env_tests :: [testcase],
    forall testcase term result.
Environment testcase term result
-> testcase -> term -> Maybe result
env_eval :: testcase -> term -> Maybe result }

newtype Tester testcase term result m a =
  Tester (ReaderT (Environment testcase term result) m a)
  deriving (forall a b.
a
-> Tester testcase term result m b
-> Tester testcase term result m a
forall a b.
(a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
forall testcase term result (m :: * -> *) a b.
Functor m =>
a
-> Tester testcase term result m b
-> Tester testcase term result m a
forall testcase term result (m :: * -> *) a b.
Functor m =>
(a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b.
a
-> Tester testcase term result m b
-> Tester testcase term result m a
$c<$ :: forall testcase term result (m :: * -> *) a b.
Functor m =>
a
-> Tester testcase term result m b
-> Tester testcase term result m a
fmap :: forall a b.
(a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
$cfmap :: forall testcase term result (m :: * -> *) a b.
Functor m =>
(a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
Functor, forall a. a -> Tester testcase term result m a
forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m a
forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
forall a b.
Tester testcase term result m (a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
forall a b c.
(a -> b -> c)
-> Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m c
forall {testcase} {term} {result} {m :: * -> *}.
Applicative m =>
Functor (Tester testcase term result m)
forall testcase term result (m :: * -> *) a.
Applicative m =>
a -> Tester testcase term result m a
forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m a
forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m (a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
forall testcase term result (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m a
$c<* :: forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m a
*> :: forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
$c*> :: forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
liftA2 :: forall a b c.
(a -> b -> c)
-> Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m c
$cliftA2 :: forall testcase term result (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m c
<*> :: forall a b.
Tester testcase term result m (a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
$c<*> :: forall testcase term result (m :: * -> *) a b.
Applicative m =>
Tester testcase term result m (a -> b)
-> Tester testcase term result m a
-> Tester testcase term result m b
pure :: forall a. a -> Tester testcase term result m a
$cpure :: forall testcase term result (m :: * -> *) a.
Applicative m =>
a -> Tester testcase term result m a
Applicative, forall a. a -> Tester testcase term result m a
forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
forall a b.
Tester testcase term result m a
-> (a -> Tester testcase term result m b)
-> Tester testcase term result m b
forall {testcase} {term} {result} {m :: * -> *}.
Monad m =>
Applicative (Tester testcase term result m)
forall testcase term result (m :: * -> *) a.
Monad m =>
a -> Tester testcase term result m a
forall testcase term result (m :: * -> *) a b.
Monad m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
forall testcase term result (m :: * -> *) a b.
Monad m =>
Tester testcase term result m a
-> (a -> Tester testcase term result m b)
-> Tester testcase term result m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Tester testcase term result m a
$creturn :: forall testcase term result (m :: * -> *) a.
Monad m =>
a -> Tester testcase term result m a
>> :: forall a b.
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
$c>> :: forall testcase term result (m :: * -> *) a b.
Monad m =>
Tester testcase term result m a
-> Tester testcase term result m b
-> Tester testcase term result m b
>>= :: forall a b.
Tester testcase term result m a
-> (a -> Tester testcase term result m b)
-> Tester testcase term result m b
$c>>= :: forall testcase term result (m :: * -> *) a b.
Monad m =>
Tester testcase term result m a
-> (a -> Tester testcase term result m b)
-> Tester testcase term result m b
Monad, forall a. IO a -> Tester testcase term result m a
forall {testcase} {term} {result} {m :: * -> *}.
MonadIO m =>
Monad (Tester testcase term result m)
forall testcase term result (m :: * -> *) a.
MonadIO m =>
IO a -> Tester testcase term result m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Tester testcase term result m a
$cliftIO :: forall testcase term result (m :: * -> *) a.
MonadIO m =>
IO a -> Tester testcase term result m a
MonadIO, String -> Tester testcase term result m ()
forall {testcase} {term} {result} {m :: * -> *}.
MonadTerminal m =>
Monad (Tester testcase term result m)
forall testcase term result (m :: * -> *).
MonadTerminal m =>
String -> Tester testcase term result m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> Tester testcase term result m ()
$cputTemp :: forall testcase term result (m :: * -> *).
MonadTerminal m =>
String -> Tester testcase term result m ()
putLine :: String -> Tester testcase term result m ()
$cputLine :: forall testcase term result (m :: * -> *).
MonadTerminal m =>
String -> Tester testcase term result m ()
putText :: String -> Tester testcase term result m ()
$cputText :: forall testcase term result (m :: * -> *).
MonadTerminal m =>
String -> Tester testcase term result m ()
MonadTerminal, MonadPruner term' res')

instance MonadTrans (Tester testcase term result) where
  lift :: forall (m :: * -> *) a.
Monad m =>
m a -> Tester testcase term result m a
lift = forall testcase term result (m :: * -> *) a.
ReaderT (Environment testcase term result) m a
-> Tester testcase term result m a
Tester forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

run ::
  Config -> Gen testcase -> (testcase -> term -> Maybe result) ->
  Tester testcase term result m a -> Gen (m a)
run :: forall testcase term result (m :: * -> *) a.
Config
-> Gen testcase
-> (testcase -> term -> Maybe result)
-> Tester testcase term result m a
-> Gen (m a)
run config :: Config
config@Config{Int
Maybe QCGen
cfg_fixed_seed :: Maybe QCGen
cfg_max_test_size :: Int
cfg_num_tests :: Int
cfg_fixed_seed :: Config -> Maybe QCGen
cfg_max_test_size :: Config -> Int
cfg_num_tests :: Config -> Int
..} Gen testcase
gen testcase -> term -> Maybe result
eval (Tester ReaderT (Environment testcase term result) m a
x) = do
  QCGen
seed <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Arbitrary a => Gen a
arbitrary forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QCGen
cfg_fixed_seed
  let
    seeds :: [QCGen]
seeds = forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall g. RandomGen g => g -> (g, g)
split) QCGen
seed
    n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a b. (RealFrac a, Integral b) => a -> b
ceiling (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
cfg_num_tests forall a. Num a => a -> a -> a
* (Double
1 forall a. Num a => a -> a -> a
- Double
zeroProportion)))
    zeroes :: Int
zeroes = Int
cfg_num_tests forall a. Num a => a -> a -> a
- Int
n
    k :: Int
k = forall a. Ord a => a -> a -> a
max Int
1 Int
cfg_max_test_size
    bias :: Integer
bias = Integer
3
    -- Run this proportion of tests of size 0.
    zeroProportion :: Double
zeroProportion = Double
0.01
    -- Bias tests towards smaller sizes.
    -- We do this by distributing the cube of the size uniformly.
    sizes :: [Int]
sizes =
      forall a. Int -> a -> [a]
replicate Int
zeroes Int
0 forall a. [a] -> [a] -> [a]
++
      (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Int
k forall a. Num a => a -> a -> a
-) forall a b. (a -> b) -> a -> b
$
       forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (RealFrac a, Integral b) => a -> b
truncate forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Floating a => a -> a -> a
** (Double
1forall a. Fractional a => a -> a -> a
/forall a. Num a => Integer -> a
fromInteger Integer
bias)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) forall a b. (a -> b) -> a -> b
$
       Integer -> Integer -> [Integer]
uniform (forall a. Integral a => a -> Integer
toInteger Int
n) (forall a. Integral a => a -> Integer
toInteger Int
kforall a b. (Num a, Integral b) => a -> b -> a
^Integer
bias))
    tests :: [testcase]
tests = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a. Gen a -> QCGen -> Int -> a
unGen Gen testcase
gen) [QCGen]
seeds [Int]
sizes
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (Environment testcase term result) m a
x
    Environment {
      env_config :: Config
env_config = Config
config,
      env_tests :: [testcase]
env_tests = [testcase]
tests,
      env_eval :: testcase -> term -> Maybe result
env_eval = testcase -> term -> Maybe result
eval }

-- uniform n k: generate a list of n integers which are distributed evenly between 0 and k-1.
uniform :: Integer -> Integer -> [Integer]
uniform :: Integer -> Integer -> [Integer]
uniform Integer
n Integer
k =
  -- n `div` k: divide evenly as far as possible.
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall a. Int -> a -> [a]
replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
n forall a. Integral a => a -> a -> a
`div` Integer
k)) Integer
i | Integer
i <- [Integer
0..Integer
kforall a. Num a => a -> a -> a
-Integer
1]] forall a. [a] -> [a] -> [a]
++
  -- The leftovers get distributed at equal intervals.
  [Integer
i forall a. Num a => a -> a -> a
* Integer
k forall a. Integral a => a -> a -> a
`div` Integer
leftovers | Integer
i <- [Integer
0..Integer
leftoversforall a. Num a => a -> a -> a
-Integer
1]]
  where
    leftovers :: Integer
leftovers = Integer
n forall a. Integral a => a -> a -> a
`mod` Integer
k

instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where
  test :: Prop term -> Tester testcase term result m (TestResult testcase)
test Prop term
prop =
    forall testcase term result (m :: * -> *) a.
ReaderT (Environment testcase term result) m a
-> Tester testcase term result m a
Tester forall a b. (a -> b) -> a -> b
$ do
      env :: Environment testcase term result
env@Environment{[testcase]
Config
testcase -> term -> Maybe result
env_eval :: testcase -> term -> Maybe result
env_tests :: [testcase]
env_config :: Config
env_eval :: forall testcase term result.
Environment testcase term result
-> testcase -> term -> Maybe result
env_tests :: forall testcase term result.
Environment testcase term result -> [testcase]
env_config :: forall testcase term result.
Environment testcase term result -> Config
..} <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall testcase.
TestResult testcase -> TestResult testcase -> TestResult testcase
testAnd forall testcase. TestResult testcase
TestPassed (forall a b. (a -> b) -> [a] -> [b]
map (forall result testcase term.
Eq result =>
Environment testcase term result
-> Prop term -> testcase -> TestResult testcase
quickCheckTest Environment testcase term result
env Prop term
prop) [testcase]
env_tests)
  retest :: testcase
-> Prop term -> Tester testcase term result m (TestResult testcase)
retest testcase
testcase Prop term
prop =
    forall testcase term result (m :: * -> *) a.
ReaderT (Environment testcase term result) m a
-> Tester testcase term result m a
Tester forall a b. (a -> b) -> a -> b
$ do
      env :: Environment testcase term result
env@Environment{[testcase]
Config
testcase -> term -> Maybe result
env_eval :: testcase -> term -> Maybe result
env_tests :: [testcase]
env_config :: Config
env_eval :: forall testcase term result.
Environment testcase term result
-> testcase -> term -> Maybe result
env_tests :: forall testcase term result.
Environment testcase term result -> [testcase]
env_config :: forall testcase term result.
Environment testcase term result -> Config
..} <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall result testcase term.
Eq result =>
Environment testcase term result
-> Prop term -> testcase -> TestResult testcase
quickCheckTest Environment testcase term result
env Prop term
prop testcase
testcase

quickCheckTest :: Eq result =>
  Environment testcase term result -> Prop term -> testcase -> TestResult testcase
quickCheckTest :: forall result testcase term.
Eq result =>
Environment testcase term result
-> Prop term -> testcase -> TestResult testcase
quickCheckTest Environment{env_config :: forall testcase term result.
Environment testcase term result -> Config
env_config = Config{Int
Maybe QCGen
cfg_fixed_seed :: Maybe QCGen
cfg_max_test_size :: Int
cfg_num_tests :: Int
cfg_fixed_seed :: Config -> Maybe QCGen
cfg_max_test_size :: Config -> Int
cfg_num_tests :: Config -> Int
..}, [testcase]
testcase -> term -> Maybe result
env_eval :: testcase -> term -> Maybe result
env_tests :: [testcase]
env_eval :: forall testcase term result.
Environment testcase term result
-> testcase -> term -> Maybe result
env_tests :: forall testcase term result.
Environment testcase term result -> [testcase]
..} ([Equation term]
lhs :=>: Equation term
rhs) testcase
testcase =
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall testcase.
TestResult testcase -> TestResult testcase -> TestResult testcase
testAnd (Equation term -> TestResult testcase
testEq Equation term
rhs) (forall a b. (a -> b) -> [a] -> [b]
map Equation term -> TestResult testcase
testEq [Equation term]
lhs)
  where
    testEq :: Equation term -> TestResult testcase
testEq (term
t :=: term
u) =
      case (testcase -> term -> Maybe result
env_eval testcase
testcase term
t, testcase -> term -> Maybe result
env_eval testcase
testcase term
u) of
        (Just result
t, Just result
u)
          | result
t forall a. Eq a => a -> a -> Bool
== result
u -> forall testcase. TestResult testcase
TestPassed
          | Bool
otherwise -> forall testcase. testcase -> TestResult testcase
TestFailed testcase
testcase
        (Maybe result, Maybe result)
_ -> forall testcase. TestResult testcase
Untestable