{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | QuickCheck utilities
module Test.Util.QuickCheck (
    -- * Generic QuickCheck utilities
    checkGenerator
  , checkInvariant
  , checkShrinker
    -- * Comparison functions
  , expectRight
  , ge
  , gt
  , le
  , lt
  , strictlyIncreasing
    -- * Comparing maps
  , isSubmapOfBy
    -- * Improved variants
  , elements
  , (=:=)
    -- * SOP
  , cshrinkNP
  , shrinkNP
    -- * Convenience
  , collects
  , forAllGenRunShrinkCheck
  , implies
    -- * Typeclass laws
  , prop_lawfulEqAndTotalOrd
  ) where

import           Control.Monad.Except
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Proxy
import           Data.SOP.Constraint
import           Data.SOP.Strict
import           GHC.Stack (HasCallStack)
import           Ouroboros.Consensus.Util (repeatedly)
import           Ouroboros.Consensus.Util.Condense (Condense, condense)
import qualified Test.QuickCheck as QC
import           Test.QuickCheck hiding (elements)

{-------------------------------------------------------------------------------
  Generic QuickCheck utilities
-------------------------------------------------------------------------------}

-- | Test the generator
--
-- Uses explicit 'forAll' as we don't want to assume a correct shrinker.
checkGenerator :: (Arbitrary a, Show a) => (a -> Property) -> Property
checkGenerator :: forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkGenerator a -> Property
p = Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen a
forall a. Arbitrary a => Gen a
arbitrary ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ a -> Property
p

-- | Test the shrinker
checkShrinker :: forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkShrinker :: forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkShrinker a -> Property
p =
    -- Starting point, some arbitrary value
    -- Explicit 'forAll': don't shrink when testing the shrinker
    Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen a
forall a. Arbitrary a => Gen a
arbitrary a -> Property
go
  where
    go :: a -> Property
    go :: a -> Property
go a
a =
        if [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (a -> [a]
forall a. Arbitrary a => a -> [a]
shrink a
a) then
          Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        else
          -- Nested 'forAll': testing that /all/ shrunk values satisfy the
          -- property is too expensive. Since we're not shrinking, nesting
          -- 'forAll' is ok.
          Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([a] -> Gen a
forall a. HasCallStack => [a] -> Gen a
elements (a -> [a]
forall a. Arbitrary a => a -> [a]
shrink a
a)) ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \a
a' -> a -> Property
p a
a' Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. a -> Property
go a
a'

-- | Check invariant
checkInvariant :: (a -> Except String ()) -> (a -> Property)
checkInvariant :: forall a. (a -> Except String ()) -> a -> Property
checkInvariant a -> Except String ()
f = () -> Either String () -> Property
forall a b. (Show a, Show b, Eq b) => b -> Either a b -> Property
expectRight () (Either String () -> Property)
-> (a -> Either String ()) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except String () -> Either String ()
forall e a. Except e a -> Either e a
runExcept (Except String () -> Either String ())
-> (a -> Except String ()) -> a -> Either String ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Except String ()
f

-- | Explicit quantification using the “gen-run-shrink-check” pattern.
--
-- Instead of the usual two stages where one generates an input and then checks
-- the property for that input, we rely on three stages: one generates an input,
-- then transforms it into an output, and then checks the output.
--
-- When adding a shrinker to the mix, we can allow it to inspect the output
-- value as well, which increases its expressivity. This makes sense if the
-- “run” phase is particularly expensive.
forAllGenRunShrinkCheck ::
  Testable prop =>
  Gen input ->
  (input -> output) ->
  (input -> output -> [input]) ->
  (input -> output -> prop) ->
  Property
forAllGenRunShrinkCheck :: forall prop input output.
Testable prop =>
Gen input
-> (input -> output)
-> (input -> output -> [input])
-> (input -> output -> prop)
-> Property
forAllGenRunShrinkCheck Gen input
gen input -> output
run input -> output -> [input]
shrink_ input -> output -> prop
check =
  Gen input -> (input -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen input
gen ((input -> Property) -> Property)
-> (input -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \input
input ->
    ((input, output) -> [(input, output)])
-> (input, output) -> ((input, output) -> prop) -> Property
forall prop a.
Testable prop =>
(a -> [a]) -> a -> (a -> prop) -> Property
shrinking
      ((input -> (input, output)) -> [input] -> [(input, output)]
forall a b. (a -> b) -> [a] -> [b]
map input -> (input, output)
run' ([input] -> [(input, output)])
-> ((input, output) -> [input])
-> (input, output)
-> [(input, output)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (input -> output -> [input]) -> (input, output) -> [input]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry input -> output -> [input]
shrink_)
      (input -> (input, output)
run' input
input)
      ((input -> output -> prop) -> (input, output) -> prop
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry input -> output -> prop
check)
  where
    run' :: input -> (input, output)
run' input
inp = (input
inp, input -> output
run input
inp)

{-------------------------------------------------------------------------------
  Comparison functions
-------------------------------------------------------------------------------}

infix 4 `lt`
infix 4 `le`
infix 4 `gt`
infix 4 `ge`

-- | Like '<', but prints a counterexample when it fails.
lt :: (Ord a, Show a) => a -> a -> Property
a
x lt :: forall a. (Ord a, Show a) => a -> a -> Property
`lt` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y

-- | Like '<=', but prints a counterexample when it fails.
le :: (Ord a, Show a) => a -> a -> Property
a
x le :: forall a. (Ord a, Show a) => a -> a -> Property
`le` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y

-- | Like '>', but prints a counterexample when it fails.
gt :: (Ord a, Show a) => a -> a -> Property
a
x gt :: forall a. (Ord a, Show a) => a -> a -> Property
`gt` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y

-- | Like '>=', but prints a counterexample when it fails.
ge :: (Ord a, Show a) => a -> a -> Property
a
x ge :: forall a. (Ord a, Show a) => a -> a -> Property
`ge` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" < " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y

strictlyIncreasing :: forall a. (Show a, Ord a) => [a] -> Property
strictlyIncreasing :: forall a. (Show a, Ord a) => [a] -> Property
strictlyIncreasing [a]
xs =
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([a] -> String
forall a. Show a => a -> String
show [a]
xs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ [a] -> Property
go [a]
xs
  where
    go :: [a] -> Property
    go :: [a] -> Property
go []       = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    go [a
_]      = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    go (a
x:a
y:[a]
zs) = a
x a -> a -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`lt` a
y Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. [a] -> Property
go (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)

-- | Check that we have the expected 'Right' value
--
-- @expectRight b ab@ is roughly equivalent to @Right b === ab@, but avoids an
-- equality constraint on @a@.
expectRight :: (Show a, Show b, Eq b) => b -> Either a b -> Property
expectRight :: forall a b. (Show a, Show b, Eq b) => b -> Either a b -> Property
expectRight b
b (Right b
b') = b
b b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b
b'
expectRight b
_ (Left a
a)   = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Unexpected left " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
                             Bool
False

{-------------------------------------------------------------------------------
  Comparing maps
-------------------------------------------------------------------------------}

isSubmapOfBy :: (Ord k, Show k, Show a, Show b)
             => (a -> b -> Property) -> Map k a -> Map k b -> Property
isSubmapOfBy :: forall k a b.
(Ord k, Show k, Show a, Show b) =>
(a -> b -> Property) -> Map k a -> Map k b -> Property
isSubmapOfBy a -> b -> Property
p Map k a
l Map k b
r = [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin [
      case k -> Map k b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k b
r of
        Maybe b
Nothing -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"key " String -> String -> String
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with value " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not present in other map") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                     Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
        Just b
b  -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"key " String -> String -> String
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with values " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
b
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" doesn't satisfy the property") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                     a -> b -> Property
p a
a b
b
    | (k
k, a
a) <- Map k a -> [(k, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k a
l
    ]

{-------------------------------------------------------------------------------
  Improved variants
-------------------------------------------------------------------------------}

-- | Generates one of the given values. The input list must be non-empty.
--
-- NOTE unlike the standard @elements@, this variant has a 'HasCallStack'
-- constraint, which makes debugging the 'error' much easier.
elements :: HasCallStack => [a] -> Gen a
elements :: forall a. HasCallStack => [a] -> Gen a
elements [] = String -> Gen a
forall a. HasCallStack => String -> a
error String
"Test.Util.QuickCheck.elements used with empty list"
elements [a]
xs = [a] -> Gen a
forall a. [a] -> Gen a
QC.elements [a]
xs

-- | Like '===', but uses 'Condense' instead of 'Show' when it fails.
infix 4 =:=
(=:=) :: (Eq a, Condense a) => a -> a -> Property
a
x =:= :: forall a. (Eq a, Condense a) => a -> a -> Property
=:= a
y =
    String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Condense a => a -> String
condense a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
interpret Bool
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Condense a => a -> String
condense a
y) Bool
res
  where
    res :: Bool
res = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
    interpret :: Bool -> String
interpret Bool
True  = String
" == "
    interpret Bool
False = String
" /= "

{-------------------------------------------------------------------------------
  SOP
-------------------------------------------------------------------------------}

cshrinkNP :: forall proxy c f g xs.
             All c xs
          => proxy c
          -> (forall a. c a => f a -> g a)    -- For elements we don't shrink
          -> (forall a. c a => f a -> [g a])
          -> NP f xs
          -> [NP g xs]
cshrinkNP :: forall (proxy :: (* -> Constraint) -> *) (c :: * -> Constraint)
       (f :: * -> *) (g :: * -> *) (xs :: [*]).
All c xs =>
proxy c
-> (forall a. c a => f a -> g a)
-> (forall a. c a => f a -> [g a])
-> NP f xs
-> [NP g xs]
cshrinkNP proxy c
p forall a. c a => f a -> g a
g forall a. c a => f a -> [g a]
f = NP f xs -> [NP g xs]
forall (xs' :: [*]). All c xs' => NP f xs' -> [NP g xs']
go
  where
    go :: All c xs' => NP f xs' -> [NP g xs']
    go :: forall (xs' :: [*]). All c xs' => NP f xs' -> [NP g xs']
go NP f xs'
Nil       = [] -- Can't shrink the empty list
    go (f x
x :* NP f xs1
xs) = [[NP g xs']] -> [NP g xs']
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          -- Shrink the head of the list
          [ g x
x' g x -> NP g xs1 -> NP g (x : xs1)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* proxy c -> (forall a. c a => f a -> g a) -> NP f xs1 -> NP g xs1
forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap proxy c
p f a -> g a
forall a. c a => f a -> g a
g NP f xs1
xs | g x
x' <- f x -> [g x]
forall a. c a => f a -> [g a]
f f x
x ]

          -- Or shrink the tail of the list
        , [ f x -> g x
forall a. c a => f a -> g a
g f x
x g x -> NP g xs1 -> NP g (x : xs1)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP g xs1
xs' | NP g xs1
xs' <- NP f xs1 -> [NP g xs1]
forall (xs' :: [*]). All c xs' => NP f xs' -> [NP g xs']
go NP f xs1
xs ]
        ]

shrinkNP :: (forall a. f a -> g a)    -- For elements we don't shrink
         -> (forall a. f a -> [g a])
         -> NP f xs
         -> [NP g xs]
shrinkNP :: forall (f :: * -> *) (g :: * -> *) (xs :: [*]).
(forall a. f a -> g a)
-> (forall a. f a -> [g a]) -> NP f xs -> [NP g xs]
shrinkNP forall a. f a -> g a
g forall a. f a -> [g a]
f NP f xs
np = NP f xs -> (SListI xs => [NP g xs]) -> [NP g xs]
forall {k} (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP f xs
np ((SListI xs => [NP g xs]) -> [NP g xs])
-> (SListI xs => [NP g xs]) -> [NP g xs]
forall a b. (a -> b) -> a -> b
$ Proxy Top
-> (forall a. Top a => f a -> g a)
-> (forall a. Top a => f a -> [g a])
-> NP f xs
-> [NP g xs]
forall (proxy :: (* -> Constraint) -> *) (c :: * -> Constraint)
       (f :: * -> *) (g :: * -> *) (xs :: [*]).
All c xs =>
proxy c
-> (forall a. c a => f a -> g a)
-> (forall a. c a => f a -> [g a])
-> NP f xs
-> [NP g xs]
cshrinkNP (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Top) f a -> g a
forall a. f a -> g a
forall a. Top a => f a -> g a
g f a -> [g a]
forall a. f a -> [g a]
forall a. Top a => f a -> [g a]
f NP f xs
np

{-------------------------------------------------------------------------------
  Convenience
-------------------------------------------------------------------------------}

collects :: Show a => [a] -> Property -> Property
collects :: forall a. Show a => [a] -> Property -> Property
collects = (a -> Property -> Property) -> [a] -> Property -> Property
forall a b. (a -> b -> b) -> [a] -> b -> b
repeatedly a -> Property -> Property
forall a prop. (Show a, Testable prop) => a -> prop -> Property
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 :: forall prop. Testable prop => Bool -> prop -> Property
implies Bool
p1 prop
p2 = Bool -> Bool
not Bool
p1 Bool -> prop -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. prop
p2
infixr 0 `implies`

{-------------------------------------------------------------------------------
  Typeclass laws
-------------------------------------------------------------------------------}

prop_lawfulEqAndTotalOrd ::
     forall a. (Show a, Ord a)
  => a -> a -> a -> Property
prop_lawfulEqAndTotalOrd :: forall a. (Show a, Ord a) => a -> a -> a -> Property
prop_lawfulEqAndTotalOrd a
a a
b a
c = [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
    [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Not total: a <= b || b <= a VIOLATED" (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
        a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b Bool -> Bool -> Bool
|| a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Not transitive: a <= b && b <= c => a <= c VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        let antecedent :: Bool
antecedent = a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
c in
        Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
antecedent String
"Antecedent for transitivity" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool
antecedent Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
`implies` a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
c
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Not reflexive: a <= a VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        a
a a -> a -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`le` a
a
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Not antisymmetric: a <= b && b <= a => a == b VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        let antecedent :: Bool
antecedent = a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a in
        Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
antecedent String
"Antecedent for antisymmetry" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool
antecedent Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
`implies` a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
    , -- compatibility laws
      String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a <= b) == (b >= a) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
a)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a < b) == (a <= b && a /= b) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b Bool -> Bool -> Bool
&& a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
b)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a > b) = (b < a) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
a)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a < b) == (compare a b == LT) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a > b) == (compare a b == GT) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(a == b) == (compare a b == EQ) VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"min a b == if a <= b then a else b VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        a -> a -> a
forall a. Ord a => a -> a -> a
min a
a a
b a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== if a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b then a
a else a
b
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"max a b == if a >= b then a else b VIOLATED" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        a -> a -> a
forall a. Ord a => a -> a -> a
max a
a a
b a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== if a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
b then a
a else a
b
    ]