-- |
-- Module      : Test.Tasty.LeanCheck
-- Copyright   : (c) 2018 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- LeanCheck support for the Tasty test framework.
--
-- Here's how your @test.hs@ might look like:
--
-- > import Test.Tasty
-- > import Test.Tasty.LeanCheck as LC
-- > import Data.List
-- >
-- > main :: IO ()
-- > main = defaultMain tests
-- >
-- > tests :: TestTree
-- > tests = testGroup "Test properties checked by LeanCheck"
-- >   [ LC.testProperty "sort == sort . reverse" $
-- >       \list -> sort (list :: [Int]) == sort (reverse list)
-- >   , LC.testProperty "Fermat's little theorem" $
-- >       \x -> ((x :: Integer)^7 - x) `mod` 7 == 0
-- >   -- the following property do not hold
-- >   , LC.testProperty "Fermat's last theorem" $
-- >       \x y z n ->
-- >         (n :: Integer) >= 3 LC.==> x^n + y^n /= (z^n :: Integer)
-- >   ]
--
-- The output for the above program is:
--
-- > $ ./test
-- > Test properties checked by LeanCheck
-- >   sort == sort . reverse:  OK
-- >     +++ OK, passed 200 tests.
-- >   Fermat's little theorem: OK
-- >     +++ OK, passed 200 tests.
-- >   Fermat's last theorem:   FAIL
-- >     *** Failed! Falsifiable (after 71 tests):
-- >     0 0 0 3
-- >
-- > 1 out of 3 tests failed (0.00s)
--
-- Use @--leancheck-tests@ to configure the maximum number of tests for each
-- property.
--
-- Please see the documentation of
-- "Test.LeanCheck" and Tasty
-- for more details.
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ == 708
{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving #-}
#endif
module Test.Tasty.LeanCheck
  ( testProperty
  , LeanCheckTests (..)
  , module Test.LeanCheck
  )
where

import Test.Tasty.Providers hiding (Result)
import Test.Tasty.Options
import Test.LeanCheck
import Data.Proxy
import Control.Applicative (pure)
import Control.Exception (SomeException, catch, evaluate)
#if __GLASGOW_HASKELL__ == 708
import Data.Typeable (Typeable)

deriving instance Typeable Results
deriving instance Typeable Result
deriving instance Typeable LeanCheckTests
#endif

newtype Results = Results [([String],Bool)]

data Result = OK        Int
            | Falsified Int [String]
            | Exception Int [String] String
  deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: Result -> Result -> Bool
Eq, 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)

-- | Create a 'Test' for a LeanCheck 'Testable' property.
-- Example:
--
-- > LC.testProperty "sort is idempotent" $ \xs -> sort (sort xs :: [Int]) == sort xs
testProperty :: Testable a => TestName -> a -> TestTree
testProperty :: String -> a -> TestTree
testProperty String
name = String -> Results -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
name (Results -> TestTree) -> (a -> Results) -> a -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([String], Bool)] -> Results
Results ([([String], Bool)] -> Results)
-> (a -> [([String], Bool)]) -> a -> Results
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [([String], Bool)]
forall a. Testable a => a -> [([String], Bool)]
results

-- | Number of test cases for LeanCheck to generate.
newtype LeanCheckTests = LeanCheckTests Int
  deriving (Int -> LeanCheckTests -> ShowS
[LeanCheckTests] -> ShowS
LeanCheckTests -> String
(Int -> LeanCheckTests -> ShowS)
-> (LeanCheckTests -> String)
-> ([LeanCheckTests] -> ShowS)
-> Show LeanCheckTests
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LeanCheckTests] -> ShowS
$cshowList :: [LeanCheckTests] -> ShowS
show :: LeanCheckTests -> String
$cshow :: LeanCheckTests -> String
showsPrec :: Int -> LeanCheckTests -> ShowS
$cshowsPrec :: Int -> LeanCheckTests -> ShowS
Show, LeanCheckTests -> LeanCheckTests -> Bool
(LeanCheckTests -> LeanCheckTests -> Bool)
-> (LeanCheckTests -> LeanCheckTests -> Bool) -> Eq LeanCheckTests
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LeanCheckTests -> LeanCheckTests -> Bool
$c/= :: LeanCheckTests -> LeanCheckTests -> Bool
== :: LeanCheckTests -> LeanCheckTests -> Bool
$c== :: LeanCheckTests -> LeanCheckTests -> Bool
Eq, Eq LeanCheckTests
Eq LeanCheckTests
-> (LeanCheckTests -> LeanCheckTests -> Ordering)
-> (LeanCheckTests -> LeanCheckTests -> Bool)
-> (LeanCheckTests -> LeanCheckTests -> Bool)
-> (LeanCheckTests -> LeanCheckTests -> Bool)
-> (LeanCheckTests -> LeanCheckTests -> Bool)
-> (LeanCheckTests -> LeanCheckTests -> LeanCheckTests)
-> (LeanCheckTests -> LeanCheckTests -> LeanCheckTests)
-> Ord LeanCheckTests
LeanCheckTests -> LeanCheckTests -> Bool
LeanCheckTests -> LeanCheckTests -> Ordering
LeanCheckTests -> LeanCheckTests -> LeanCheckTests
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LeanCheckTests -> LeanCheckTests -> LeanCheckTests
$cmin :: LeanCheckTests -> LeanCheckTests -> LeanCheckTests
max :: LeanCheckTests -> LeanCheckTests -> LeanCheckTests
$cmax :: LeanCheckTests -> LeanCheckTests -> LeanCheckTests
>= :: LeanCheckTests -> LeanCheckTests -> Bool
$c>= :: LeanCheckTests -> LeanCheckTests -> Bool
> :: LeanCheckTests -> LeanCheckTests -> Bool
$c> :: LeanCheckTests -> LeanCheckTests -> Bool
<= :: LeanCheckTests -> LeanCheckTests -> Bool
$c<= :: LeanCheckTests -> LeanCheckTests -> Bool
< :: LeanCheckTests -> LeanCheckTests -> Bool
$c< :: LeanCheckTests -> LeanCheckTests -> Bool
compare :: LeanCheckTests -> LeanCheckTests -> Ordering
$ccompare :: LeanCheckTests -> LeanCheckTests -> Ordering
$cp1Ord :: Eq LeanCheckTests
Ord)

instance IsOption LeanCheckTests where
  defaultValue :: LeanCheckTests
defaultValue = Int -> LeanCheckTests
LeanCheckTests Int
200
  parseValue :: String -> Maybe LeanCheckTests
parseValue = (Int -> LeanCheckTests) -> Maybe Int -> Maybe LeanCheckTests
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> LeanCheckTests
LeanCheckTests (Maybe Int -> Maybe LeanCheckTests)
-> (String -> Maybe Int) -> String -> Maybe LeanCheckTests
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe Int
forall a. Read a => String -> Maybe a
safeRead
  optionName :: Tagged LeanCheckTests String
optionName = String -> Tagged LeanCheckTests String
forall (m :: * -> *) a. Monad m => a -> m a
return String
"leancheck-tests"
  optionHelp :: Tagged LeanCheckTests String
optionHelp = String -> Tagged LeanCheckTests String
forall (m :: * -> *) a. Monad m => a -> m a
return String
"Depth to use for leancheck tests"

instance IsTest Results where
  testOptions :: Tagged Results [OptionDescription]
testOptions = [OptionDescription] -> Tagged Results [OptionDescription]
forall (m :: * -> *) a. Monad m => a -> m a
return [Proxy LeanCheckTests -> OptionDescription
forall v. IsOption v => Proxy v -> OptionDescription
Option (Proxy LeanCheckTests
forall k (t :: k). Proxy t
Proxy :: Proxy LeanCheckTests)]
  run :: OptionSet -> Results -> (Progress -> IO ()) -> IO Result
run OptionSet
opts Results
results Progress -> IO ()
_ = Int -> Results -> IO Result
resultIO Int
m Results
results IO Result -> (Result -> IO Result) -> IO Result
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Result
r -> Result -> IO Result
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result -> IO Result) -> Result -> IO Result
forall a b. (a -> b) -> a -> b
$
    case Result
r of
    OK Int
n             -> String -> Result
testPassed (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ String
"+++ OK, passed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests"
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Char
_ -> Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m) String
" (exhausted)"
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    Falsified Int
i [String]
ce   -> String -> Result
testFailed (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ String
"*** Failed! Falsifiable (after "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests):\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
joinArgs [String]
ce
    Exception Int
i [String]
ce String
e -> String -> Result
testFailed (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ String
"*** Failed! Exception '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' (after " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests):\n"
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
joinArgs [String]
ce
    where
    LeanCheckTests Int
m = OptionSet -> LeanCheckTests
forall v. IsOption v => OptionSet -> v
lookupOption OptionSet
opts

resultsIO :: Int -> Results -> [IO Result]
resultsIO :: Int -> Results -> [IO Result]
resultsIO Int
n (Results [([String], Bool)]
results) = (Int -> ([String], Bool) -> IO Result)
-> [Int] -> [([String], Bool)] -> [IO Result]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ([String], Bool) -> IO Result
torio [Int
1..] ([([String], Bool)] -> [IO Result])
-> [([String], Bool)] -> [IO Result]
forall a b. (a -> b) -> a -> b
$ Int -> [([String], Bool)] -> [([String], Bool)]
forall a. Int -> [a] -> [a]
take Int
n [([String], Bool)]
results
  where
    tor :: Int -> ([String], Bool) -> Result
tor Int
i ([String]
_,Bool
True) = Int -> Result
OK Int
i
    tor Int
i ([String]
as,Bool
False) = Int -> [String] -> Result
Falsified Int
i [String]
as
    torio :: Int -> ([String], Bool) -> IO Result
torio Int
i r :: ([String], Bool)
r@([String]
as,Bool
_) = Result -> IO Result
forall a. a -> IO a
evaluate (Int -> ([String], Bool) -> Result
tor Int
i ([String], Bool)
r)
       IO Result -> (SomeException -> IO Result) -> IO Result
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \SomeException
e -> let SomeException
_ = SomeException
e :: SomeException
                     in Result -> IO Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [String] -> String -> Result
Exception Int
i [String]
as (SomeException -> String
forall a. Show a => a -> String
show SomeException
e))

resultIO :: Int -> Results -> IO Result
resultIO :: Int -> Results -> IO Result
resultIO Int
n = [IO Result] -> IO Result
forall (m :: * -> *). Monad m => [m Result] -> m Result
computeResult ([IO Result] -> IO Result)
-> (Results -> [IO Result]) -> Results -> IO Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Results -> [IO Result]
resultsIO Int
n
  where
  computeResult :: [m Result] -> m Result
computeResult []  = String -> m Result
forall a. HasCallStack => String -> a
error String
"resultIO: no results, empty Listable enumeration?"
  computeResult [m Result
r] = m Result
r
  computeResult (m Result
r:[m Result]
rs) = m Result
r m Result -> (Result -> m Result) -> m Result
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Result
r -> case Result
r of
                                     (OK Int
_) -> [m Result] -> m Result
computeResult [m Result]
rs
                                     Result
_      -> Result -> m Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
r

-- joins the counter-example arguments
joinArgs :: [String] -> String
joinArgs :: [String] -> String
joinArgs [String]
ce | (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char
'\n' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) [String]
ce = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
chopBreak [String]
ce
            | Bool
otherwise            = [String] -> String
unwords [String]
ce

-- chops a line break at the end if there is any
chopBreak :: String -> String
chopBreak :: ShowS
chopBreak [] = []
chopBreak [Char
'\n'] = []
chopBreak (Char
x:String
xs) = Char
xChar -> ShowS
forall a. a -> [a] -> [a]
:ShowS
chopBreak String
xs