    {-# 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", 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 :: 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", 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 :: forall a. (Star a, Eq a, Show a) => 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 :: forall a. RingProp a
    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 <- 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 -> 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
    forall a. Semiring a => a
    zero :: a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs ctx

    semiringAdditiveLeftIdentity :: forall a. SemiringProp a
    semiringAdditiveLeftIdentity :: forall a. SemiringProp a
    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
      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
    forall a. Semiring a => a
    zero a -> a -> a
    forall a. Semiring a => a -> a -> a
    + a
    x
      let rhs = a
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringAdditiveRightIdentity :: forall a. SemiringProp a
    semiringAdditiveRightIdentity :: forall a. SemiringProp a
    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
      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
    x a -> a -> a
    forall a. Semiring a => a -> a -> a
    + a
    forall a. Semiring a => a
    zero
      let rhs = a
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringAdditiveAssociativity :: forall a. SemiringProp a
    semiringAdditiveAssociativity :: forall a. SemiringProp a
    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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      c <- forAll gen
      let 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
    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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringAdditiveCommutativity :: forall a. SemiringProp a
    semiringAdditiveCommutativity :: forall a. SemiringProp a
    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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      let lhs = a
    a a -> a -> a
    forall a. Semiring a => a -> a -> a
    + a
    b
      let rhs = a
    b a -> a -> a
    forall a. Semiring a => a -> a -> a
    + a
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringMultiplicativeLeftIdentity :: forall a. SemiringProp a
    semiringMultiplicativeLeftIdentity :: forall a. SemiringProp a
    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
      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
    forall a. Semiring a => a
    one a -> a -> a
    forall a. Semiring a => a -> a -> a
    * a
    x
      let rhs = a
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringMultiplicativeRightIdentity :: forall a. SemiringProp a
    semiringMultiplicativeRightIdentity :: forall a. SemiringProp a
    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
      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
    x a -> a -> a
    forall a. Semiring a => a -> a -> a
    * a
    forall a. Semiring a => a
    one
      let rhs = a
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringMultiplicativeAssociativity :: forall a. SemiringProp a
    semiringMultiplicativeAssociativity :: forall a. SemiringProp a
    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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      c <- forAll gen
      let 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
    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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringLeftMultiplicationDistributes :: forall a. SemiringProp a
    semiringLeftMultiplicationDistributes :: forall a. SemiringProp a
    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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      c <- forAll gen
      let 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
    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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringRightMultiplicationDistributes :: forall a. SemiringProp a
    semiringRightMultiplicationDistributes :: forall a. SemiringProp a
    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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      c <- forAll gen
      let 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
    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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringLeftAnnihilation :: forall a. SemiringProp a
    semiringLeftAnnihilation :: forall a. SemiringProp a
    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
      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
    forall a. Semiring a => a
    zero a -> a -> a
    forall a. Semiring a => a -> a -> a
    * a
    x
      let rhs = a
    forall a. Semiring a => a
    zero

      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    semiringRightAnnihilation :: forall a. SemiringProp a
    semiringRightAnnihilation :: forall a. SemiringProp a
    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
      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
    x a -> a -> a
    forall a. Semiring a => a -> a -> a
    * a
    forall a. Semiring a => a
    zero
      let rhs = a
    forall a. Semiring a => a
    zero
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    starAsteration :: forall a. StarProp a
    starAsteration :: forall a. StarProp a
    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
      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 -> a
    forall a. Star a => a -> a
    star a
    x
      let 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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    starAplus :: forall a. StarProp a
    starAplus :: forall a. StarProp a
    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
      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 -> a
    forall a. Star a => a -> a
    aplus a
    x
      let 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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
                  ]
            }
      heqCtx lhs rhs ctx

    #endif