    -- |
    -- Module:      Test.QuickCheck.Classes.Euclidean
    -- Copyright:   (c) 2019 Andrew Lelechenko
    -- Licence:     BSD3
    --

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall #-}

    #if !HAVE_SEMIRINGS
    module Test.QuickCheck.Classes.Euclidean where
    #else

    module Test.QuickCheck.Classes.Euclidean
      ( gcdDomainLaws
      , euclideanLaws
      ) where

    import Prelude hiding (quotRem, quot, rem, gcd, lcm)
    import Data.Maybe
    import Data.Proxy (Proxy)
    import Data.Euclidean
    import Data.Semiring (Semiring(..))

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

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

    -- | Test that a 'GcdDomain' instance obey several laws.
    --
    -- Check that 'divide' is an inverse of times:
    --
    -- * @y \/= 0 => (x * y) \`divide\` y == Just x@,
    -- * @y \/= 0, x \`divide\` y == Just z => x == z * y@.
    --
    -- Check that 'gcd' is a common divisor and is a multiple of any common divisor:
    --
    -- * @x \/= 0, y \/= 0 => isJust (x \`divide\` gcd x y) && isJust (y \`divide\` gcd x y)@,
    -- * @z \/= 0 => isJust (gcd (x * z) (y * z) \`divide\` z)@.
    --
    -- Check that 'lcm' is a common multiple and is a factor of any common multiple:
    --
    -- * @x \/= 0, y \/= 0 => isJust (lcm x y \`divide\` x) && isJust (lcm x y \`divide\` y)@,
    -- * @x \/= 0, y \/= 0, isJust (z \`divide\` x), isJust (z \`divide\` y) => isJust (z \`divide\` lcm x y)@.
    --
    -- Check that 'gcd' of 'coprime' numbers is a unit of the semiring (has an inverse):
    --
    -- * @y \/= 0, coprime x y => isJust (1 \`divide\` gcd x y)@.
    gcdDomainLaws :: (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Laws
    gcdDomainLaws :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Laws
    gcdDomainLaws Proxy a
    p = String -> [(String, Property)] -> Laws
    Laws String
    "GcdDomain"
      [ (String
    "divide1", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    divideLaw1 Proxy a
    p)
      , (String
    "divide2", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    divideLaw2 Proxy a
    p)
      , (String
    "gcd1", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    gcdLaw1 Proxy a
    p)
      , (String
    "gcd2", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    gcdLaw2 Proxy a
    p)
      , (String
    "lcm1", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    lcmLaw1 Proxy a
    p)
      , (String
    "lcm2", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    lcmLaw2 Proxy a
    p)
      , (String
    "coprime", Proxy a -> Property
    forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    coprimeLaw Proxy a
    p)
      ]

    divideLaw1 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    divideLaw1 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    divideLaw1 Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> (a
    x a -> a -> a
    forall a. Semiring a => a -> a -> a
    `times` a
    y) a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    y Maybe a -> Maybe a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x

    divideLaw2 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    divideLaw2 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    divideLaw2 Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> Property -> (a -> Property) -> Maybe a -> Property
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Bool -> Property
    forall prop. Testable prop => prop -> Property
    property Bool
    True) (\a
    z -> a
    x a -> a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === a
    z a -> a -> a
    forall a. Semiring a => a -> a -> a
    `times` a
    y) (a
    x a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    y)

    gcdLaw1 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    gcdLaw1 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    gcdLaw1 Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Bool -> Bool
    || a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a
    x a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    gcd a
    x a
    y) Bool -> Bool -> Property
    forall prop1 prop2.
    (Testable prop1, Testable prop2) =>
    prop1 -> prop2 -> Property
    .&&. Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a
    y a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    gcd a
    x a
    y)

    gcdLaw2 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    gcdLaw2 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    gcdLaw2 Proxy a
    _ = (a -> a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> a -> Property) -> Property)
    -> (a -> a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y a
    z ->
      a
    z a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Bool -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    gcd (a
    x a -> a -> a
    forall a. Semiring a => a -> a -> a
    `times` a
    z) (a
    y a -> a -> a
    forall a. Semiring a => a -> a -> a
    `times` a
    z) a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    z)

    lcmLaw1 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    lcmLaw1 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    lcmLaw1 Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Bool -> Bool
    && a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    lcm a
    x a
    y a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    x) Bool -> Bool -> Property
    forall prop1 prop2.
    (Testable prop1, Testable prop2) =>
    prop1 -> prop2 -> Property
    .&&. Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    lcm a
    x a
    y a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    y)

    lcmLaw2 :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    lcmLaw2 :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    lcmLaw2 Proxy a
    _ = (a -> a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> a -> Property) -> Property)
    -> (a -> a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y a
    z ->
      a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Bool -> Bool
    && a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> Maybe a -> Bool
    forall a. Maybe a -> Bool
    isNothing (a
    z a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    x) Bool -> Property -> Property
    forall prop1 prop2.
    (Testable prop1, Testable prop2) =>
    prop1 -> prop2 -> Property
    .||. Maybe a -> Bool
    forall a. Maybe a -> Bool
    isNothing (a
    z a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a
    y) Bool -> Bool -> Property
    forall prop1 prop2.
    (Testable prop1, Testable prop2) =>
    prop1 -> prop2 -> Property
    .||. Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a
    z a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    lcm a
    x a
    y)

    coprimeLaw :: forall a. (Eq a, GcdDomain a, Arbitrary a, Show a) => Proxy a -> Property
    coprimeLaw :: forall a.
    (Eq a, GcdDomain a, Arbitrary a, Show a) =>
    Proxy a -> Property
    coprimeLaw Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> a -> a -> Bool
    forall a. GcdDomain a => a -> a -> Bool
    coprime a
    x a
    y Bool -> Bool -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (a
    forall a. Semiring a => a
    one a -> a -> Maybe a
    forall a. GcdDomain a => a -> a -> Maybe a
    `divide` a -> a -> a
    forall a. GcdDomain a => a -> a -> a
    gcd a
    x a
    y)

    -- | Test that a 'Euclidean' instance obey laws of a Euclidean domain.
    --
    -- * @y \/= 0, r == x \`rem\` y => r == 0 || degree r < degree y@,
    -- * @y \/= 0, (q, r) == x \`quotRem\` y => x == q * y + r@,
    -- * @y \/= 0 => x \`quot\` x y == fst (x \`quotRem\` y)@,
    -- * @y \/= 0 => x \`rem\` x y == snd (x \`quotRem\` y)@.
    euclideanLaws :: (Eq a, Euclidean a, Arbitrary a, Show a) => Proxy a -> Laws
    euclideanLaws :: forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Laws
    euclideanLaws Proxy a
    p = String -> [(String, Property)] -> Laws
    Laws String
    "Euclidean"
      [ (String
    "degree", Proxy a -> Property
    forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    degreeLaw Proxy a
    p)
      , (String
    "quotRem", Proxy a -> Property
    forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    quotRemLaw Proxy a
    p)
      , (String
    "quot", Proxy a -> Property
    forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    quotLaw Proxy a
    p)
      , (String
    "rem", Proxy a -> Property
    forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    remLaw Proxy a
    p)
      ]

    degreeLaw :: forall a. (Eq a, Euclidean a, Arbitrary a, Show a) => Proxy a -> Property
    degreeLaw :: forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    degreeLaw Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> let (a
    _, a
    r) = a
    x a -> a -> (a, a)
    forall a. Euclidean a => a -> a -> (a, a)
    `quotRem` a
    y in (a
    r a -> a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === a
    forall a. Semiring a => a
    zero Property -> Bool -> Property
    forall prop1 prop2.
    (Testable prop1, Testable prop2) =>
    prop1 -> prop2 -> Property
    .||. a -> Natural
    forall a. Euclidean a => a -> Natural
    degree a
    r Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < a -> Natural
    forall a. Euclidean a => a -> Natural
    degree a
    y)

    quotRemLaw :: forall a. (Eq a, Euclidean a, Arbitrary a, Show a) => Proxy a -> Property
    quotRemLaw :: forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    quotRemLaw Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> let (a
    q, a
    r) = a
    x a -> a -> (a, a)
    forall a. Euclidean a => a -> a -> (a, a)
    `quotRem` a
    y in a
    x a -> a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === (a
    q a -> a -> a
    forall a. Semiring a => a -> a -> a
    `times` a
    y) a -> a -> a
    forall a. Semiring a => a -> a -> a
    `plus` a
    r

    quotLaw :: forall a. (Eq a, Euclidean a, Arbitrary a, Show a) => Proxy a -> Property
    quotLaw :: forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    quotLaw Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> a -> a -> a
    forall a. Euclidean a => a -> a -> a
    quot a
    x a
    y a -> a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === (a, a) -> a
    forall a b. (a, b) -> a
    fst (a -> a -> (a, a)
    forall a. Euclidean a => a -> a -> (a, a)
    quotRem a
    x a
    y)

    remLaw :: forall a. (Eq a, Euclidean a, Arbitrary a, Show a) => Proxy a -> Property
    remLaw :: forall a.
    (Eq a, Euclidean a, Arbitrary a, Show a) =>
    Proxy a -> Property
    remLaw Proxy a
    _ = (a -> a -> Property) -> Property
    forall prop. Testable prop => prop -> Property
    property ((a -> a -> Property) -> Property)
    -> (a -> a -> Property) -> Property
    forall a b. (a -> b) -> a -> b
    $ \(a
    x :: a) a
    y ->
      a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    forall a. Semiring a => a
    zero Bool -> Property -> Property
    forall prop. Testable prop => Bool -> prop -> Property
    ==> a -> a -> a
    forall a. Euclidean a => a -> a -> a
    rem a
    x a
    y a -> a -> Property
    forall a. (Eq a, Show a) => a -> a -> Property
    === (a, a) -> a
    forall a b. (a, b) -> b
    snd (a -> a -> (a, a)
    forall a. Euclidean a => a -> a -> (a, a)
    quotRem a
    x a
    y)

    #endif