{-# 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 :: forall a. (Semiring a, Eq a, Show a) => Gen a -> Laws
semiringLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Semiring"
[ (String
"Additive Left Identity", forall a. SemiringProp a
semiringAdditiveLeftIdentity Gen a
gen)
, (String
"Additive Right Identity", forall a. SemiringProp a
semiringAdditiveRightIdentity Gen a
gen)
, (String
"Additive Associativity", forall a. SemiringProp a
semiringAdditiveAssociativity Gen a
gen)
, (String
"Additive Commutativity", forall a. SemiringProp a
semiringAdditiveCommutativity Gen a
gen)
, (String
"Multiplicative Left Identity", forall a. SemiringProp a
semiringMultiplicativeLeftIdentity Gen a
gen)
, (String
"Multiplicative Right Identity", forall a. SemiringProp a
semiringMultiplicativeRightIdentity Gen a
gen)
, (String
"Multiplicative Associativity", forall a. SemiringProp a
semiringMultiplicativeAssociativity Gen a
gen)
, (String
"Multiplication Left-Distributes Over Addition", forall a. SemiringProp a
semiringLeftMultiplicationDistributes Gen a
gen)
, (String
"Multiplication Right-Distributes Over Addition", forall a. SemiringProp a
semiringRightMultiplicationDistributes Gen a
gen)
, (String
"Multiplicative Left Annihilation", forall a. SemiringProp a
semiringLeftAnnihilation Gen a
gen)
, (String
"Multiplicative Right Annihilation", forall a. SemiringProp a
semiringRightAnnihilation Gen a
gen)
]
ringLaws :: (Ring a, Eq a, Show a) => Gen a -> Laws
ringLaws :: forall a. (Ring a, Eq a, Show a) => Gen a -> Laws
ringLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Ring"
[ (String
"Additive Inverse", forall a. RingProp a
ringAdditiveInverse Gen a
gen)
]
starLaws :: (Star a, Eq a, Show a) => Gen a -> Laws
starLaws :: forall a. (Star a, Eq a, Show a) => Gen a -> Laws
starLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Star"
[ (String
"Asteration", forall a. StarProp a
starAsteration Gen a
gen)
, (String
"APlus", 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 :: forall a. RingProp a
ringAdditiveInverse Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Ring a => a -> a
negate a
a forall a. Semiring a => a -> a -> a
+ a
a
let rhs :: a
rhs = forall a. Semiring a => a
zero :: a
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
a; showZ :: String
showZ = forall a. Show a => a -> String
show (forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"negate a + a" String -> String -> String
`congruency` String
"zero, where"
, String
"a = " forall a. [a] -> [a] -> [a]
++ String
showA
, String
"zero = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
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 :: forall a. SemiringProp a
semiringAdditiveLeftIdentity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Semiring a => a
zero forall a. Semiring a => a -> a -> a
+ a
x
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showZ :: String
showZ = forall a. Show a => a -> String
show (forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"zero + x" String -> String -> String
`congruency` String
"x, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringAdditiveRightIdentity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a
x forall a. Semiring a => a -> a -> a
+ forall a. Semiring a => a
zero
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showZ :: String
showZ = forall a. Show a => a -> String
show (forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"x + zero" String -> String -> String
`congruency` String
"x, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringAdditiveAssociativity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
c <- 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. Semiring a => a -> a -> a
+ (a
b forall a. Semiring a => a -> a -> a
+ a
c)
let rhs :: a
rhs = (a
a forall a. Semiring a => a -> a -> a
+ a
b) forall a. Semiring a => a -> a -> a
+ a
c
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
a; showY :: String
showY = forall a. Show a => a -> String
show a
b; showZ :: String
showZ = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
, String
"z = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringAdditiveCommutativity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- 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. Semiring a => a -> a -> a
+ a
b
let rhs :: a
rhs = a
b forall a. Semiring a => a -> a -> a
+ a
a
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
a; showY :: String
showY = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
]
}
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 :: forall a. SemiringProp a
semiringMultiplicativeLeftIdentity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Semiring a => a
one forall a. Semiring a => a -> a -> a
* a
x
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showO :: String
showO = forall a. Show a => a -> String
show (forall a. Semiring a => a
one :: a);
in [String] -> String
lawWhere
[ String
"one * x" String -> String -> String
`congruency` String
"x, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " forall a. [a] -> [a] -> [a]
++ String
showO
]
}
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 :: forall a. SemiringProp a
semiringMultiplicativeRightIdentity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a
x forall a. Semiring a => a -> a -> a
* forall a. Semiring a => a
one
let rhs :: a
rhs = a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showO :: String
showO = forall a. Show a => a -> String
show (forall a. Semiring a => a
one :: a);
in [String] -> String
lawWhere
[ String
"x * one" String -> String -> String
`congruency` String
"x, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " forall a. [a] -> [a] -> [a]
++ String
showO
]
}
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 :: forall a. SemiringProp a
semiringMultiplicativeAssociativity Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
c <- 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. Semiring a => a -> a -> a
* (a
b forall a. Semiring a => a -> a -> a
* a
c)
let rhs :: a
rhs = (a
a forall a. Semiring a => a -> a -> a
* a
b) forall a. Semiring a => a -> a -> a
* a
c
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
a; showY :: String
showY = forall a. Show a => a -> String
show a
b; showZ :: String
showZ = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
, String
"z = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringLeftMultiplicationDistributes Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
c <- 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. Semiring a => a -> a -> a
* (a
b forall a. Semiring a => a -> a -> a
+ a
c)
let rhs :: a
rhs = (a
a forall a. Semiring a => a -> a -> a
* a
b) forall a. Semiring a => a -> a -> a
+ (a
a forall a. Semiring a => a -> a -> a
* a
c)
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
a; showY :: String
showY = forall a. Show a => a -> String
show a
b; showZ :: String
showZ = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
, String
"z = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringRightMultiplicationDistributes Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
b <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
a
c <- 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. Semiring a => a -> a -> a
+ a
b) forall a. Semiring a => a -> a -> a
* a
c
let rhs :: a
rhs = (a
a forall a. Semiring a => a -> a -> a
* a
c) forall a. Semiring a => a -> a -> a
+ (a
b forall a. Semiring a => a -> a -> a
* a
c)
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
a; showY :: String
showY = forall a. Show a => a -> String
show a
b; showZ :: String
showZ = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
, String
"z = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringLeftAnnihilation Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Semiring a => a
zero forall a. Semiring a => a -> a -> a
* a
x
let rhs :: a
rhs = forall a. Semiring a => a
zero
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showZ :: String
showZ = forall a. Show a => a -> String
show (forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"zero * x" String -> String -> String
`congruency` String
"zero, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. SemiringProp a
semiringRightAnnihilation Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a
x forall a. Semiring a => a -> a -> a
* forall a. Semiring a => a
zero
let rhs :: a
rhs = forall a. Semiring a => a
zero
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showZ :: String
showZ = forall a. Show a => a -> String
show (forall a. Semiring a => a
zero :: a);
in [String] -> String
lawWhere
[ String
"x * zero" String -> String -> String
`congruency` String
"zero, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"zero = " forall a. [a] -> [a] -> [a]
++ String
showZ
]
}
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 :: forall a. StarProp a
starAsteration Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Star a => a -> a
star a
x
let rhs :: a
rhs = forall a. Semiring a => a
one forall a. Semiring a => a -> a -> a
+ a
x forall a. Semiring a => a -> a -> a
* forall a. Star a => a -> a
star a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show a
x; showOne :: String
showOne = forall a. Show a => a -> String
show (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 = " forall a. [a] -> [a] -> [a]
++ String
showX
, String
"one = " forall a. [a] -> [a] -> [a]
++ String
showOne
]
}
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 :: forall a. StarProp a
starAplus Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
a
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = forall a. Star a => a -> a
aplus a
x
let rhs :: a
rhs = a
x forall a. Semiring a => a -> a -> a
* forall a. Star a => a -> a
star a
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = 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 = " forall a. [a] -> [a] -> [a]
++ String
showX
]
}
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
#endif