{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
module Test.HUnit.DejaFu
(
testAuto
, testDejafu
, testDejafus
, testAutoWay
, testDejafuWay
, testDejafusWay
, testAutoWithSettings
, testDejafuWithSettings
, testDejafusWithSettings
, Condition
, Predicate
, ProPredicate(..)
, module Test.DejaFu.Settings
, Program
, Basic
, ConcT
, ConcIO
, WithSetup
, WithSetupAndTeardown
, withSetup
, withTeardown
, withSetupAndTeardown
, Invariant
, registerInvariant
, inspectIORef
, inspectMVar
, inspectTVar
, testProperty
, testPropertyFor
, 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 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 qualified Test.DejaFu.Settings
import qualified Test.DejaFu.Types as D
import Test.HUnit (Assertable(..), Test(..), Testable(..),
assertFailure, assertString)
import Test.HUnit.Lang (HUnitFailure(..))
instance Testable (Conc.ConcIO ()) where
test conc = TestCase (assert conc)
instance Assertable (Conc.ConcIO ()) where
assert conc = do
traces <- SCT.runSCTWithSettings (set ldiscard (Just (pdiscard assertableP)) defaultSettings) (try conc)
assertString . showErr $ peval assertableP traces
assertableP :: Predicate (Either HUnitFailure ())
assertableP = alwaysTrue $ \case
Right (Left HUnitFailure {}) -> False
_ -> True
testAuto :: (Eq a, Show a)
=> Program pty IO a
-> Test
testAuto = testAutoWithSettings defaultSettings
testAutoWay :: (Eq a, Show a)
=> Way
-> MemType
-> Program pty IO a
-> Test
testAutoWay way = testAutoWithSettings . fromWayAndMemType way
testAutoWithSettings :: (Eq a, Show a)
=> Settings IO a
-> Program pty IO a
-> Test
testAutoWithSettings settings = testDejafusWithSettings settings
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
]
testDejafu :: Show b
=> String
-> ProPredicate a b
-> Program pty IO a
-> Test
testDejafu = testDejafuWithSettings defaultSettings
testDejafuWay :: Show b
=> Way
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> Test
testDejafuWay way = testDejafuWithSettings . fromWayAndMemType way
testDejafuWithSettings :: Show b
=> Settings IO a
-> String
-> ProPredicate a b
-> Program p IO a
-> Test
testDejafuWithSettings settings name p = testDejafusWithSettings settings [(name, p)]
testDejafus :: Show b
=> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testDejafus = testDejafusWithSettings defaultSettings
testDejafusWay :: Show b
=> Way
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testDejafusWay way = testDejafusWithSettings . fromWayAndMemType way
testDejafusWithSettings :: Show b
=> Settings IO a
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testDejafusWithSettings = testconc
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 = testPropertyFor 10 100
testPropertyFor :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> Int
-> Int
-> String
-> p
-> Test
testPropertyFor = testprop
testconc :: Show b
=> Settings IO a
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testconc settings tests concio = case map toTest tests of
[t] -> t
ts -> TestList ts
where
toTest (name, p) = TestLabel name . TestCase $ do
let discarder = maybe id D.strengthenDiscard (get ldiscard settings) (pdiscard p)
traces <- SCT.runSCTWithSettings (set ldiscard (Just discarder) settings) concio
assertString . showErr $ peval p traces
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> Int -> Int -> String -> p -> Test
testprop sn vn name p = TestLabel name . TestCase $ do
ce <- R.checkFor sn vn 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:\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.showCondition 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 (n-1)
indent :: String -> String
indent = intercalate "\n" . map ('\t':) . lines