    {-# 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 :: forall a. (Ord a, Arbitrary a, Show a) => 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 :: forall a. (Show a, Ord a, Arbitrary a) => 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 :: forall a. (Show a, Ord a, Arbitrary a) => 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 :: forall a. (Show a, Ord a, Arbitrary a) => 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