{-# 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 :: 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) 
  ]

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

-- | 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 :: 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