{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Integral
  ( integralLaws
  ) where

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

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

-- | Tests the following properties:
--
-- [/Quotient Remainder/]
--   @(quot x y) * y + (rem x y) ≡ x@
-- [/Division Modulus/]
--   @(div x y) * y + (mod x y) ≡ x@
-- [/Integer Roundtrip/]
--   @fromInteger (toInteger x) ≡ x@
-- [/QuotRem is (Quot, Rem)/]
--   @quotRem x y ≡ (quot x y, rem x y)@
-- [/DivMod is (Div, Mod)/]
--   @divMod x y ≡ (div x y, mod x y)@
integralLaws :: (Integral a, Arbitrary a, Show a) => Proxy a -> Laws
integralLaws :: Proxy a -> Laws
integralLaws p :: Proxy a
p = String -> [(String, Property)] -> Laws
Laws "Integral"
  [ ("Quotient Remainder", Proxy a -> Property
forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralQuotientRemainder Proxy a
p)
  , ("Division Modulus", Proxy a -> Property
forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralDivisionModulus Proxy a
p)
  , ("Integer Roundtrip", Proxy a -> Property
forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralIntegerRoundtrip Proxy a
p)
  , ("QuotRem is (Quot, Rem)", Proxy a -> Property
forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralQuotRem Proxy a
p)
  , ("DivMod is (Div, Mod)", Proxy a -> Property
forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralDivMod Proxy a
p)
  ]

integralQuotientRemainder :: forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralQuotientRemainder :: Proxy a -> Property
integralQuotientRemainder _ = Bool
-> ((a, a) -> Bool)
-> ((a, a) -> [String])
-> String
-> ((a, a) -> a)
-> String
-> ((a, a) -> a)
-> Property
forall a b.
(Arbitrary a, Show b, Eq b) =>
Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> b)
-> String
-> (a -> b)
-> Property
myForAllShrink Bool
False (\(_,y :: a
y) -> a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= 0)
  (\(a
x :: a, y :: a
y) -> ["x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x, "y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y])
  "(quot x y) * y + (rem x y)"
  (\(x :: a
x,y :: a
y) -> (a -> a -> a
forall a. Integral a => a -> a -> a
quot a
x a
y) a -> a -> a
forall a. Num a => a -> a -> a
* a
y a -> a -> a
forall a. Num a => a -> a -> a
+ (a -> a -> a
forall a. Integral a => a -> a -> a
rem a
x a
y))
  "x"
  (\(x :: a
x,_) -> a
x)

integralDivisionModulus :: forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralDivisionModulus :: Proxy a -> Property
integralDivisionModulus _ = Bool
-> ((a, a) -> Bool)
-> ((a, a) -> [String])
-> String
-> ((a, a) -> a)
-> String
-> ((a, a) -> a)
-> Property
forall a b.
(Arbitrary a, Show b, Eq b) =>
Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> b)
-> String
-> (a -> b)
-> Property
myForAllShrink Bool
False (\(_,y :: a
y) -> a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= 0)
  (\(a
x :: a, y :: a
y) -> ["x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x, "y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y])
  "(div x y) * y + (mod x y)"
  (\(x :: a
x,y :: a
y) -> (a -> a -> a
forall a. Integral a => a -> a -> a
div a
x a
y) a -> a -> a
forall a. Num a => a -> a -> a
* a
y a -> a -> a
forall a. Num a => a -> a -> a
+ (a -> a -> a
forall a. Integral a => a -> a -> a
mod a
x a
y))
  "x"
  (\(x :: a
x,_) -> a
x)

integralIntegerRoundtrip :: forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralIntegerRoundtrip :: Proxy a -> Property
integralIntegerRoundtrip _ = Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> a)
-> String
-> (a -> a)
-> Property
forall a b.
(Arbitrary a, Show b, Eq b) =>
Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> b)
-> String
-> (a -> b)
-> Property
myForAllShrink Bool
False (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True)
  (\(a
x :: a) -> ["x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x])
  "fromInteger (toInteger x)"
  (\x :: a
x -> Integer -> a
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x))
  "x"
  (\x :: a
x -> a
x)

integralQuotRem :: forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralQuotRem :: Proxy a -> Property
integralQuotRem _ = Bool
-> ((a, a) -> Bool)
-> ((a, a) -> [String])
-> String
-> ((a, a) -> (a, a))
-> String
-> ((a, a) -> (a, a))
-> Property
forall a b.
(Arbitrary a, Show b, Eq b) =>
Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> b)
-> String
-> (a -> b)
-> Property
myForAllShrink Bool
False (\(_,y :: a
y) -> a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= 0)
  (\(a
x :: a, y :: a
y) -> ["x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x, "y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y])
  "quotRem x y"
  (\(x :: a
x,y :: a
y) -> a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
quotRem a
x a
y)
  "(quot x y, rem x y)"
  (\(x :: a
x,y :: a
y) -> (a -> a -> a
forall a. Integral a => a -> a -> a
quot a
x a
y, a -> a -> a
forall a. Integral a => a -> a -> a
rem a
x a
y))

integralDivMod :: forall a. (Integral a, Arbitrary a, Show a) => Proxy a -> Property
integralDivMod :: Proxy a -> Property
integralDivMod _ = Bool
-> ((a, a) -> Bool)
-> ((a, a) -> [String])
-> String
-> ((a, a) -> (a, a))
-> String
-> ((a, a) -> (a, a))
-> Property
forall a b.
(Arbitrary a, Show b, Eq b) =>
Bool
-> (a -> Bool)
-> (a -> [String])
-> String
-> (a -> b)
-> String
-> (a -> b)
-> Property
myForAllShrink Bool
False (\(_,y :: a
y) -> a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= 0)
  (\(a
x :: a, y :: a
y) -> ["x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x, "y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y])
  "divMod x y"
  (\(x :: a
x,y :: a
y) -> a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
x a
y)
  "(div x y, mod x y)"
  (\(x :: a
x,y :: a
y) -> (a -> a -> a
forall a. Integral a => a -> a -> a
div a
x a
y, a -> a -> a
forall a. Integral a => a -> a -> a
mod a
x a
y))