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