{-# LANGUAGE ScopedTypeVariables #-}
module Hedgehog.Classes.Ord (ordLaws) where
import Hedgehog
import Hedgehog.Classes.Common
ordLaws :: forall a. (Ord a, Show a) => Gen a -> Laws
ordLaws :: Gen a -> Laws
ordLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Ord"
[ (String
"Antisymmetry", Gen a -> Property
forall a. (Ord a, Show a) => Gen a -> Property
ordAntisymmetric Gen a
gen)
, (String
"Transitivity", Gen a -> Property
forall a. (Ord a, Show a) => Gen a -> Property
ordTransitive Gen a
gen)
, (String
"Reflexivity", Gen a -> Property
forall a. (Ord a, Show a) => Gen a -> Property
ordReflexive Gen a
gen)
, (String
"Totality", Gen a -> Property
forall a. (Ord a, Show a) => Gen a -> Property
ordTotal Gen a
gen)
]
ordAntisymmetric :: forall a. (Ord a, Show a) => Gen a -> Property
ordAntisymmetric :: Gen a -> Property
ordAntisymmetric 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
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: Bool
lhs = (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b) Bool -> Bool -> Bool
&& (a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a)
let rhs :: Bool
rhs = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
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
"Antisymmetry", lawContextTcName :: String
lawContextTcName = String
"Ord"
, lawContextLawBody :: String
lawContextLawBody = String
"x <= y && y <= x" String -> String -> String
`congruency` String
"x == y"
, lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
in [String] -> String
lawWhere
[ String
"x <= y && y <= x" String -> String -> String
`congruency` String
"x == y, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
, String
"y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showB
]
}
Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx
ordTransitive :: forall a. (Ord a, Show a) => Gen a -> Property
ordTransitive :: Gen a -> Property
ordTransitive 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
a
z <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: Bool
lhs = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y Bool -> Bool -> Bool
&& a
y a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
z
let rhs :: Bool
rhs = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
z
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
"Transitivity", lawContextTcName :: String
lawContextTcName = String
"Ord"
, lawContextLawBody :: String
lawContextLawBody = String
"x <= y && y <= z" String -> String -> String
`implies` String
"x <= z"
, lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
, 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; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z;
in [String] -> String
lawWhere
[ String
"x <= y && y <= z" String -> String -> String
`implies` String
"x <= z, 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
, String
"z = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
case (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y, a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
y a
z) of
(Ordering
LT,Ordering
LT) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hLessThanCtx a
x a
z Context
ctx
(Ordering
LT,Ordering
EQ) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hLessThanCtx a
x a
z Context
ctx
(Ordering
LT,Ordering
GT) -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success
(Ordering
EQ,Ordering
LT) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hLessThanCtx a
x a
z Context
ctx
(Ordering
EQ,Ordering
EQ) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
x a
z Context
ctx
(Ordering
EQ,Ordering
GT) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hGreaterThanCtx a
x a
z Context
ctx
(Ordering
GT,Ordering
LT) -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success
(Ordering
GT,Ordering
EQ) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hGreaterThanCtx a
x a
z Context
ctx
(Ordering
GT,Ordering
GT) -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Ord a, Show a, HasCallStack) =>
a -> a -> Context -> m ()
hGreaterThanCtx a
x a
z Context
ctx
ordTotal :: forall a. (Ord a, Show a) => Gen a -> Property
ordTotal :: Gen a -> Property
ordTotal 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
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: Bool
lhs = (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b) Bool -> Bool -> Bool
|| (a
b a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a)
let rhs :: Bool
rhs = Bool
True
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
"Totality", lawContextTcName :: String
lawContextTcName = String
"Ord"
, lawContextLawBody :: String
lawContextLawBody = String
"x <= y || y <= x" String -> String -> String
`congruency` String
"True"
, lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
in [String] -> String
lawWhere
[ String
"(x <= y) || (y <= x)" String -> String -> String
`congruency` String
"True, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
, String
"y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showB
]
}
Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx
ordReflexive :: forall a. (Ord a, Show a) => Gen a -> Property
ordReflexive :: Gen a -> Property
ordReflexive 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 :: Bool
lhs = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x
let rhs :: Bool
rhs = Bool
True
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
"Reflexivity", lawContextTcName :: String
lawContextTcName = String
"Ord"
, lawContextLawBody :: String
lawContextLawBody = String
"x <= x" String -> String -> String
`congruency` String
"True"
, lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x;
in [String] -> String
lawWhere
[ String
"x <= x" String -> String -> String
`congruency` String
"True, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
]
}
Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx