{-# 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

-- | Tests the following 'Semiring' laws:
--
-- [__Additive Left Identity__]: @'zero' '+' x@ ≡ @x@
-- [__Additive Right Identity__]: @x '+' 'zero'@ ≡ @x@
-- [__Additive Associativity__]: @x '+' (y '+' z)@ ≡ @(x '+' y) '+' z@
-- [__Additive Commutativity__]: @x '+' y@ ≡ @y '+' x@
-- [__Multiplicative Left Identity__]: @'one' '*' x@ ≡ @x@ 
-- [__Multiplicative Right Identity__]: @x '*' 'one'@ ≡ @x@ 
-- [__Multiplicative Associativity__]: @x '*' (y '*' z)@ ≡ @(x '*' y) '*' z@ 
-- [__Multiplicatiion Left-Distributes Over Addtion__]: @x '*' (y '+' z)@ ≡ @(x '*' y) '+' (x '*' z)@ 
-- [__Multiplication Right-Distibutes Over Addition__]: @(y '+' z) '*' x@ ≡ @(y '*' x) '+' (z '*' x)@
-- [__Multiplicative Left Annihilation__]: @'zero' '*' x@ ≡ @'zero'@ 
-- [__Multiplicative Right Annihilation__]: @x '*' 'zero'@ ≡ @'zero'@ 
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) 
  ]

-- | Tests the following 'Ring' laws:
--
-- [__Additive Inverse__]: @'negate' x '+' x@ ≡ @'zero'@
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)
  ]

-- | Tests the following 'Star' laws:
--
-- [__Asteration__]: @'star' x@ ≡ @'one' '+' x '*' 'star' x@
-- [__APlus__]: @'aplus' x@ ≡ @x '*' 'star' x@
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