{-# 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
  , (=:=)
    -- * 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           Ouroboros.Consensus.Util (repeatedly)
import           Ouroboros.Consensus.Util.Condense (Condense, condense)
import           Test.QuickCheck

{-------------------------------------------------------------------------------
  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
-------------------------------------------------------------------------------}

-- | 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
    ]