{-# language CPP #-}
{-# language ScopedTypeVariables #-}
{-# language RankNTypes #-}
#ifndef HAVE_SEMIRINGS
module Hedgehog.Classes.Semiring () where
#else
module Hedgehog.Classes.Semiring (semiringLaws, ringLaws, starLaws) where
import Hedgehog
import Hedgehog.Classes.Common
import Prelude hiding (Num(..))
import Data.Semiring
import Data.Star
semiringLaws :: (Semiring a, Eq a, Show a) => Gen a -> Laws
semiringLaws :: Gen a -> Laws
semiringLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Semiring"
[ (String
"Additive Left Identity", Gen a -> Property
forall a. SemiringProp a
semiringAdditiveLeftIdentity Gen a
gen)
, (String
"Additive Right Identity", Gen a -> Property
forall a. SemiringProp a
semiringAdditiveRightIdentity Gen a
gen)
, (String
"Additive Associativity", Gen a -> Property
forall a. SemiringProp a
semiringAdditiveAssociativity Gen a
gen)
, (String
"Additive Commutativity", Gen a -> Property
forall a. SemiringProp a
semiringAdditiveCommutativity Gen a
gen)
, (String
"Multiplicative Left Identity", Gen a -> Property
forall a. SemiringProp a
semiringMultiplicativeLeftIdentity Gen a
gen)
, (String
"Multiplicative Right Identity", Gen a -> Property
forall a. SemiringProp a
semiringMultiplicativeRightIdentity Gen a
gen)
, (String
"Multiplicative Associativity", Gen a -> Property
forall a. SemiringProp a
semiringMultiplicativeAssociativity Gen a
gen)
, (String
"Multiplication Left-Distributes Over Addition", Gen a -> Property
forall a. SemiringProp a
semiringLeftMultiplicationDistributes Gen a
gen)
, (String
"Multiplication Right-Distributes Over Addition", Gen a -> Property
forall a. SemiringProp a
semiringRightMultiplicationDistributes Gen a
gen)
, (String
"Multiplicative Left Annihilation", Gen a -> Property
forall a. SemiringProp a
semiringLeftAnnihilation Gen a
gen)
, (String
"Multiplicative Right Annihilation", Gen a -> Property
forall a. SemiringProp a
semiringRightAnnihilation Gen a
gen)
]
ringLaws :: (Ring a, Eq a, Show a) => Gen a -> Laws
ringLaws :: Gen a -> Laws
ringLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Ring"
[ (String
"Additive Inverse", Gen a -> Property
forall a. RingProp a
ringAdditiveInverse Gen a
gen)
]
starLaws :: (Star a, Eq a, Show a) => Gen a -> Laws
starLaws :: Gen a -> Laws
starLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Star"
[ (String
"Asteration", Gen a -> Property
forall a. StarProp a
starAsteration Gen a
gen)
, (String
"APlus", Gen a -> Property
forall a. StarProp a
starAplus Gen a
gen)
]
type SemiringProp a = (Semiring a, Eq a, Show a) => Gen a -> Property
type RingProp a = (Ring a, Eq a, Show a) => Gen a -> Property
type StarProp a = (Star a, Eq a, Show a) => Gen a -> Property
ringAdditiveInverse :: forall a. RingProp a
ringAdditiveInverse :: Gen a -> Property
ringAdditiveInverse 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
let lhs :: a
lhs = a -> a
forall a. Ring a => a -> a
negate a
a a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
a
let rhs :: a
rhs = a
forall a. Semiring a => a
zero :: a
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
"Additive Inverse", lawContextTcName :: String
lawContextTcName = String
"Ring"
, lawContextLawBody :: String
lawContextLawBody = String
"negate a + a" String -> String -> String
`congruency` String
"zero"
, lawContextTcProp :: String
lawContextTcProp =
let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"negate a + a" String -> String -> String
`congruency` String
"zero, where"
, String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
, String
"zero = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
, 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
semiringAdditiveLeftIdentity :: forall a. SemiringProp a
semiringAdditiveLeftIdentity :: Gen a -> Property
semiringAdditiveLeftIdentity 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 = a
forall a. Semiring a => a
zero a -> a -> a
forall a. Semiring a => a -> a -> a
+ 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
"Additive Left Identity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"zero + x" String -> String -> String
`congruency` String
"x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"zero + x" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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
semiringAdditiveRightIdentity :: forall a. SemiringProp a
semiringAdditiveRightIdentity :: Gen a -> Property
semiringAdditiveRightIdentity 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 = a
x a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
forall a. Semiring a => a
zero
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
"Additive Right Identity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x + zero" String -> String -> String
`congruency` String
"x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"x + zero" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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
semiringAdditiveAssociativity :: forall a. SemiringProp a
semiringAdditiveAssociativity :: Gen a -> Property
semiringAdditiveAssociativity 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
a
c <- 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 -> a -> a
forall a. Semiring a => a -> a -> a
+ (a
b a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
c)
let rhs :: a
rhs = (a
a a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
b) a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
c
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
"Additive Associativity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x + (y + z)" String -> String -> String
`congruency` String
"(x + y) + z"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
a; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
b; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
c;
in [String] -> String
lawWhere
[ String
"x + (y + z)" String -> String -> String
`congruency` String
"(x + y) + 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
]
}
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
semiringAdditiveCommutativity :: forall a. SemiringProp a
semiringAdditiveCommutativity :: Gen a -> Property
semiringAdditiveCommutativity 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 :: a
lhs = a
a a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
b
let rhs :: a
rhs = a
b a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
a
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
"Additive Commutativity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x + y" String -> String -> String
`congruency` String
"y + x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
a; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
b;
in [String] -> String
lawWhere
[ String
"x + y" String -> String -> String
`congruency` String
"y + 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
]
}
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
semiringMultiplicativeLeftIdentity :: forall a. SemiringProp a
semiringMultiplicativeLeftIdentity :: Gen a -> Property
semiringMultiplicativeLeftIdentity 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 = a
forall a. Semiring a => a
one a -> a -> a
forall a. Semiring a => a -> a -> a
* 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
"Multiplicative Left Identity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"one * x" String -> String -> String
`congruency` String
"x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showO :: String
showO = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
one :: a);
in [String] -> String
lawWhere
[ String
"one * x" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showO
]
}
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
semiringMultiplicativeRightIdentity :: forall a. SemiringProp a
semiringMultiplicativeRightIdentity :: Gen a -> Property
semiringMultiplicativeRightIdentity 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 = a
x a -> a -> a
forall a. Semiring a => a -> a -> a
* a
forall a. Semiring a => a
one
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
"Multiplicative Right Identity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x * one" String -> String -> String
`congruency` String
"x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showO :: String
showO = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
one :: a);
in [String] -> String
lawWhere
[ String
"x * one" String -> String -> String
`congruency` String
"x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showO
]
}
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
semiringMultiplicativeAssociativity :: forall a. SemiringProp a
semiringMultiplicativeAssociativity :: Gen a -> Property
semiringMultiplicativeAssociativity 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
a
c <- 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 -> a -> a
forall a. Semiring a => a -> a -> a
* (a
b a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c)
let rhs :: a
rhs = (a
a a -> a -> a
forall a. Semiring a => a -> a -> a
* a
b) a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c
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
"Multiplicative Associativity", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x * (y * z)" String -> String -> String
`congruency` String
"(x * y) * z"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
a; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
b; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
c;
in [String] -> String
lawWhere
[ String
"x * (y * z)" String -> String -> String
`congruency` String
"(x * y) * 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
]
}
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
semiringLeftMultiplicationDistributes :: forall a. SemiringProp a
semiringLeftMultiplicationDistributes :: Gen a -> Property
semiringLeftMultiplicationDistributes 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
a
c <- 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 -> a -> a
forall a. Semiring a => a -> a -> a
* (a
b a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
c)
let rhs :: a
rhs = (a
a a -> a -> a
forall a. Semiring a => a -> a -> a
* a
b) a -> a -> a
forall a. Semiring a => a -> a -> a
+ (a
a a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c)
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
"Multiplication Left-Distributes Over Addition", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x * (y + z)" String -> String -> String
`congruency` String
"(x * y) + (x * z)"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
a; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
b; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
c;
in [String] -> String
lawWhere
[ String
"x * (y + z)" String -> String -> String
`congruency` String
"(x * y) + (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
]
}
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
semiringRightMultiplicationDistributes :: forall a. SemiringProp a
semiringRightMultiplicationDistributes :: Gen a -> Property
semiringRightMultiplicationDistributes 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
a
c <- 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 -> a -> a
forall a. Semiring a => a -> a -> a
+ a
b) a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c
let rhs :: a
rhs = (a
a a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c) a -> a -> a
forall a. Semiring a => a -> a -> a
+ (a
b a -> a -> a
forall a. Semiring a => a -> a -> a
* a
c)
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
"Multiplication Right-Distributes Over Addition", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"(y + z) * x" String -> String -> String
`congruency` String
"(y * x) + (z * x)"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
a; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
b; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
c;
in [String] -> String
lawWhere
[ String
"(y + z) * x" String -> String -> String
`congruency` String
"(y * x) + (z * 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
, String
"z = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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
semiringLeftAnnihilation :: forall a. SemiringProp a
semiringLeftAnnihilation :: Gen a -> Property
semiringLeftAnnihilation 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 = a
forall a. Semiring a => a
zero a -> a -> a
forall a. Semiring a => a -> a -> a
* a
x
let rhs :: a
rhs = a
forall a. Semiring a => a
zero
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
"Multiplicative Left Annihilation", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"zero * x" String -> String -> String
`congruency` String
"zero"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"zero * x" String -> String -> String
`congruency` String
"zero, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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
semiringRightAnnihilation :: forall a. SemiringProp a
semiringRightAnnihilation :: Gen a -> Property
semiringRightAnnihilation 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 = a
x a -> a -> a
forall a. Semiring a => a -> a -> a
* a
forall a. Semiring a => a
zero
let rhs :: a
rhs = a
forall a. Semiring a => a
zero
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
"Multiplicative Right Annihilation", lawContextTcName :: String
lawContextTcName = String
"Semiring"
, lawContextLawBody :: String
lawContextLawBody = String
"x * zero" String -> String -> String
`congruency` String
"zero"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"x * zero" String -> String -> String
`congruency` String
"zero, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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
starAsteration :: forall a. StarProp a
starAsteration :: Gen a -> Property
starAsteration 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 = a -> a
forall a. Star a => a -> a
star a
x
let rhs :: a
rhs = a
forall a. Semiring a => a
one a -> a -> a
forall a. Semiring a => a -> a -> a
+ a
x a -> a -> a
forall a. Semiring a => a -> a -> a
* a -> a
forall a. Star a => a -> a
star 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
"Asteration", lawContextTcName :: String
lawContextTcName = String
"Star"
, lawContextLawBody :: String
lawContextLawBody = String
"star x" String -> String -> String
`congruency` String
"one + x * star x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showOne :: String
showOne = a -> String
forall a. Show a => a -> String
show (a
forall a. Semiring a => a
one :: a);
in [String] -> String
lawWhere
[ String
"star x" String -> String -> String
`congruency` String
"one + x * star x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showOne
]
}
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
starAplus :: forall a. StarProp a
starAplus :: Gen a -> Property
starAplus 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 = a -> a
forall a. Star a => a -> a
aplus a
x
let rhs :: a
rhs = a
x a -> a -> a
forall a. Semiring a => a -> a -> a
* a -> a
forall a. Star a => a -> a
star 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
"APlus", lawContextTcName :: String
lawContextTcName = String
"Star"
, lawContextLawBody :: String
lawContextLawBody = String
"aplus x" String -> String -> String
`congruency` String
"x * star x"
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x
in [String] -> String
lawWhere
[ String
"aplus x" String -> String -> String
`congruency` String
"x * star x, where"
, String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
]
}
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
#endif