{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Ord
  ( ordLaws
  ) where

import Data.Proxy (Proxy)
import Test.QuickCheck hiding ((.&.))
import Test.QuickCheck.Property (Property)

import Test.QuickCheck.Classes.Internal (Laws(..))

-- | Tests the following properties:
--
-- [/Antisymmetry/]
--   @a ≤ b ∧ b ≤ a ⇒ a = b@ 
-- [/Transitivity/]
--   @a ≤ b ∧ b ≤ c ⇒ a ≤ c@
-- [/Totality/]
--   @a ≤ b ∨ a > b@
ordLaws :: (Ord a, Arbitrary a, Show a) => Proxy a -> Laws
ordLaws :: Proxy a -> Laws
ordLaws Proxy a
p = String -> [(String, Property)] -> Laws
Laws String
"Ord"
  [ (String
"Antisymmetry", Proxy a -> Property
forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordAntisymmetric Proxy a
p)
  , (String
"Transitivity", Proxy a -> Property
forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordTransitive Proxy a
p)
  , (String
"Totality", Proxy a -> Property
forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordTotal Proxy a
p)
  ]

ordAntisymmetric :: forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordAntisymmetric :: Proxy a -> Property
ordAntisymmetric Proxy a
_ = (a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Bool) -> Property) -> (a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) 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)) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b)

ordTotal :: forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordTotal :: Proxy a -> Property
ordTotal Proxy a
_ = (a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Bool) -> Property) -> (a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) 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)) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True

-- Technically, this tests something a little stronger than it is supposed to.
-- But that should be alright since this additional strength is implied by
-- the rest of the Ord laws.
ordTransitive :: forall a. (Show a, Ord a, Arbitrary a) => Proxy a -> Property
ordTransitive :: Proxy a -> Property
ordTransitive Proxy a
_ = (a -> a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> a -> Bool) -> Property)
-> (a -> a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) a
b a
c -> case (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b, a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
b a
c) of
  (Ordering
LT,Ordering
LT) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c
  (Ordering
LT,Ordering
EQ) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c
  (Ordering
LT,Ordering
GT) -> Bool
True
  (Ordering
EQ,Ordering
LT) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c
  (Ordering
EQ,Ordering
EQ) -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c
  (Ordering
EQ,Ordering
GT) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
c
  (Ordering
GT,Ordering
LT) -> Bool
True
  (Ordering
GT,Ordering
EQ) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
c
  (Ordering
GT,Ordering
GT) -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
c