Skip to content

Commit

Permalink
TOREORDER extract non-discarding implies QuickCheck utility
Browse files Browse the repository at this point in the history
  • Loading branch information
amesgen committed Apr 25, 2024
1 parent 5e2893d commit 5779c0f
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 9 deletions.
Empty file.
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ import Test.Util.HardFork.Future (Future)
import Test.Util.Orphans.Arbitrary ()
import Test.Util.Orphans.IOLike ()
import Test.Util.Orphans.NoThunks ()
import Test.Util.QuickCheck
import Test.Util.Range
import Test.Util.Shrink (andId, dropId)
import Test.Util.Slots (NumSlots (..))
Expand Down Expand Up @@ -674,10 +675,6 @@ prop_general_internal syncity pga testOutput =
| ((s1, _, max1), (s2, min2, _)) <- orderedPairs extrema
]
where
-- QuickCheck's @==>@ 'discard's the test if @p1@ fails; that's not
-- what we want
implies p1 p2 = not p1 .||. p2

-- all pairs @(x, y)@ where @x@ precedes @y@ in the given list
orderedPairs :: [a] -> [(a, a)]
orderedPairs = \case
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ module Test.Util.QuickCheck (
-- * Convenience
, collects
, forAllGenRunShrinkCheck
, implies
-- * Typeclass laws
, prop_lawfulEqAndTotalOrd
) where
Expand Down Expand Up @@ -221,6 +222,13 @@ shrinkNP g f np = npToSListI np $ cshrinkNP (Proxy @Top) g f np
collects :: Show a => [a] -> Property -> Property
collects = repeatedly collect

-- | QuickCheck's '==>' 'discard's the test if @p1@ fails; this is sometimes not
-- what we want, for example if we have other properties that do not depend on
-- @p1@ being true.
implies :: Testable prop => Bool -> prop -> Property
implies p1 p2 = not p1 .||. p2
infixr 0 `implies`

{-------------------------------------------------------------------------------
Typeclass laws
-------------------------------------------------------------------------------}
Expand All @@ -234,13 +242,13 @@ prop_lawfulEqAndTotalOrd a b c = conjoin
, counterexample "Not transitive: not (a <= b && b <= c => a <= c)" $
let antecedent = a <= b && b <= c in
classify antecedent "Antecedent for transitivity" $
antecedent =>> a `le` c
antecedent `implies` a `le` c
, counterexample "Not reflexive: not (a <= a)" $
a `le` a
, counterexample "Not antisymmetric: not (a <= b && b <= a => a == b)" $
let antecedent = a <= b && b <= a in
classify antecedent "Antecedent for antisymmetry" $
antecedent =>> a === b
antecedent `implies` a === b
, -- compatibility laws
counterexample "not ((a <= b) == (b >= a))" $
(a <= b) === (b >= a)
Expand All @@ -259,6 +267,3 @@ prop_lawfulEqAndTotalOrd a b c = conjoin
, counterexample "not (max a b == if a >= b then a else b)" $
max a b == if a >= b then a else b
]
where
infixr 0 =>>
p1 =>> p2 = not p1 .||. p2

0 comments on commit 5779c0f

Please sign in to comment.