#if __GLASGOW_HASKELL__ >= 800
#endif
module Test.HUnit.DejaFu
(
testAuto
, testDejafu
, testDejafus
, testAutoWay
, testDejafuWay
, testDejafusWay
, testDejafuDiscard
, testAutoIO
, testDejafuIO
, testDejafusIO
, testAutoWayIO
, testDejafuWayIO
, testDejafusWayIO
, testDejafuDiscardIO
, Way
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, Bounds(..)
, defaultBounds
, MemType(..)
, defaultMemType
, Discard(..)
, defaultDiscarder
, testProperty
, R.Sig(..)
, R.RefinementProperty
, R.Testable(..)
, R.Listable(..)
, R.expectFailure
, R.refines, (R.=>=)
, R.strictlyRefines, (R.->-)
, R.equivalentTo, (R.===)
) where
import Control.Monad.Catch (try)
import Control.Monad.ST (runST)
import qualified Data.Foldable as F
import Data.List (intercalate, intersperse)
import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT
import Test.HUnit (Assertable(..), Test(..), Testable(..),
assertFailure, assertString)
import Test.HUnit.Lang (HUnitFailure(..))
import Unsafe.Coerce (unsafeCoerce)
runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
runSCTio = SCT.runSCTDiscard
instance Testable (Conc.ConcST t ()) where
test conc = TestCase (assert conc)
instance Testable (Conc.ConcIO ()) where
test conc = TestCase (assert conc)
instance Assertable (Conc.ConcST t ()) where
assert conc = do
let traces = runSCTst' conc'
assertString . showErr $ assertableP traces
where
conc' :: Conc.ConcST t (Either HUnitFailure ())
conc' = try conc
runSCTst' :: Conc.ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Conc.Trace)]
runSCTst' = unsafeCoerce $ runSCTst (const Nothing) defaultWay defaultMemType
instance Assertable (Conc.ConcIO ()) where
assert conc = do
traces <- runSCTio (const Nothing) defaultWay defaultMemType (try conc)
assertString . showErr $ assertableP traces
assertableP :: Predicate (Either HUnitFailure ())
assertableP = alwaysTrue $ \r -> case r of
Right (Left HUnitFailure {}) -> False
_ -> True
testAuto :: (Eq a, Show a)
=> (forall t. Conc.ConcST t a)
-> Test
testAuto = testAutoWay defaultWay defaultMemType
testAutoWay :: (Eq a, Show a)
=> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> Test
testAutoWay way memtype conc =
testDejafusWay way memtype conc autocheckCases
testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> Test
testAutoIO = testAutoWayIO defaultWay defaultMemType
testAutoWayIO :: (Eq a, Show a)
=> Way -> MemType -> Conc.ConcIO a -> Test
testAutoWayIO way memtype concio =
testDejafusWayIO way memtype concio autocheckCases
autocheckCases :: Eq a => [(String, Predicate a)]
autocheckCases =
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
]
testDejafu :: Show a
=> (forall t. Conc.ConcST t a)
-> String
-> Predicate a
-> Test
testDejafu = testDejafuWay defaultWay defaultMemType
testDejafuWay :: Show a
=> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> String
-> Predicate a
-> Test
testDejafuWay = testDejafuDiscard (const Nothing)
testDejafuDiscard :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> String
-> Predicate a
-> Test
testDejafuDiscard discard way memtype conc name test =
testst discard way memtype conc [(name, test)]
testDejafus :: Show a
=> (forall t. Conc.ConcST t a)
-> [(String, Predicate a)]
-> Test
testDejafus = testDejafusWay defaultWay defaultMemType
testDejafusWay :: Show a
=> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> [(String, Predicate a)]
-> Test
testDejafusWay = testst (const Nothing)
testDejafuIO :: Show a => Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuIO = testDejafuWayIO defaultWay defaultMemType
testDejafuWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuWayIO = testDejafuDiscardIO (const Nothing)
testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
testDejafuDiscardIO discard way memtype concio name test =
testio discard way memtype concio [(name, test)]
testDejafusIO :: Show a => Conc.ConcIO a -> [(String, Predicate a)] -> Test
testDejafusIO = testDejafusWayIO defaultWay defaultMemType
testDejafusWayIO :: Show a
=> Way -> MemType -> Conc.ConcIO a -> [(String, Predicate a)] -> Test
testDejafusWayIO = testio (const Nothing)
testProperty :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> String
-> p
-> Test
testProperty = testprop
testst :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> (forall t. Conc.ConcST t a)
-> [(String, Predicate a)]
-> Test
testst discard way memtype conc tests = case map toTest tests of
[t] -> t
ts -> TestList ts
where
toTest (name, p) = TestLabel name . TestCase $
assertString . showErr $ p traces
traces = runSCTst discard way memtype conc
testio :: Show a
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> Conc.ConcIO a
-> [(String, Predicate a)]
-> Test
testio discard way memtype concio tests = case map toTest tests of
[t] -> t
ts -> TestList ts
where
toTest (name, p) = TestLabel name . TestCase $ do
traces <- runSCTio discard way memtype concio
assertString . showErr $ p traces
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> String -> p -> Test
testprop name p = TestLabel name . TestCase $ do
ce <- R.check' p
case ce of
Just c -> assertFailure . init $ unlines
[ "*** Failure: " ++
(if null (R.failingArgs c) then "" else unwords (R.failingArgs c) ++ " ") ++
"(seed " ++ show (R.failingSeed c) ++ ")"
, " left: " ++ show (F.toList $ R.leftResults c)
, " right: " ++ show (F.toList $ R.rightResults c)
]
Nothing -> pure ()
showErr :: Show a => Result a -> String
showErr res
| _pass res = ""
| otherwise = "Failed after " ++ show (_casesChecked res) ++ " cases:\n" ++ msg ++ unlines failures ++ rest where
msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
failures = intersperse "" . map (indent . showres) . take 5 $ _failures res
showres (r, t) = either Conc.showFail show r ++ " " ++ Conc.showTrace t
rest = if moreThan (_failures res) 5 then "\n\t..." else ""
moreThan :: [a] -> Int -> Bool
moreThan [] n = n < 0
moreThan _ 0 = True
moreThan (_:xs) n = moreThan xs (n1)
indent :: String -> String
indent = intercalate "\n" . map ('\t':) . lines