-- | A simple testing driver for testing properties using FEAT.
-- Contains three drivers with different levels of flexibility of configuration.
--
-- Ironically, this code is mostly untested at the moment.
module Test.Feat.Driver(
   -- * Simple test driver
   test
   -- * Test driver with show/readable options
   , testOptions
   , Options(..)
   , defOptions
   -- * Extremely flexible test driver
   , testFlex
   , Result(..)
   , FlexibleOptions
   , FlexOptions(..)
   , defFlex
   , toFlex
   , toFlexWith
   ) where

import Control.Enumerable
import Test.Feat.Access
import Test.Feat.Finite
import Test.Feat.Enumerate

import System.Timeout
import Data.IORef

-- | Basic options for executing a test. Unlike 'FlexibleOptions' this type has Show/Read instances.
data Options = Options
   { Options -> Maybe Int
oTimeoutSec :: Maybe Int
   , Options -> Maybe (Int, Int)
oSizeFromTo :: Maybe (Int,Int)        -- ^ (first size, last size)
   , Options -> Maybe Int
oMaxCounter :: Maybe Int              -- ^ Maximum number of counterexamples
   , Options -> Bool
oSilent     :: Bool
   , Options -> Maybe (Index, Index)
oSkipping   :: Maybe (Index, Integer) -- ^ (start-index, steps to skip)
   , Options -> Maybe Index
oBounded    :: Maybe Integer          -- ^ Maximum number of tests per size
   } deriving (Int -> Options -> ShowS
[Options] -> ShowS
Options -> String
(Int -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> String
$cshow :: Options -> String
showsPrec :: Int -> Options -> ShowS
$cshowsPrec :: Int -> Options -> ShowS
Show,ReadPrec [Options]
ReadPrec Options
Int -> ReadS Options
ReadS [Options]
(Int -> ReadS Options)
-> ReadS [Options]
-> ReadPrec Options
-> ReadPrec [Options]
-> Read Options
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Options]
$creadListPrec :: ReadPrec [Options]
readPrec :: ReadPrec Options
$creadPrec :: ReadPrec Options
readList :: ReadS [Options]
$creadList :: ReadS [Options]
readsPrec :: Int -> ReadS Options
$creadsPrec :: Int -> ReadS Options
Read)

-- | Much more flexible options for configuring every part of the test execution.
-- @a@ is the parameter type of the property.
type FlexibleOptions a = IO (FlexOptions a)

-- | FlexOptions
data FlexOptions a = FlexOptions
   { FlexOptions a -> IO Bool -> IO (Result, [a])
fIO      :: IO Bool     -> IO (Result,[a]) -- ^ The whole execution of the test is sent through this function.
   , FlexOptions a -> a -> IO Bool
fReport  :: a           -> IO Bool -- ^ Applied to each found counterexample, return False to stop testing
   , FlexOptions a -> String -> IO ()
fOutput  :: String      -> IO () -- ^ Print text
   , FlexOptions a -> Enumerate a -> Enumerate a
fProcess :: Enumerate a -> Enumerate a -- ^ Applied to the enumeration before running
   , FlexOptions a -> Enumerate a
fEnum    :: Enumerate a -- ^ The base enumeration to use, before applying @fProcess@.
   }

data Result = Exhausted -- ^ Reached max size
            | Quota     -- ^ Reached max number of counterexamples
            | TimedOut
            | Other
            deriving Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> Result -> ShowS
Show

-- | 60 seconds timeout, maximum size of 100, bound of 100000 tests per size
defOptions :: Options
defOptions :: Options
defOptions = Options :: Maybe Int
-> Maybe (Int, Int)
-> Maybe Int
-> Bool
-> Maybe (Index, Index)
-> Maybe Index
-> Options
Options
  { oTimeoutSec :: Maybe Int
oTimeoutSec = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
60
  , oSizeFromTo :: Maybe (Int, Int)
oSizeFromTo = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
0,Int
100)
  , oSilent :: Bool
oSilent     = Bool
False
  , oSkipping :: Maybe (Index, Index)
oSkipping   = Maybe (Index, Index)
forall a. Maybe a
Nothing
  , oBounded :: Maybe Index
oBounded    = Index -> Maybe Index
forall a. a -> Maybe a
Just Index
100000
  , oMaxCounter :: Maybe Int
oMaxCounter = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  }

defFlex :: Enumerable a => FlexibleOptions a
defFlex :: FlexibleOptions a
defFlex = Enumerate a -> FlexibleOptions a
forall a. Enumerate a -> FlexibleOptions a
defFlexWith Enumerate a
forall a. Enumerable a => Enumerate a
optimal

-- | For testing without using the 'Enumerable' class.
defFlexWith :: Enumerate a -> FlexibleOptions a
defFlexWith :: Enumerate a -> FlexibleOptions a
defFlexWith Enumerate a
e = Enumerate a -> Options -> FlexibleOptions a
forall a. Enumerate a -> Options -> FlexibleOptions a
toFlexWith Enumerate a
e Options
defOptions

toFlex :: Enumerable a => Options -> FlexibleOptions a
toFlex :: Options -> FlexibleOptions a
toFlex = Enumerate a -> Options -> FlexibleOptions a
forall a. Enumerate a -> Options -> FlexibleOptions a
toFlexWith Enumerate a
forall a. Enumerable a => Enumerate a
optimal

toFlexWith :: Enumerate a -> Options -> FlexibleOptions a
toFlexWith :: Enumerate a -> Options -> FlexibleOptions a
toFlexWith Enumerate a
e Options
o = do
  IORef [a]
res <- [a] -> IO (IORef [a])
forall a. a -> IO (IORef a)
newIORef []
  IORef Int
count <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
  let doReport :: a -> IO Bool
doReport a
x = do
        IORef [a] -> ([a] -> [a]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [a]
res (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:)
        IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef Int
count (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        IO Bool -> (Int -> IO Bool) -> Maybe Int -> IO Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) (Int -> IO Bool
checkCount) (Options -> Maybe Int
oMaxCounter Options
o)
      checkCount :: Int -> IO Bool
checkCount Int
mx = do
        Int
n <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
count
        Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
mx)
      doIO :: IO Bool -> IO (Result, [a])
doIO IO Bool
io = do
        Maybe Bool
mb <- IO (Maybe Bool)
-> (Int -> IO (Maybe Bool)) -> Maybe Int -> IO (Maybe Bool)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Bool -> Maybe Bool) -> IO Bool -> IO (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Maybe Bool
forall a. a -> Maybe a
Just IO Bool
io) (\Int
t -> Int -> IO Bool -> IO (Maybe Bool)
forall a. Int -> IO a -> IO (Maybe a)
timeout (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1000000) IO Bool
io) (Options -> Maybe Int
oTimeoutSec Options
o)
        [a]
res' <- IORef [a] -> IO [a]
forall a. IORef a -> IO a
readIORef IORef [a]
res
        (Result, [a]) -> IO (Result, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Result, [a]) -> IO (Result, [a]))
-> (Result, [a]) -> IO (Result, [a])
forall a b. (a -> b) -> a -> b
$ (Result, [a])
-> (Bool -> (Result, [a])) -> Maybe Bool -> (Result, [a])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Result
TimedOut,[a]
res') (\Bool
b -> if Bool
b then (Result
Exhausted,[a]
res') else (Result
Quota,[a]
res')) Maybe Bool
mb
      skip :: Enumerate a -> Enumerate a
skip  = (Enumerate a -> Enumerate a)
-> ((Index, Index) -> Enumerate a -> Enumerate a)
-> Maybe (Index, Index)
-> Enumerate a
-> Enumerate a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Enumerate a -> Enumerate a
forall a. a -> a
id ((Enumerate a -> (Index, Index) -> Enumerate a)
-> (Index, Index) -> Enumerate a -> Enumerate a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Index -> Index -> Enumerate a) -> (Index, Index) -> Enumerate a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Index -> Index -> Enumerate a) -> (Index, Index) -> Enumerate a)
-> (Enumerate a -> Index -> Index -> Enumerate a)
-> Enumerate a
-> (Index, Index)
-> Enumerate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enumerate a -> Index -> Index -> Enumerate a
forall a. Enumerate a -> Index -> Index -> Enumerate a
skipping)) (Options -> Maybe (Index, Index)
oSkipping Options
o)
      bound :: Enumerate a -> Enumerate a
bound = (Enumerate a -> Enumerate a)
-> (Index -> Enumerate a -> Enumerate a)
-> Maybe Index
-> Enumerate a
-> Enumerate a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Enumerate a -> Enumerate a
forall a. a -> a
id ((Enumerate a -> Index -> Enumerate a)
-> Index -> Enumerate a -> Enumerate a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Enumerate a -> Index -> Enumerate a
forall a. Enumerate a -> Index -> Enumerate a
bounded) (Options -> Maybe Index
oBounded Options
o)
      sizes :: Enumerate a -> Enumerate a
sizes = (Enumerate a -> Enumerate a)
-> ((Int, Int) -> Enumerate a -> Enumerate a)
-> Maybe (Int, Int)
-> Enumerate a
-> Enumerate a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Enumerate a -> Enumerate a
forall a. a -> a
id ((Enumerate a -> (Int, Int) -> Enumerate a)
-> (Int, Int) -> Enumerate a -> Enumerate a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Enumerate a -> (Int, Int) -> Enumerate a
forall a. Enumerate a -> (Int, Int) -> Enumerate a
sizeRange) (Options -> Maybe (Int, Int)
oSizeFromTo Options
o)
  FlexOptions a -> FlexibleOptions a
forall (m :: * -> *) a. Monad m => a -> m a
return (FlexOptions a -> FlexibleOptions a)
-> FlexOptions a -> FlexibleOptions a
forall a b. (a -> b) -> a -> b
$ FlexOptions :: forall a.
(IO Bool -> IO (Result, [a]))
-> (a -> IO Bool)
-> (String -> IO ())
-> (Enumerate a -> Enumerate a)
-> Enumerate a
-> FlexOptions a
FlexOptions
      { fIO :: IO Bool -> IO (Result, [a])
fIO = IO Bool -> IO (Result, [a])
doIO
      , fOutput :: String -> IO ()
fOutput = if Options -> Bool
oSilent Options
o then IO () -> String -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) else String -> IO ()
putStr
      , fReport :: a -> IO Bool
fReport = a -> IO Bool
doReport
      , fProcess :: Enumerate a -> Enumerate a
fProcess = Enumerate a -> Enumerate a
forall a. Enumerate a -> Enumerate a
bound (Enumerate a -> Enumerate a)
-> (Enumerate a -> Enumerate a) -> Enumerate a -> Enumerate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enumerate a -> Enumerate a
forall a. Enumerate a -> Enumerate a
skip (Enumerate a -> Enumerate a)
-> (Enumerate a -> Enumerate a) -> Enumerate a -> Enumerate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enumerate a -> Enumerate a
forall a. Enumerate a -> Enumerate a
sizes
      , fEnum :: Enumerate a
fEnum = Enumerate a
e
      }

-- | Test with default options ('defOptions'). Returns a list of counterexamples
test :: Enumerable a => (a -> Bool) -> IO [a]
test :: (a -> Bool) -> IO [a]
test = Options -> (a -> Bool) -> IO [a]
forall a. Enumerable a => Options -> (a -> Bool) -> IO [a]
testOptions Options
defOptions

-- | Test with basic options. Returns a list of counterexamples.
testOptions :: Enumerable a => Options -> (a -> Bool) -> IO [a]
testOptions :: Options -> (a -> Bool) -> IO [a]
testOptions Options
o a -> Bool
p = ((Result, [a]) -> [a]) -> IO (Result, [a]) -> IO [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Result, [a]) -> [a]
forall a b. (a, b) -> b
snd (IO (Result, [a]) -> IO [a]) -> IO (Result, [a]) -> IO [a]
forall a b. (a -> b) -> a -> b
$ FlexibleOptions a -> (a -> Bool) -> IO (Result, [a])
forall a. FlexibleOptions a -> (a -> Bool) -> IO (Result, [a])
testFlex FlexibleOptions a
fo a -> Bool
p
  where
    fo :: FlexibleOptions a
fo = Options -> FlexibleOptions a
forall a. Enumerable a => Options -> FlexibleOptions a
toFlex Options
o

-- | The most flexible test driver, can be configured to behave in almost any way.
testFlex :: FlexibleOptions a -> (a -> Bool) -> IO (Result, [a])
testFlex :: FlexibleOptions a -> (a -> Bool) -> IO (Result, [a])
testFlex FlexibleOptions a
ioOp a -> Bool
p = do
  FlexOptions a
op <- FlexibleOptions a
ioOp
  let e :: Enumerate a
e = FlexOptions a -> Enumerate a -> Enumerate a
forall a. FlexOptions a -> Enumerate a -> Enumerate a
fProcess FlexOptions a
op (FlexOptions a -> Enumerate a
forall a. FlexOptions a -> Enumerate a
fEnum FlexOptions a
op)
      lazyResult :: [(Index, [a])]
lazyResult = [(Index
n,(a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
p) [a]
xs) | (Index
n,[a]
xs) <- Enumerate a -> [(Index, [a])]
forall a. Enumerate a -> [(Index, [a])]
valuesWith Enumerate a
e]
      runSize :: a -> (a, [a]) -> IO Bool
runSize a
k (a
n,[a]
cs) = do
        FlexOptions a -> String -> IO ()
forall a. FlexOptions a -> String -> IO ()
fOutput FlexOptions a
op (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"*** Searching in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" values of size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
        [IO Bool] -> IO Bool
doWhile ((a -> IO Bool) -> [a] -> [IO Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> FlexOptions a -> String -> IO ()
forall a. FlexOptions a -> String -> IO ()
fOutput FlexOptions a
op String
"Counterexample found!\n" IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FlexOptions a -> a -> IO Bool
forall a. FlexOptions a -> a -> IO Bool
fReport FlexOptions a
op a
x) [a]
cs)
  rxs :: (Result, [a])
rxs@(Result
r,[a]
_) <- FlexOptions a -> IO Bool -> IO (Result, [a])
forall a. FlexOptions a -> IO Bool -> IO (Result, [a])
fIO FlexOptions a
op (([IO Bool] -> IO Bool
doWhile ([IO Bool] -> IO Bool) -> [IO Bool] -> IO Bool
forall a b. (a -> b) -> a -> b
$ (Index -> (Index, [a]) -> IO Bool)
-> [Index] -> [(Index, [a])] -> [IO Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Index -> (Index, [a]) -> IO Bool
forall a a. (Show a, Show a) => a -> (a, [a]) -> IO Bool
runSize [Index
0 :: Integer ..] [(Index, [a])]
lazyResult))
  case Result
r of
     Result
Exhausted -> FlexOptions a -> String -> IO ()
forall a. FlexOptions a -> String -> IO ()
fOutput FlexOptions a
op String
"Search space exhausted\n"
     Result
TimedOut  -> FlexOptions a -> String -> IO ()
forall a. FlexOptions a -> String -> IO ()
fOutput FlexOptions a
op String
"Timed out\n"
     Result
_         -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  (Result, [a]) -> IO (Result, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Result, [a])
rxs


doWhile :: [IO Bool] -> IO Bool
doWhile :: [IO Bool] -> IO Bool
doWhile [] = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
doWhile (IO Bool
iob:[IO Bool]
iobs) = IO Bool
iob IO Bool -> (Bool -> IO Bool) -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b -> if Bool
b then [IO Bool] -> IO Bool
doWhile [IO Bool]
iobs else Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False