{-# 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(..))
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)
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