barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-11-05 06:45:08 +03:00
Code Issues Projects Releases Wiki Activity

Wrap predicate functions in a newtype & separate ty params

Browse Source 
Also adds a Functor and Profunctor instance for predicates.  The old
predicate type is kept as an alias for the (common) case where both
tyvars are the same.
This commit is contained in:
Michael Walker 2017-11-08 00:34:43 +00:00
parent 3348c4705c
commit 6eaae0a589
9 changed files with 198 additions and 141 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
dejafu-tests/Common.hs
View File

@ -11,7 +11,7 @@ import qualified Control.Monad.Catch as C
import Control.Monad.Conc.Class
import Control.Monad.STM.Class
import System.Random (mkStdGen)
import Test.DejaFu (Predicate, Failure, Result(..), alwaysTrue)
import Test.DejaFu (Predicate, ProPredicate(..), Failure, Result(..), alwaysTrue)
import Test.DejaFu.Conc (ConcIO)
import qualified Test.Framework as TF
import Test.Framework.Providers.HUnit (hUnitTestToTests)
@ -108,6 +108,8 @@ newTVarInt = newTVar
-- | A test which should fail.
failing :: Predicate a -> Predicate a
failing p as =
let result = p as
in result { _pass = not (_pass result) }
failing p = p
{ peval = \xs ->
let result = peval p xs
in result { _pass = not (_pass result) }
}

8
dejafu-tests/Examples/SearchParty.hs
View File

@ -28,21 +28,19 @@ import Test.Framework.Providers.HUnit (hUnitTestToTests)
import Test.HUnit (test)
import Test.HUnit.DejaFu (testDejafu)
import Common
import Examples.SearchParty.Impredicative
tests :: [Test]
tests = hUnitTestToTests $ test
[ testDejafu concFilter "concurrent filter" (invPred checkResultLists)
[ testDejafu concFilter "concurrent filter" (failing checkResultLists)
]
-- | Filter a list concurrently.
concFilter :: MonadConc m => m [Int]
concFilter = unsafeRunFind $ [0..5] @! const True
-- | Invert the result of a predicate.
invPred :: Predicate a -> Predicate a
invPred p xs = let r = p xs in r { _pass = not (_pass r) }
-- | Check that two lists of results are equal, modulo order.
checkResultLists :: Eq a => Predicate [a]
checkResultLists = alwaysTrue2 checkLists where

6
dejafu/CHANGELOG.markdown
View File

@ -23,6 +23,12 @@ This project is versioned according to the [Package Versioning Policy](https://p
- The `autocheckIO`, `dejafuIO`, `dejafusIO`, `autocheckWayIO`, `dejafuWayIO`, `dejafusWayIO`,
`dejafuDiscardIO`, `runTestM`, and `runTestWayM` functions are now gone.
- The `Predicate` type has been replaced with a more general `ProPredicate` type which is a
profunctor. (#124)
All testing functions have been generalised to take a `ProPredicate` instead. The `Predicate a`
type remains as an alias for `ProPredicate a a`.
### Test.DejaFu.Common
- New `ForkOS` and `IsCurrentThreadBound` thread actions. (#126)

250
dejafu/Test/DejaFu.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-- |
@ -6,7 +7,7 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : MultiParamTypeClasses
-- Portability : LambdaCase, MultiParamTypeClasses
--
-- Deterministic testing for concurrent computations.
--
@ -223,6 +224,7 @@ module Test.DejaFu
-- results.
, Predicate
, ProPredicate(..)
, representative
, abortsNever
, abortsAlways
@ -285,6 +287,7 @@ import Control.Monad.Ref (MonadRef)
import Data.Function (on)
import Data.List (intercalate, intersperse, minimumBy)
import Data.Ord (comparing)
import Data.Profunctor (Profunctor(..))
import Test.DejaFu.Common
import Test.DejaFu.Conc
@ -344,10 +347,10 @@ autocheckCases =
-- if it passes.
--
-- @since 1.0.0.0
dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-> (String, ProPredicate a b)
-- ^ The predicate (with a name) to check
-> n Bool
dejafu = dejafuWay defaultWay defaultMemType
@ -356,14 +359,14 @@ dejafu = dejafuWay defaultWay defaultMemType
-- memory model.
--
-- @since 1.0.0.0
dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-> (String, ProPredicate a b)
-- ^ The predicate (with a name) to check
-> n Bool
dejafuWay = dejafuDiscard (const Nothing)
@ -371,7 +374,7 @@ dejafuWay = dejafuDiscard (const Nothing)
-- | Variant of 'dejafuWay' which can selectively discard results.
--
-- @since 1.0.0.0
dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> Way
@ -380,21 +383,21 @@ dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> ConcT r n a
-- ^ The computation to test
-> (String, Predicate a)
-> (String, ProPredicate a b)
-- ^ The predicate (with a name) to check
-> n Bool
dejafuDiscard discard way memtype conc (name, test) = do
traces <- runSCTDiscard discard way memtype conc
liftIO $ doTest name (test traces)
liftIO $ doTest name (peval test traces)
-- | Variant of 'dejafu' which takes a collection of predicates to
-- test, returning 'True' if all pass.
--
-- @since 1.0.0.0
dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> ConcT r n a
-- ^ The computation to test
-> [(String, Predicate a)]
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> n Bool
dejafus = dejafusWay defaultWay defaultMemType
@ -403,19 +406,19 @@ dejafus = dejafusWay defaultWay defaultMemType
-- memory model.
--
-- @since 1.0.0.0
dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show a)
dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b)
=> Way
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> ConcT r n a
-- ^ The computation to test
-> [(String, Predicate a)]
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> n Bool
dejafusWay way memtype conc tests = do
traces <- runSCT way memtype conc
results <- mapM (\(name, test) -> liftIO . doTest name $ test traces) tests
results <- mapM (\(name, test) -> liftIO . doTest name $ peval test traces) tests
pure (and results)
@ -464,11 +467,11 @@ instance Foldable Result where
--
-- @since 1.0.0.0
runTest :: (MonadConc n, MonadRef r n)
=> Predicate a
=> ProPredicate a b
-- ^ The predicate to check
-> ConcT r n a
-- ^ The computation to test
-> n (Result a)
-> n (Result b)
runTest = runTestWay defaultWay defaultMemType
-- | Variant of 'runTest' which takes a way to run the program and a
@ -480,100 +483,124 @@ runTestWay :: (MonadConc n, MonadRef r n)
-- ^ How to run the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> ConcT r n a
-- ^ The computation to test
-> n (Result a)
-> n (Result b)
runTestWay way memtype predicate conc =
predicate <$> runSCT way memtype conc
peval predicate <$> runSCT way memtype conc
-------------------------------------------------------------------------------
-- Predicates
-- | A @Predicate@ is a function which collapses a list of results
-- into a 'Result'.
-- into a 'Result', possibly discarding some on the way.
--
-- @since 0.1.0.0
type Predicate a = [(Either Failure a, Trace)] -> Result a
-- @Predicate@ cannot be a functor as the type parameter is used both
-- co- and contravariantly.
--
-- @since 1.0.0.0
type Predicate a = ProPredicate a a
-- | Reduce the list of failures in a @Predicate@ to one
-- | A @ProPredicate@ is a function which collapses a list of results
-- into a 'Result', possibly discarding some on the way.
--
-- @since 1.0.0.0
newtype ProPredicate a b = ProPredicate
{ peval :: [(Either Failure a, Trace)] -> Result b
-- ^ Compute the result with the un-discarded results.
}
instance Profunctor ProPredicate where
dimap f g p = ProPredicate
{ peval = fmap g . peval p . map (first (fmap f))
}
instance Functor (ProPredicate x) where
fmap = dimap id
-- | Reduce the list of failures in a @ProPredicate@ to one
-- representative trace for each unique result.
--
-- This may throw away \"duplicate\" failures which have a unique
-- cause but happen to manifest in the same way. However, it is
-- convenient for filtering out true duplicates.
--
-- @since 0.2.0.0
representative :: Eq a => Predicate a -> Predicate a
representative p xs = result { _failures = choose . collect $ _failures result } where
result = p xs
collect = groupBy' [] ((==) `on` fst)
choose = map $ minimumBy (comparing $ \(_, trc) -> (preEmps trc, length trc))
-- @since 1.0.0.0
representative :: Eq b => ProPredicate a b -> ProPredicate a b
representative p = p
{ peval = \xs ->
let result = peval p xs
in result { _failures = choose . collect $ _failures result }
}
where
collect = groupBy' [] ((==) `on` fst)
choose = map $ minimumBy (comparing $ \(_, trc) -> (preEmps trc, length trc))
preEmps trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)
preEmps trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)
groupBy' res _ [] = res
groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys
groupBy' res _ [] = res
groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys
insert' _ x [] = [[x]]
insert' eq x (ys@(y:_):yss)
| x `eq` y = (x:ys) : yss
| otherwise = ys : insert' eq x yss
insert' _ _ ([]:_) = undefined
insert' _ x [] = [[x]]
insert' eq x (ys@(y:_):yss)
| x `eq` y = (x:ys) : yss
| otherwise = ys : insert' eq x yss
insert' _ _ ([]:_) = undefined
-- | Check that a computation never aborts.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
abortsNever :: Predicate a
abortsNever = alwaysTrue (not . either (==Abort) (const False))
-- | Check that a computation always aborts.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
abortsAlways :: Predicate a
abortsAlways = alwaysTrue $ either (==Abort) (const False)
-- | Check that a computation aborts at least once.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
abortsSometimes :: Predicate a
abortsSometimes = somewhereTrue $ either (==Abort) (const False)
-- | Check that a computation never deadlocks.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
deadlocksNever :: Predicate a
deadlocksNever = alwaysTrue (not . either isDeadlock (const False))
-- | Check that a computation always deadlocks.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
deadlocksAlways :: Predicate a
deadlocksAlways = alwaysTrue $ either isDeadlock (const False)
-- | Check that a computation deadlocks at least once.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
deadlocksSometimes :: Predicate a
deadlocksSometimes = somewhereTrue $ either isDeadlock (const False)
-- | Check that a computation never fails with an uncaught exception.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
exceptionsNever :: Predicate a
exceptionsNever = alwaysTrue (not . either isUncaughtException (const False))
-- | Check that a computation always fails with an uncaught exception.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
exceptionsAlways :: Predicate a
exceptionsAlways = alwaysTrue $ either isUncaughtException (const False)
-- | Check that a computation fails with an uncaught exception at least once.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
exceptionsSometimes :: Predicate a
exceptionsSometimes = somewhereTrue $ either isUncaughtException (const False)
@ -581,36 +608,43 @@ exceptionsSometimes = somewhereTrue $ either isUncaughtException (const False)
-- particular this means either: (a) it always fails in the same way,
-- or (b) it never fails and the values returned are all equal.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
alwaysSame :: Eq a => Predicate a
alwaysSame = representative $ alwaysTrue2 (==)
-- | Check that the result of a computation is not always the same.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
notAlwaysSame :: Eq a => Predicate a
notAlwaysSame [x] = (defaultFail [x]) { _casesChecked = 1 }
notAlwaysSame xs = go xs $ defaultFail [] where
go [y1,y2] res
| fst y1 /= fst y2 = incCC res { _pass = True }
| otherwise = incCC res { _failures = y1 : y2 : _failures res }
go (y1:y2:ys) res
| fst y1 /= fst y2 = go (y2:ys) . incCC $ res { _pass = True }
| otherwise = go (y2:ys) . incCC $ res { _failures = y1 : y2 : _failures res }
go _ res = res
notAlwaysSame = ProPredicate
{ peval = \case
[x] -> defaultFail [x]
xs -> go xs (defaultFail [])
}
where
go [y1,y2] res
| fst y1 /= fst y2 = incCC res { _pass = True }
| otherwise = incCC res { _failures = y1 : y2 : _failures res }
go (y1:y2:ys) res
| fst y1 /= fst y2 = go (y2:ys) . incCC $ res { _pass = True }
| otherwise = go (y2:ys) . incCC $ res { _failures = y1 : y2 : _failures res }
go _ res = res
-- | Check that the result of a unary boolean predicate is always
-- true.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
alwaysTrue :: (Either Failure a -> Bool) -> Predicate a
alwaysTrue p xs = go xs $ (defaultFail failures) { _pass = True } where
go (y:ys) res
| p (fst y) = go ys . incCC $ res
| otherwise = incCC $ res { _pass = False }
go [] res = res
alwaysTrue p = ProPredicate
{ peval = \xs -> go xs $ (defaultFail (failures xs)) { _pass = True }
}
where
go (y:ys) res
| p (fst y) = go ys . incCC $ res
| otherwise = incCC $ res { _pass = False }
go [] res = res
failures = filter (not . p . fst) xs
failures = filter (not . p . fst)
-- | Check that the result of a binary boolean predicate is true
-- between all pairs of results. Only properties which are transitive
@ -619,67 +653,77 @@ alwaysTrue p xs = go xs $ (defaultFail failures) { _pass = True } where
-- If the predicate fails, /both/ (result,trace) tuples will be added
-- to the failures list.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a
alwaysTrue2 _ [_] = defaultPass { _casesChecked = 1 }
alwaysTrue2 p xs = go xs $ defaultPass { _failures = failures } where
go [y1,y2] res
| p (fst y1) (fst y2) = incCC res
| otherwise = incCC res { _pass = False }
go (y1:y2:ys) res
| p (fst y1) (fst y2) = go (y2:ys) . incCC $ res
| otherwise = go (y2:ys) . incCC $ res { _pass = False }
go _ res = res
alwaysTrue2 p = ProPredicate
{ peval = \case
[_] -> defaultPass
xs -> go xs $ defaultPass { _failures = failures xs }
}
where
go [y1,y2] res
| p (fst y1) (fst y2) = incCC res
| otherwise = incCC res { _pass = False }
go (y1:y2:ys) res
| p (fst y1) (fst y2) = go (y2:ys) . incCC $ res
| otherwise = go (y2:ys) . incCC $ res { _pass = False }
go _ res = res
failures = fgo xs where
fgo (y1:y2:ys)
| p (fst y1) (fst y2) = fgo (y2:ys)
| otherwise = y1 : y2 : fgo2 y2 ys
fgo _ = []
failures = fgo where
fgo (y1:y2:ys)
| p (fst y1) (fst y2) = fgo (y2:ys)
| otherwise = y1 : y2 : fgo2 y2 ys
fgo _ = []
fgo2 y1 (y2:ys)
| p (fst y1) (fst y2) = fgo (y2:ys)
| otherwise = y2 : fgo2 y2 ys
fgo2 _ _ = []
fgo2 y1 (y2:ys)
| p (fst y1) (fst y2) = fgo (y2:ys)
| otherwise = y2 : fgo2 y2 ys
fgo2 _ _ = []
-- | Check that the result of a unary boolean predicate is true at
-- least once.
--
-- @since 0.1.0.0
-- @since 1.0.0.0
somewhereTrue :: (Either Failure a -> Bool) -> Predicate a
somewhereTrue p xs = go xs $ defaultFail failures where
go (y:ys) res
| p (fst y) = incCC $ res { _pass = True }
| otherwise = go ys . incCC $ res { _failures = y : _failures res }
go [] res = res
somewhereTrue p = ProPredicate
{ peval = \xs -> go xs $ defaultFail (failures xs)
}
where
go (y:ys) res
| p (fst y) = incCC $ res { _pass = True }
| otherwise = go ys . incCC $ res { _failures = y : _failures res }
go [] res = res
failures = filter (not . p . fst) xs
failures = filter (not . p . fst)
-- | Predicate for when there is a known set of results where every
-- result must be exhibited at least once.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a
gives expected results = go expected [] results $ defaultFail failures where
go waitingFor alreadySeen ((x, _):xs) res
-- If it's a result we're waiting for, move it to the
-- @alreadySeen@ list and continue.
| x `elem` waitingFor = go (filter (/=x) waitingFor) (x:alreadySeen) xs res { _casesChecked = _casesChecked res + 1 }
gives expected = ProPredicate
{ peval = \xs -> go expected [] xs $ defaultFail (failures xs)
}
where
go waitingFor alreadySeen ((x, _):xs) res
-- If it's a result we're waiting for, move it to the
-- @alreadySeen@ list and continue.
| x `elem` waitingFor = go (filter (/=x) waitingFor) (x:alreadySeen) xs res { _casesChecked = _casesChecked res + 1 }
-- If it's a result we've already seen, continue.
| x `elem` alreadySeen = go waitingFor alreadySeen xs res { _casesChecked = _casesChecked res + 1 }
-- If it's a result we've already seen, continue.
| x `elem` alreadySeen = go waitingFor alreadySeen xs res { _casesChecked = _casesChecked res + 1 }
-- If it's not a result we expected, fail.
| otherwise = res { _casesChecked = _casesChecked res + 1 }
-- If it's not a result we expected, fail.
| otherwise = res { _casesChecked = _casesChecked res + 1 }
go [] _ [] res = res { _pass = True }
go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es }
go [] _ [] res = res { _pass = True }
go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es }
failures = filter (\(r, _) -> r `notElem` expected) results
failures = filter (\(r, _) -> r `notElem` expected)
-- | Variant of 'gives' that doesn't allow for expected failures.
--
-- @since 0.2.0.0
-- @since 1.0.0.0
gives' :: (Eq a, Show a) => [a] -> Predicate a
gives' = gives . map Right

3
dejafu/dejafu.cabal
View File

@ -64,9 +64,10 @@ library
, deepseq >=1.1 && <2
, exceptions >=0.7 && <0.9
, leancheck >=0.6 && <0.8
, profunctors >=4.0 && <6.0
, random >=1.0 && <1.2
, ref-fd >=0.4 && <0.5
, transformers >=0.4 && <0.6
, transformers >=0.4 && <0.6
-- hs-source-dirs:
default-language: Haskell2010
ghc-options: -Wall

1
hunit-dejafu/CHANGELOG.markdown
View File

@ -18,6 +18,7 @@ This project is versioned according to the [Package Versioning Policy](https://p
- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
- The `Testable` and `Assertable` instances for `ConcST t ()` are gone.
- All test functions are generalised to take a `ProPredicate`.
### Miscellaneous

30
hunit-dejafu/Test/HUnit/DejaFu.hs
View File

@ -37,6 +37,8 @@ module Test.HUnit.DejaFu
, testDejafuDiscard
-- ** Re-exports
, Predicate
, ProPredicate(..)
, Way
, defaultWay
, systematically
@ -87,7 +89,7 @@ instance Testable (Conc.ConcIO ()) where
instance Assertable (Conc.ConcIO ()) where
assert conc = do
traces <- SCT.runSCTDiscard (const Nothing) defaultWay defaultMemType (try conc)
assertString . showErr $ assertableP traces
assertString . showErr $ peval assertableP traces
assertableP :: Predicate (Either HUnitFailure ())
assertableP = alwaysTrue $ \case
@ -134,12 +136,12 @@ autocheckCases =
-- | Check that a predicate holds.
--
-- @since 1.0.0.0
testDejafu :: Show a
testDejafu :: Show b
=> Conc.ConcIO a
-- ^ The computation to test
-> String
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> Test
testDejafu = testDejafuWay defaultWay defaultMemType
@ -148,7 +150,7 @@ testDejafu = testDejafuWay defaultWay defaultMemType
-- and a memory model.
--
-- @since 1.0.0.0
testDejafuWay :: Show a
testDejafuWay :: Show b
=> Way
-- ^ How to execute the concurrent program.
-> MemType
@ -157,7 +159,7 @@ testDejafuWay :: Show a
-- ^ The computation to test
-> String
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> Test
testDejafuWay = testDejafuDiscard (const Nothing)
@ -165,7 +167,7 @@ testDejafuWay = testDejafuDiscard (const Nothing)
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
-- @since 1.0.0.0
testDejafuDiscard :: Show a
testDejafuDiscard :: Show b
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> Way
@ -176,7 +178,7 @@ testDejafuDiscard :: Show a
-- ^ The computation to test
-> String
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> Test
testDejafuDiscard discard way memtype conc name test =
@ -187,10 +189,10 @@ testDejafuDiscard discard way memtype conc name test =
-- running the concurrent computation many times for each predicate.
--
-- @since 1.0.0.0
testDejafus :: Show a
testDejafus :: Show b
=> Conc.ConcIO a
-- ^ The computation to test
-> [(String, Predicate a)]
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> Test
testDejafus = testDejafusWay defaultWay defaultMemType
@ -199,14 +201,14 @@ testDejafus = testDejafusWay defaultWay defaultMemType
-- and a memory model.
--
-- @since 1.0.0.0
testDejafusWay :: Show a
testDejafusWay :: Show b
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> Conc.ConcIO a
-- ^ The computation to test
-> [(String, Predicate a)]
-> [(String, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> Test
testDejafusWay = testconc (const Nothing)
@ -250,12 +252,12 @@ testPropertyFor = testprop
-- HUnit integration
-- | Produce a HUnit 'Test' from a Deja Fu unit test.
testconc :: Show a
testconc :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> Conc.ConcIO a
-> [(String, Predicate a)]
-> [(String, ProPredicate a b)]
-> Test
testconc discard way memtype concio tests = case map toTest tests of
[t] -> t
@ -268,7 +270,7 @@ testconc discard way memtype concio tests = case map toTest tests of
-- (eg, constructing an 'MVar' to share the traces after one
-- test computed them).
traces <- SCT.runSCTDiscard discard way memtype concio
assertString . showErr $ p traces
assertString . showErr $ peval p traces
-- | Produce a HUnit 'Test' from a Deja Fu refinement property test.
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))

1
tasty-dejafu/CHANGELOG.markdown
View File

@ -18,6 +18,7 @@ This project is versioned according to the [Package Versioning Policy](https://p
- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
- The `IsTest` instance for `ConcST t (Maybe String)` is gone.
- All test functions are generalised to take a `ProPredicate`.
### Miscellaneous

30
tasty-dejafu/Test/Tasty/DejaFu.hs
View File

@ -37,6 +37,8 @@ module Test.Tasty.DejaFu
, testDejafuDiscard
-- ** Re-exports
, Predicate
, ProPredicate(..)
, Way
, defaultWay
, systematically
@ -166,12 +168,12 @@ autocheckCases =
-- | Check that a predicate holds.
--
-- @since 1.0.0.0
testDejafu :: Show a
testDejafu :: Show b
=> Conc.ConcIO a
-- ^ The computation to test
-> TestName
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> TestTree
testDejafu = testDejafuWay defaultWay defaultMemType
@ -180,7 +182,7 @@ testDejafu = testDejafuWay defaultWay defaultMemType
-- and a memory model.
--
-- @since 1.0.0.0
testDejafuWay :: Show a
testDejafuWay :: Show b
=> Way
-- ^ How to execute the concurrent program.
-> MemType
@ -189,7 +191,7 @@ testDejafuWay :: Show a
-- ^ The computation to test
-> TestName
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> TestTree
testDejafuWay = testDejafuDiscard (const Nothing)
@ -197,7 +199,7 @@ testDejafuWay = testDejafuDiscard (const Nothing)
-- | Variant of 'testDejafuWay' which can selectively discard results.
--
-- @since 1.0.0.0
testDejafuDiscard :: Show a
testDejafuDiscard :: Show b
=> (Either Failure a -> Maybe Discard)
-- ^ Selectively discard results.
-> Way
@ -208,7 +210,7 @@ testDejafuDiscard :: Show a
-- ^ The computation to test
-> String
-- ^ The name of the test.
-> Predicate a
-> ProPredicate a b
-- ^ The predicate to check
-> TestTree
testDejafuDiscard discard way memtype conc name test =
@ -219,10 +221,10 @@ testDejafuDiscard discard way memtype conc name test =
-- running the concurrent computation many times for each predicate.
--
-- @since 1.0.0.0
testDejafus :: Show a
testDejafus :: Show b
=> Conc.ConcIO a
-- ^ The computation to test
-> [(TestName, Predicate a)]
-> [(TestName, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> TestTree
testDejafus = testDejafusWay defaultWay defaultMemType
@ -231,14 +233,14 @@ testDejafus = testDejafusWay defaultWay defaultMemType
-- and a memory model.
--
-- @since 1.0.0.0
testDejafusWay :: Show a
testDejafusWay :: Show b
=> Way
-- ^ How to execute the concurrent program.
-> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> Conc.ConcIO a
-- ^ The computation to test
-> [(TestName, Predicate a)]
-> [(TestName, ProPredicate a b)]
-- ^ The list of predicates (with names) to check
-> TestTree
testDejafusWay = testconc (const Nothing)
@ -282,7 +284,7 @@ testPropertyFor = testprop
-- Tasty integration
data ConcTest where
ConcTest :: Show a => IO [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcTest
ConcTest :: Show b => IO [(Either Failure a, Conc.Trace)] -> ProPredicate a b -> ConcTest
deriving Typeable
data PropTest where
@ -294,7 +296,7 @@ instance IsTest ConcTest where
run _ (ConcTest iotraces p) _ = do
traces <- iotraces
let err = showErr $ p traces
let err = showErr $ peval p traces
pure (if null err then testPassed "" else testFailed err)
instance IsTest PropTest where
@ -313,12 +315,12 @@ instance IsTest PropTest where
Nothing -> testPassed ""
-- | Produce a Tasty 'Test' from a Deja Fu unit test.
testconc :: Show a
testconc :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> Conc.ConcIO a
-> [(TestName, Predicate a)]
-> [(TestName, ProPredicate a b)]
-> TestTree
testconc discard way memtype concio tests = case map toTest tests of
[t] -> t