{-# LANGUAGE ScopedTypeVariables #-}
module Hedgehog.Classes.Integral (integralLaws) where
import Hedgehog
import Hedgehog.Classes.Common
integralLaws :: (Integral a, Show a) => Gen a -> Laws
integralLaws :: Gen a -> Laws
integralLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Integral"
[ (String
"Quotient Remainder", Gen a -> Property
forall a. (Integral a, Show a) => Gen a -> Property
integralQuotientRemainder Gen a
gen)
, (String
"Division Modulus", Gen a -> Property
forall a. (Integral a, Show a) => Gen a -> Property
integralDivisionModulus Gen a
gen)
, (String
"Integer Roundtrip", Gen a -> Property
forall a. (Integral a, Show a) => Gen a -> Property
integralIntegerRoundtrip Gen a
gen)
]
integralQuotientRemainder :: forall a. (Integral a, Show a) => Gen a -> Property
integralQuotientRemainder :: Gen a -> Property
integralQuotientRemainder Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
y <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = (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)
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Quotient Remainder", lawContextTcName :: String
lawContextTcName = String
"Integral"
, lawContextLawBody :: String
lawContextLawBody = String
"quot x y * y + (rem x y)" String -> String -> String
`congruency` String
"x"
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
y;
in [String] -> String
lawWhere
[ String
"quot x y * y + (rem x y)" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showY
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
integralDivisionModulus :: forall a. (Integral a, Show a) => Gen a -> Property
integralDivisionModulus :: Gen a -> Property
integralDivisionModulus Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
y <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = (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)
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Division Modulus", lawContextTcName :: String
lawContextTcName = String
"Integral"
, lawContextLawBody :: String
lawContextLawBody = String
"(div x y) * y + (mod x y)" String -> String -> String
`congruency` String
"x"
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
y;
in [String] -> String
lawWhere
[ String
"(div x y) * y + (mod x y)" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showY
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
integralIntegerRoundtrip :: forall a. (Integral a, Show a) => Gen a -> Property
integralIntegerRoundtrip :: Gen a -> Property
integralIntegerRoundtrip Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = Integer -> a
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x)
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Integer Roundtrip", lawContextTcName :: String
lawContextTcName = String
"Integral"
, lawContextLawBody :: String
lawContextLawBody = String
"fromInteger . toInteger" String -> String -> String
`congruency` String
"id"
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x;
in [String] -> String
lawWhere
[ String
"fromInteger . toInteger $ x" String -> String -> String
`congruency` String
"id x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx