barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-29 00:22:38 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #253 from barrucadu/210-discard-monoids

Browse Source 
Add weaken/strengthen monoids for discard functions
This commit is contained in:
Michael Walker 2018-04-29 01:38:09 +01:00 committed by GitHub
commit 7cd308f9dd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 202 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.markdown
View File

@ -46,7 +46,7 @@ There are a few different packages under the Déjà Fu umbrella:
| | Version | Summary |
| - | ------- | ------- |
| [concurrency][h:conc] | 1.5.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
| [dejafu][h:dejafu] | 1.5.0.0 | Systematic testing for Haskell concurrency. |
| [dejafu][h:dejafu] | 1.5.1.0 | Systematic testing for Haskell concurrency. |
| [hunit-dejafu][h:hunit] | 1.2.0.0 | Deja Fu support for the HUnit test framework. |
| [tasty-dejafu][h:tasty] | 1.2.0.0 | Deja Fu support for the Tasty test framework. |

1
dejafu-tests/dejafu-tests.cabal
View File

@ -49,6 +49,7 @@ library
, abstract-deque
, concurrency
, containers
, contravariant
, deepseq
, dejafu
, exceptions

6
dejafu-tests/lib/Common.hs
View File

@ -189,6 +189,12 @@ genFunction genKey genVal = (,) <$> genVal <*> genSmallMap genKey genVal
applyFunction :: Ord k => (v, Map.Map k v) -> k -> v
applyFunction (def, assocs) k = Map.findWithDefault def k assocs
genPair :: H.Gen a -> H.Gen (a, a)
genPair g = (,) <$> g <*> g
genEither :: H.Gen l -> H.Gen r -> H.Gen (Either l r)
genEither l r = HGen.choice [Left <$> l, Right <$> r]
-------------------------------------------------------------------------------
-- Utilities

120
dejafu-tests/lib/Unit/Properties.hs
View File

@ -1,20 +1,24 @@
{-# LANGUAGE TypeFamilies #-}
module Unit.Properties where
import qualified Control.Exception as E
import Control.Monad (zipWithM)
import qualified Control.Monad.Conc.Class as C
import Control.Monad.IO.Class (liftIO)
import qualified Data.Foldable as F
import qualified Data.Map as M
import qualified Data.Sequence as S
import qualified Hedgehog as H
import qualified Hedgehog.Gen as HGen
import qualified Test.DejaFu.Conc.Internal.Common as D
import qualified Test.DejaFu.Conc.Internal.Memory as Mem
import qualified Test.DejaFu.Internal as D
import qualified Test.DejaFu.SCT.Internal.DPOR as SCT
import qualified Test.DejaFu.Types as D
import qualified Control.Exception as E
import Control.Monad (zipWithM)
import qualified Control.Monad.Conc.Class as C
import Control.Monad.IO.Class (liftIO)
import Data.Coerce (coerce)
import qualified Data.Foldable as F
import Data.Functor.Contravariant (contramap)
import Data.Functor.Contravariant.Divisible (conquer, divide)
import qualified Data.Map as M
import Data.Semigroup ((<>))
import qualified Data.Sequence as S
import qualified Hedgehog as H
import qualified Hedgehog.Gen as HGen
import qualified Test.DejaFu.Conc.Internal.Common as D
import qualified Test.DejaFu.Conc.Internal.Memory as Mem
import qualified Test.DejaFu.Internal as D
import qualified Test.DejaFu.SCT.Internal.DPOR as SCT
import qualified Test.DejaFu.Types as D
import Common
@ -32,6 +36,8 @@ classLawProps :: [TestTree]
classLawProps = toTestList
[ testGroup "Id" (eqord genId)
, testGroup "Failure" (eqord genFailure)
, testGroup "Weaken" (discardf min D.getWeakDiscarder)
, testGroup "Strengthen" (discardf max D.getStrongDiscarder)
]
where
eqord gen =
@ -72,6 +78,80 @@ classLawProps = toTestList
H.assert (y <= x)
]
discardf choose extract =
[ testProperty "Associativity (<>)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
z <- coerce . applyFunction <$> H.forAll genDiscarder
x <> (y <> z) ==== (x <> y) <> z
, testProperty "Commutativity (<>)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
x <> y ==== y <> x
, testProperty "Unit (<>)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
x <> mempty ==== x
, testProperty "Homomorphism (<>)" $ do
let o d1 d2 efa = d1 efa `choose` d2 efa
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
efa <- H.forAll genEfa
extract (x <> y) efa H.=== (extract x `o` extract y) efa
, testProperty "Identity (contramap)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
contramap id x ==== x
, testProperty "Associativity (divide + delta)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
z <- coerce . applyFunction <$> H.forAll genDiscarder
divide delta (divide delta x y) z ==== divide delta x (divide delta y z)
, testProperty "Commutativity (divide + delta)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
divide delta x y ==== divide delta y x
, testProperty "Unit (divide + delta)" $ do
x <- coerce . applyFunction <$> H.forAll genDiscarder
divide delta x conquer ==== x
, testProperty "Generalised Associativity (divide)" $ do
let genF = genFunc (genPair genSmallInt)
f <- applyFunction <$> H.forAll genF
g <- applyFunction <$> H.forAll genF
x <- coerce . applyFunction <$> H.forAll genDiscarder
y <- coerce . applyFunction <$> H.forAll genDiscarder
z <- coerce . applyFunction <$> H.forAll genDiscarder
let f' a = let (bc, d) = f a; (b, c) = g bc in (b, (c, d))
divide f (divide g x y) z ==== divide f' x (divide id y z)
, testProperty "Divisible / Contravariant Consistency (fst)" $ do
let genF = genFunc (genPair genSmallInt)
f <- applyFunction <$> H.forAll genF
x <- coerce . applyFunction <$> H.forAll genDiscarder
divide f x conquer ==== contramap (fst . f) x
, testProperty "Divisible / Contravariant Consistency (snd)" $ do
let genF = genFunc (genPair genSmallInt)
f <- applyFunction <$> H.forAll genF
x <- coerce . applyFunction <$> H.forAll genDiscarder
divide f conquer x ==== contramap (snd . f) x
]
where
genFunc = genFunction genSmallInt
d1 ==== d2 = do
efa <- H.forAll genEfa
extract d1 efa H.=== extract d2 efa
infix 4 ====
delta x = (x, x)
-------------------------------------------------------------------------------
commonProps :: [TestTree]
@ -363,3 +443,15 @@ genDepState = SCT.DepState
<$> genSmallMap genCRefId HGen.bool
<*> genSmallSet genMVarId
<*> genSmallMap genThreadId genMaskingState
genDiscarder :: H.Gen (Function (Either D.Failure Int) (Maybe D.Discard))
genDiscarder = genFunction genEfa (HGen.maybe genDiscard)
genEfa :: H.Gen (Either D.Failure Int)
genEfa = genEither genFailure genSmallInt
genDiscard :: H.Gen D.Discard
genDiscard = HGen.element
[ D.DiscardTrace
, D.DiscardResultAndTrace
]

15
dejafu/CHANGELOG.rst
View File

@ -7,6 +7,21 @@ standard Haskell versioning scheme.
.. _PVP: https://pvp.haskell.org/
1.5.1.0 (2018-03-29)
--------------------
* Git: :tag:`dejafu-1.5.1.0`
* Hackage: :hackage:`dejafu-1.5.1.0`
Added
~~~~~
- (:issue:`210`) ``Test.DejaFu.Types.Weaken`` and ``Strengthen``
newtype wrappers around discard functions, with ``Semigroup``,
``Monoid``, ``Contravariant``, and ``Divisible`` instances
corresponding to ``weakenDiscard`` and ``strengthenDiscard``.
1.5.0.0 - No More 7.10 (2018-03-28)
-----------------------------------

89
dejafu/Test/DejaFu/Types.hs
View File

@ -1,5 +1,6 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
-- |
@ -8,16 +9,20 @@
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : DeriveGeneric, GeneralizedNewtypeDeriving, StandaloneDeriving
-- Portability : DeriveGeneric, GeneralizedNewtypeDeriving, LambdaCase, StandaloneDeriving
--
-- Common types and functions used throughout DejaFu.
module Test.DejaFu.Types where
import Control.DeepSeq (NFData(..))
import Control.Exception (Exception(..), MaskingState(..),
SomeException)
import Data.Function (on)
import GHC.Generics (Generic)
import Control.DeepSeq (NFData(..))
import Control.Exception (Exception(..),
MaskingState(..),
SomeException)
import Data.Function (on)
import Data.Functor.Contravariant (Contravariant(..))
import Data.Functor.Contravariant.Divisible (Divisible(..))
import Data.Semigroup (Semigroup(..))
import GHC.Generics (Generic)
-------------------------------------------------------------------------------
-- * Identifiers
@ -625,41 +630,85 @@ deriving instance Generic Discard
instance NFData Discard
-- | Combine two discard values, keeping the weaker.
-- | A monoid for discard functions: combines two functions, keeping
-- the weaker.
--
-- @Nothing@ is weaker than @Just DiscardTrace@, which is weaker than
-- @Just DiscardResultAndTrace@. This forms a commutative monoid
-- where the unit is @const (Just DiscardResultAndTrace)@.
--
-- @since 1.5.1.0
newtype Weaken a = Weaken
{ getWeakDiscarder :: Either Failure a -> Maybe Discard }
instance Semigroup (Weaken a) where
(<>) = divide (\efa -> (efa, efa))
instance Monoid (Weaken a) where
mempty = conquer
mappend = (<>)
instance Contravariant Weaken where
contramap f (Weaken d) = Weaken (d . fmap f)
instance Divisible Weaken where
divide f (Weaken d1) (Weaken d2) = Weaken $ \case
Right a ->
let (b, c) = f a
in min (d1 (Right b)) (d2 (Right c))
Left e -> min (d1 (Left e)) (d2 (Left e))
conquer = Weaken (const (Just DiscardResultAndTrace))
-- | Combine two discard functions, keeping the weaker.
--
-- @since 1.0.0.0
weakenDiscard ::
(Either Failure a -> Maybe Discard)
-> (Either Failure a -> Maybe Discard)
-> Either Failure a -> Maybe Discard
weakenDiscard d1 d2 efa = case (d1 efa, d2 efa) of
(Nothing, _) -> Nothing
(_, Nothing) -> Nothing
(Just DiscardTrace, _) -> Just DiscardTrace
(_, Just DiscardTrace) -> Just DiscardTrace
_ -> Just DiscardResultAndTrace
weakenDiscard d1 d2 =
getWeakDiscarder (Weaken d1 <> Weaken d2)
-- | Combine two discard functions, keeping the stronger.
-- | A monoid for discard functions: combines two functions, keeping
-- the stronger.
--
-- @Just DiscardResultAndTrace@ is stronger than @Just DiscardTrace@,
-- which is stronger than @Nothing@. This forms a commutative monoid
-- where the unit is @const Nothing@.
--
-- @since 1.5.1.0
newtype Strengthen a = Strengthen
{ getStrongDiscarder :: Either Failure a -> Maybe Discard }
instance Semigroup (Strengthen a) where
(<>) = divide (\efa -> (efa, efa))
instance Monoid (Strengthen a) where
mempty = conquer
mappend = (<>)
instance Contravariant Strengthen where
contramap f (Strengthen d) = Strengthen (d . fmap f)
instance Divisible Strengthen where
divide f (Strengthen d1) (Strengthen d2) = Strengthen $ \case
Right a ->
let (b, c) = f a
in max (d1 (Right b)) (d2 (Right c))
Left e -> max (d1 (Left e)) (d2 (Left e))
conquer = Strengthen (const Nothing)
-- | Combine two discard functions, keeping the stronger.
--
-- @since 1.0.0.0
strengthenDiscard ::
(Either Failure a -> Maybe Discard)
-> (Either Failure a -> Maybe Discard)
-> Either Failure a -> Maybe Discard
strengthenDiscard d1 d2 efa = case (d1 efa, d2 efa) of
(Just DiscardResultAndTrace, _) -> Just DiscardResultAndTrace
(_, Just DiscardResultAndTrace) -> Just DiscardResultAndTrace
(Just DiscardTrace, _) -> Just DiscardTrace
(_, Just DiscardTrace) -> Just DiscardTrace
_ -> Nothing
strengthenDiscard d1 d2 =
getStrongDiscarder (Strengthen d1 <> Strengthen d2)
-------------------------------------------------------------------------------
-- * Memory Models

5
dejafu/dejafu.cabal
View File

@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: dejafu
version: 1.5.0.0
version: 1.5.1.0
synopsis: A library for unit-testing concurrent programs.
description:
@ -33,7 +33,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/barrucadu/dejafu.git
tag: dejafu-1.5.0.0
tag: dejafu-1.5.1.0
library
exposed-modules: Test.DejaFu
@ -61,6 +61,7 @@ library
build-depends: base >=4.9 && <5
, concurrency >=1.5 && <1.6
, containers >=0.5 && <0.6
, contravariant >=1.2 && <1.5
, deepseq >=1.1 && <2
, exceptions >=0.7 && <0.11
, leancheck >=0.6 && <0.8

2
doc/getting_started.rst
View File

@ -28,7 +28,7 @@ There are a few different packages under the Déjà Fu umbrella:
:header: "Package", "Version", "Summary"
":hackage:`concurrency`", "1.5.0.0", "Typeclasses, functions, and data types for concurrency and STM"
":hackage:`dejafu`", "1.5.0.0", "Systematic testing for Haskell concurrency"
":hackage:`dejafu`", "1.5.1.0", "Systematic testing for Haskell concurrency"
":hackage:`hunit-dejafu`", "1.2.0.0", "Déjà Fu support for the HUnit test framework"
":hackage:`tasty-dejafu`", "1.2.0.0", "Déjà Fu support for the tasty test framework"