hedgehog-classes 0.1.1.0 → 0.1.2
raw patch · 10 files changed
+418/−120 lines, 10 filesdep +semiringsdep ~basedep ~containersdep ~pretty-showPVP ok
version bump matches the API change (PVP)
Dependencies added: semirings
Dependency ranges changed: base, containers, pretty-show, wl-pprint-annotated
API changes (from Hackage documentation)
+ Hedgehog.Classes: ringLaws :: (Ring a, Eq a, Show a) => Gen a -> Laws
+ Hedgehog.Classes: semiringLaws :: (Semiring a, Eq a, Show a) => Gen a -> Laws
+ Hedgehog.Classes: starLaws :: (Star a, Eq a, Show a) => Gen a -> Laws
Files
- CHANGELOG.md +12/−0
- README.md +10/−8
- hedgehog-classes.cabal +22/−26
- src/Hedgehog/Classes.hs +18/−4
- src/Hedgehog/Classes/Common/Compat.hs +0/−38
- src/Hedgehog/Classes/Common/Gen.hs +4/−0
- src/Hedgehog/Classes/Common/Property.hs +0/−40
- src/Hedgehog/Classes/Eq.hs +0/−1
- src/Hedgehog/Classes/Foldable.hs +3/−3
- src/Hedgehog/Classes/Semiring.hs +349/−0
CHANGELOG.md view
@@ -3,6 +3,18 @@ `hedgehog-classes` uses [PVP Versioning][1]. The changelog is available [on GitHub][2]. +0.1.2+=====++* add `semiringLaws`, `ringLaws`, `starLaws`+* fix bug in `foldableLaws` that could cause implementations of+ `foldMap` and `fold` that evaluate in weird orders to pass (rather than fail).++0.1.1+=====++* Initial (stable) hackage release.+ 0.0.0 =====
README.md view
@@ -7,7 +7,7 @@ ## Motivation -`hedgehog-classes` is a wrapper around [Hedgehog](http://hedgehog.qa/) that aims to provide a simple, straightforward API for testing common typeclass laws <i>quickly</i>, while providing good error messages in helping debug any failing tests. It is inspired by the [quickcheck-classes](http://hackage.haskell.org/package/quickcheck-classes) library.+`hedgehog-classes` is a wrapper around [Hedgehog](http://hedgehog.qa/) that aims to provide a simple, straightforward API for testing common typeclass laws <i>quickly</i>, while providing good error messages to help debug any failing tests. It is inspired by the [quickcheck-classes](http://hackage.haskell.org/package/quickcheck-classes) library. ## API Overview @@ -24,7 +24,7 @@ It is a typeclass name along with a list of named property tests. -The second part of `hedgehog-classes` are the functions, which follow a simple structure. All functions in `hedgehog-classes` have one of the following three type signatures, based on the kind of the type which the corresponding typeclass parameterises. Below, 'Ctx' refers to the typeclass in question:+The second part of `hedgehog-classes` are the functions, which follow a simple structure. All functions in `hedgehog-classes` have one of the following three type signatures, based on the kind of the type which the corresponding typeclass parameterises (Nullary, Unary, or Binary). Note that they all return a 'Laws', only the inputs are different. Below, 'Ctx' refers to the typeclass in question: ```haskell -- Typeclasses that have kind 'Type -> Constraint', e.g. 'Eq'@@ -45,9 +45,7 @@ ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws ``` -The third and last part of `hedgehog-classes` are the three convenience functions used to run--your tests. They all return an `IO Bool`, where `True` is returned if all the tests pass, and `False` otherwise. They are as following:+The third and last part of `hedgehog-classes` are the three convenience functions used to run your tests. They all return an `IO Bool`, where `True` is returned if all the tests pass, and `False` otherwise. They are as following: ```haskell -- Test a single typeclasses' laws.@@ -61,7 +59,7 @@ lawsCheckMany :: [(String, [Laws])] -> IO Bool ``` -That is all there is to using `hedgehog-classes` in your test suite. For usage examples, see the [haddocks](http://hackage.haskell.org/package/hedgehog-classes)+That is all there is to using `hedgehog-classes` in your test suite. For usage examples, see the [haddocks](http://hackage.haskell.org/package/hedgehog-classes). ## Distributing your own `Laws` @@ -86,7 +84,8 @@ - Does not make an effort to provide custom error messages - Currently the only thing `hedgehog-checkers` can do that this library cannot is test properties of higher-kinded typeclass laws where the construction of- the type + the type requires constraints on its type arguments (e.g. `Ord` for something+ like `Data.Set.Set`) - [hedgehog-laws](https://github.com/qfpl/hedgehog-laws): - All of the things that apply to `hedgehog-checkers`, but even more incomplete.@@ -122,6 +121,9 @@ - `aeson` - ToJSON - ToJSON/FromJSON+ - `semirings`+ - Semiring+ - Ring Some typeclasses can have additional laws, which are not part of their sufficient definition. A common example is commutativity of a monoid. In such cases where this is sensible, `hedgehog-classes` provides functions such `commutativeMonoidLaws`, `commutativeSemigroupLaws`, etc. `hedgehog-classes` also tests that `foldl'`/`foldr'` actually accumulate strictly. There are other such cases that are documented on Hackage. @@ -138,7 +140,7 @@ To use this library to export your own `Laws` functions which you wish to distribute, add it to the library stanza of your cabal file. [hackage]: http://hackage.haskell.org/package/hedgehog-classes- [hackage-shield]: https://img.shields.io/badge/hackage-v0.6.1-blue.svg+ [hackage-shield]: https://img.shields.io/badge/hackage-v0.1.1.0-blue.svg ## Improvements
hedgehog-classes.cabal view
@@ -1,8 +1,8 @@-cabal-version: 2.0+cabal-version: 2.4 name: hedgehog-classes version:- 0.1.1.0+ 0.1.2 synopsis: Hedgehog will eat your typeclass bugs description:@@ -20,7 +20,7 @@ bug-reports: https://github.com/chessai/hedgehog-classes/issues license:- BSD3+ BSD-3-Clause license-file: LICENSE author:@@ -52,19 +52,19 @@ -- flag semigroupoids -- description:--- You can disable the use of the `semirings` package using `-f-semirings`.+-- You can disable the use of the `semigroupoids` package using `-f-semigroupoids`. -- . -- This may be useful for accelerating builds in sandboxes for expert users. -- default: True -- manual: True --- flag semirings--- description:--- You can disable the use of the `semirings` package using `-f-semirings`.--- .--- This may be useful for accelerating builds in sandboxes for expert users.--- default: True--- manual: True+flag semirings+ description:+ You can disable the use of the `semirings` package using `-f-semirings`.+ .+ This may be useful for accelerating builds in sandboxes for expert users.+ default: True+ manual: True library hs-source-dirs:@@ -108,35 +108,31 @@ Hedgehog.Classes.Monoid Hedgehog.Classes.Ord Hedgehog.Classes.Semigroup--- Hedgehog.Classes.Semiring+ Hedgehog.Classes.Semiring Hedgehog.Classes.Show Hedgehog.Classes.ShowRead Hedgehog.Classes.Storable Hedgehog.Classes.Traversable build-depends:- base >= 4.12.0.0 && < 4.14.0.0- , hedgehog >= 0.5.0.0 && < 0.7.0.0- , containers >= 0.5.9.2 && < 0.7.0.0- , pretty-show >= 1.6.0.0 && < 2.0.0.0- , transformers >= 0.5.0.0 && < 0.6.0.0- , wl-pprint-annotated >= 0.0.0.0 && < 0.2.0.0+ , base >= 4.12 && < 4.14+ , hedgehog >= 0.5 && < 0.7+ , containers >= 0.5 && < 0.7+ , pretty-show >= 1.6 && < 2.0+ , transformers >= 0.5 && < 0.6+ , wl-pprint-annotated >= 0.0 && < 0.2 ghc-options: -Wall default-language: Haskell2010- if impl(ghc < 8.5)- buildable: False- if impl(ghc >= 8.5)- cpp-options: -DHAVE_QUANTIFIED_CONSTRAINTS if flag(aeson)- build-depends: aeson >= 0.9.0.0 && < 1.5.0.0+ build-depends: aeson >= 0.9 && < 1.5 cpp-options: -DHAVE_AESON -- if flag(semigroupoids) -- build-depends: semigroupoids >= 0.5.3.0 && < 0.6.0.0 -- cpp-options: -DHAVE_SEMIGROUPOIDS--- if flag(semirings)--- build-depends: semirings >= 0.3.1.1 && < 0.4.0.0--- cpp-options: -DHAVE_SEMIRINGS+ if flag(semirings)+ build-depends: semirings >= 0.2 && < 0.4+ cpp-options: -DHAVE_SEMIRINGS -- if flag(vector) -- build-depends: vector >= 0.12.0.0 && < 0.13.0.0 -- cpp-options: -DHAVE_VECTOR
src/Hedgehog/Classes.hs view
@@ -1,3 +1,5 @@+{-# language CPP #-}+ {-| This library provides sets of properties that should hold for common typeclasses. @@ -27,12 +29,19 @@ , exponentialSemigroupLaws , idempotentSemigroupLaws , rectangularBandSemigroupLaws+#if HAVE_AESON + , jsonLaws+#endif+ , genericLaws+#if HAVE_SEMIRINGS+ , semiringLaws+ , ringLaws+ , starLaws+#endif , showLaws , showReadLaws , storableLaws- , genericLaws- , jsonLaws-+ -- ** Unary type constructors , alternativeLaws , applicativeLaws@@ -55,7 +64,7 @@ , categoryLaws , commutativeCategoryLaws - -- * Defining your own laws+ -- * Defining your own 'Laws' , Laws(..) , LawContext(..) , Context(..)@@ -86,7 +95,9 @@ import Hedgehog.Classes.Generic (genericLaws) import Hedgehog.Classes.Integral (integralLaws) --import Hedgehog.Classes.Ix (ixLaws)+#if HAVE_AESON import Hedgehog.Classes.Json (jsonLaws)+#endif import Hedgehog.Classes.Monad (monadLaws) import Hedgehog.Classes.MonadIO (monadIOLaws) import Hedgehog.Classes.MonadPlus (monadPlusLaws)@@ -94,6 +105,9 @@ import Hedgehog.Classes.Monoid (monoidLaws, commutativeMonoidLaws) import Hedgehog.Classes.Ord (ordLaws) import Hedgehog.Classes.Semigroup (semigroupLaws, commutativeSemigroupLaws, exponentialSemigroupLaws, idempotentSemigroupLaws, rectangularBandSemigroupLaws)+#if HAVE_SEMIRINGS+import Hedgehog.Classes.Semiring (semiringLaws, ringLaws, starLaws)+#endif import Hedgehog.Classes.Show (showLaws) import Hedgehog.Classes.ShowRead (showReadLaws) import Hedgehog.Classes.Storable (storableLaws)
src/Hedgehog/Classes/Common/Compat.hs view
@@ -1,8 +1,4 @@-{-# LANGUAGE CPP #-}--#if HAVE_QUANTIFIED_CONSTRAINTS {-# LANGUAGE QuantifiedConstraints #-}-#endif module Hedgehog.Classes.Common.Compat ( readMaybe@@ -18,10 +14,6 @@ , neq2 ) where -#if HAVE_QUANTIFIED_CONSTRAINTS == 0-import qualified Data.Functor.Classes as C-#endif- import Text.Read (readMaybe) eq :: Eq a => a -> a -> Bool@@ -30,50 +22,20 @@ neq :: Eq a => a -> a -> Bool neq = (/=) -#if HAVE_QUANTIFIED_CONSTRAINTS eq1 :: (Eq a, forall x. Eq x => Eq (f x)) => f a -> f a -> Bool eq1 = (==)-#else-eq1 :: (C.Eq1 f, Eq a) => f a -> f a -> Bool-eq1 = C.eq1-#endif -#if HAVE_QUANTIFIED_CONSTRAINTS neq1 :: (Eq a, forall x. Eq x => Eq (f x)) => f a -> f a -> Bool neq1 = (/=)-#else-neq1 :: (C.Eq1 f, Eq a) => f a -> f a -> Bool-neq1 x y = not $ C.eq1 x y -#endif -#if HAVE_QUANTIFIED_CONSTRAINTS eq2 :: (Eq a, Eq b, forall x y. (Eq x, Eq y) => Eq (f x y)) => f a b -> f a b -> Bool eq2 = (==)-#else-eq2 :: (C.Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool-eq2 = C.eq2-#endif -#if HAVE_QUANTIFIED_CONSTRAINTS neq2 :: (Eq a, Eq b, forall x y. (Eq x, Eq y) => Eq (f x y)) => f a b -> f a b -> Bool neq2 = (/=)-#else-neq2 :: (C.Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool-neq2 x y = not $ C.eq2 x y-#endif -#if HAVE_QUANTIFIED_CONSTRAINTS show1 :: (Show a, forall x. (Show x) => Show (f x)) => f a -> String show1 = Prelude.show-#else-show1 :: (C.Show1 f, Show a) => f a -> String-show1 x = C.showsPrec1 0 x ""-#endif -#if HAVE_QUANTIFIED_CONSTRAINTS show2 :: (Show a, Show b, forall x y. (Show x, Show y) => Show (f x y)) => f a b -> String show2 = Prelude.show-#else-show2 :: (C.Show2 f, Show a, Show b) => f a b -> String-show2 x = C.showsPrec2 0 x ""-#endif
src/Hedgehog/Classes/Common/Gen.hs view
@@ -2,6 +2,7 @@ module Hedgehog.Classes.Common.Gen ( genSmallList+ , genVerySmallList , genSmallNonEmptyList , genShowReadPrecedence , genSmallString@@ -36,6 +37,9 @@ genSmallList :: Gen a -> Gen [a] genSmallList gen = Gen.list (Range.linear 0 6) gen++genVerySmallList :: Gen a -> Gen [a]+genVerySmallList gen = Gen.list (Range.linear 0 2) gen genSmallString :: Gen String genSmallString = Gen.string (Range.linear 0 6) Gen.ascii
src/Hedgehog/Classes/Common/Property.hs view
@@ -4,10 +4,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}--#if HAVE_QUANTIFIED_CONSTRAINTS {-# LANGUAGE QuantifiedConstraints #-}-#endif -- | This module exports hedgehog comparison tests -- that don't contain CallStack information, since this would@@ -32,10 +29,6 @@ import qualified Data.Char as Char import qualified Data.List as List -#if HAVE_QUANTIFIED_CONSTRAINTS == 0-import qualified Data.Functor.Classes as C-#endif- bar :: String bar = "━━━" @@ -156,12 +149,8 @@ , HasCallStack , Eq a , Show a-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x. Eq x => Eq (f x) , forall x. Show x => Show (f x)-#else- , C.Eq1 f, C.Show1 f-#endif ) => f a -> f a -> Context -> m () hneqCtx1 x y ctx = do ok <- withFrozenCallStack $ evalNoSrc (x `neq1` y)@@ -176,12 +165,8 @@ , HasCallStack , Eq a , Show a-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x. Eq x => Eq (f x) , forall x. Show x => Show (f x)-#else- , C.Eq1 f, C.Show1 f-#endif ) => f a -> f a -> m () hneq1 x y = hneqCtx1 x y NoContext @@ -192,12 +177,8 @@ , HasCallStack , Eq a , Show a-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x. Eq x => Eq (f x) , forall x. Show x => Show (f x)-#else- , C.Eq1 f, C.Show1 f-#endif ) => f a -> f a -> Context -> m () heqCtx1 x y ctx = do ok <- withFrozenCallStack $ evalNoSrc (x `eq1` y)@@ -212,12 +193,8 @@ , HasCallStack , Eq a , Show a-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x. Eq x => Eq (f x) , forall x. Show x => Show (f x)-#else- , C.Eq1 f, C.Show1 f-#endif ) => f a -> f a -> m () heq1 x y = heqCtx1 x y NoContext @@ -232,12 +209,8 @@ , Eq b , Show a , Show b-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x y. (Eq x, Eq y) => Eq (f x y) , forall x y. (Show x, Show y) => Show (f x y)-#else- , C.Eq2 f, C.Show2 f-#endif ) => f a b -> f a b -> Context -> m () heqCtx2 x y ctx = do ok <- withFrozenCallStack $ evalNoSrc (x `eq2` y)@@ -254,12 +227,8 @@ , Eq b , Show a , Show b-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x y. (Eq x, Eq y) => Eq (f x y) , forall x y. (Show x, Show y) => Show (f x y)-#else- , C.Eq2 f, C.Show2 f-#endif ) => f a b -> f a b -> m () heq2 x y = heqCtx2 x y NoContext @@ -274,12 +243,8 @@ , Eq b , Show a , Show b-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x y. (Eq x, Eq y) => Eq (f x y) , forall x y. (Show x, Show y) => Show (f x y)-#else- , C.Eq2 f, C.Show2 f-#endif ) => f a b -> f a b -> Context -> m () hneqCtx2 x y ctx = do ok <- withFrozenCallStack $ evalNoSrc (x `neq2` y)@@ -296,12 +261,7 @@ , Eq b , Show a , Show b-#if HAVE_QUANTIFIED_CONSTRAINTS , forall x y. (Eq x, Eq y) => Eq (f x y) , forall x y. (Show x, Show y) => Show (f x y)-#else- , C.Eq2 f, C.Show2 f-#endif ) => f a b -> f a b -> m () hneq2 x y = hneqCtx2 x y NoContext-
src/Hedgehog/Classes/Eq.hs view
@@ -10,7 +10,6 @@ -- [__Reflexivity__]: @x '==' x@ ≡ @'True'@ -- [__Symmetry__]: @x '==' y@ ≡ @y '==' x@ -- [__Transitivity__]: @x '==' y '&&' y '==' z@ ≡ @x '==' z@--- [__Substitutivity__]: @x '==' y@ ≡ @f x '==' f y@ -- [__Negation__]: @x '/=' y@ ≡ @'not' (x '==' y)@ eqLaws :: (Eq a, Show a) => Gen a -> Laws eqLaws gen = Laws "Eq"
src/Hedgehog/Classes/Foldable.hs view
@@ -51,7 +51,7 @@ , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x) ) => (forall x. Gen x -> Gen (f x)) -> Property foldableFold fgen = property $ do- a <- forAll $ fgen genSmallSum+ a <- forAll $ fgen $ genVerySmallList genSmallInteger let lhs = Foldable.fold a let rhs = Foldable.foldMap id a let ctx = contextualise $ LawContext@@ -76,7 +76,7 @@ foldableFoldMap fgen = property $ do a <- forAll $ fgen genSmallInteger e <- forAll genQuadraticEquation- let f = Sum . runQuadraticEquation e+ let f = (:[]) . runQuadraticEquation e let lhs = Foldable.foldMap f a let rhs = Foldable.foldr (mappend . f) mempty a let ctx = contextualise $ LawContext@@ -85,7 +85,7 @@ , lawContextTcName = "Foldable" , lawContextTcProp = let showA = show a- showF = "Sum $ " ++ show e+ showF = "(:[]) $ " ++ show e in lawWhere [ "foldMap f a" `congruency` "foldr (mappend . f) mempty a, where" , "f = " ++ showF
+ src/Hedgehog/Classes/Semiring.hs view
@@ -0,0 +1,349 @@+{-# 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 = Laws "Semiring"+ [ ("Additive Left Identity", semiringAdditiveLeftIdentity gen)+ , ("Additive Right Identity", semiringAdditiveRightIdentity gen)+ , ("Additive Associativity", semiringAdditiveAssociativity gen)+ , ("Additive Commutativity", semiringAdditiveCommutativity gen)+ , ("Multiplicative Left Identity", semiringMultiplicativeLeftIdentity gen)+ , ("Multiplicative Right Identity", semiringMultiplicativeRightIdentity gen)+ , ("Multiplicative Associativity", semiringMultiplicativeAssociativity gen)+ , ("Multiplication Left-Distributes Over Addition", semiringLeftMultiplicationDistributes gen)+ , ("Multiplication Right-Distributes Over Addition", semiringRightMultiplicationDistributes gen)+ , ("Multiplicative Left Annihilation", semiringLeftAnnihilation gen) + , ("Multiplicative Right Annihilation", semiringRightAnnihilation gen) + ]++-- | Tests the following 'Ring' laws:+--+-- [__Additive Inverse__]: @'negate' x '+' x@ ≡ @'zero'@+ringLaws :: (Ring a, Eq a, Show a) => Gen a -> Laws+ringLaws gen = Laws "Ring"+ [ ("Additive Inverse", ringAdditiveInverse 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 = Laws "Star"+ [ ("Asteration", starAsteration gen)+ , ("APlus", starAplus 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 = property $ do+ a <- forAll gen+ let lhs = negate a + a+ let rhs = zero :: a+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Additive Inverse", lawContextTcName = "Ring"+ , lawContextLawBody = "negate a + a" `congruency` "zero"+ , lawContextTcProp =+ let showA = show a; showZ = show (zero :: a);+ in lawWhere+ [ "negate a + a" `congruency` "zero, where"+ , "a = " ++ showA + , "zero = " ++ showZ+ ]+ , lawContextReduced = reduced lhs rhs+ }+ heqCtx lhs rhs ctx++semiringAdditiveLeftIdentity :: forall a. SemiringProp a+semiringAdditiveLeftIdentity gen = property $ do+ x <- forAll gen+ let lhs = zero + x+ let rhs = x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Additive Left Identity", lawContextTcName = "Semiring"+ , lawContextLawBody = "zero + x" `congruency` "x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showZ = show (zero :: a);+ in lawWhere+ [ "zero + x" `congruency` "x, where"+ , "x = " ++ showX+ , "zero = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++semiringAdditiveRightIdentity :: forall a. SemiringProp a+semiringAdditiveRightIdentity gen = property $ do+ x <- forAll gen+ let lhs = x + zero+ let rhs = x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Additive Right Identity", lawContextTcName = "Semiring"+ , lawContextLawBody = "x + zero" `congruency` "x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showZ = show (zero :: a);+ in lawWhere+ [ "x + zero" `congruency` "x, where"+ , "x = " ++ showX+ , "zero = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++semiringAdditiveAssociativity :: forall a. SemiringProp a+semiringAdditiveAssociativity gen = property $ do+ a <- forAll gen+ b <- forAll gen+ c <- forAll gen+ let lhs = a + (b + c)+ let rhs = (a + b) + c+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Additive Associativity", lawContextTcName = "Semiring"+ , lawContextLawBody = "x + (y + z)" `congruency` "(x + y) + z"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show a; showY = show b; showZ = show c;+ in lawWhere+ [ "x + (y + z)" `congruency` "(x + y) + z, where"+ , "x = " ++ showX+ , "y = " ++ showY+ , "z = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++semiringAdditiveCommutativity :: forall a. SemiringProp a+semiringAdditiveCommutativity gen = property $ do+ a <- forAll gen+ b <- forAll gen+ let lhs = a + b+ let rhs = b + a+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Additive Commutativity", lawContextTcName = "Semiring"+ , lawContextLawBody = "x + y" `congruency` "y + x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show a; showY = show b;+ in lawWhere+ [ "x + y" `congruency` "y + x, where"+ , "x = " ++ showX+ , "y = " ++ showY+ ]+ } + heqCtx lhs rhs ctx++semiringMultiplicativeLeftIdentity :: forall a. SemiringProp a+semiringMultiplicativeLeftIdentity gen = property $ do+ x <- forAll gen+ let lhs = one * x+ let rhs = x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplicative Left Identity", lawContextTcName = "Semiring"+ , lawContextLawBody = "one * x" `congruency` "x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showO = show (one :: a);+ in lawWhere+ [ "one * x" `congruency` "x, where"+ , "x = " ++ showX+ , "one = " ++ showO+ ] + } + heqCtx lhs rhs ctx+ +semiringMultiplicativeRightIdentity :: forall a. SemiringProp a+semiringMultiplicativeRightIdentity gen = property $ do+ x <- forAll gen+ let lhs = x * one+ let rhs = x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplicative Right Identity", lawContextTcName = "Semiring"+ , lawContextLawBody = "x * one" `congruency` "x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showO = show (one :: a);+ in lawWhere+ [ "x * one" `congruency` "x, where"+ , "x = " ++ showX+ , "one = " ++ showO+ ]+ } + heqCtx lhs rhs ctx++semiringMultiplicativeAssociativity :: forall a. SemiringProp a+semiringMultiplicativeAssociativity gen = property $ do+ a <- forAll gen+ b <- forAll gen+ c <- forAll gen+ let lhs = a * (b * c)+ let rhs = (a * b) * c+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplicative Associativity", lawContextTcName = "Semiring"+ , lawContextLawBody = "x * (y * z)" `congruency` "(x * y) * z"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show a; showY = show b; showZ = show c;+ in lawWhere+ [ "x * (y * z)" `congruency` "(x * y) * z, where"+ , "x = " ++ showX+ , "y = " ++ showY+ , "z = " ++ showZ+ ] + } + heqCtx lhs rhs ctx++semiringLeftMultiplicationDistributes :: forall a. SemiringProp a+semiringLeftMultiplicationDistributes gen = property $ do+ a <- forAll gen+ b <- forAll gen+ c <- forAll gen+ let lhs = a * (b + c)+ let rhs = (a * b) + (a * c)+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplication Left-Distributes Over Addition", lawContextTcName = "Semiring"+ , lawContextLawBody = "x * (y + z)" `congruency` "(x * y) + (x * z)"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show a; showY = show b; showZ = show c;+ in lawWhere+ [ "x * (y + z)" `congruency` "(x * y) + (x * z), where"+ , "x = " ++ showX+ , "y = " ++ showY+ , "z = " ++ showZ+ ] + } + heqCtx lhs rhs ctx++semiringRightMultiplicationDistributes :: forall a. SemiringProp a+semiringRightMultiplicationDistributes gen = property $ do+ a <- forAll gen+ b <- forAll gen+ c <- forAll gen+ let lhs = (a + b) * c+ let rhs = (a * c) + (b * c)+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplication Right-Distributes Over Addition", lawContextTcName = "Semiring"+ , lawContextLawBody = "(y + z) * x" `congruency` "(y * x) + (z * x)"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show a; showY = show b; showZ = show c;+ in lawWhere+ [ "(y + z) * x" `congruency` "(y * x) + (z * x), where"+ , "x = " ++ showX+ , "y = " ++ showY+ , "z = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++semiringLeftAnnihilation :: forall a. SemiringProp a+semiringLeftAnnihilation gen = property $ do+ x <- forAll gen+ let lhs = zero * x+ let rhs = zero++ let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplicative Left Annihilation", lawContextTcName = "Semiring"+ , lawContextLawBody = "zero * x" `congruency` "zero"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showZ = show (zero :: a);+ in lawWhere+ [ "zero * x" `congruency` "zero, where"+ , "x = " ++ showX+ , "zero = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++semiringRightAnnihilation :: forall a. SemiringProp a+semiringRightAnnihilation gen = property $ do+ x <- forAll gen+ let lhs = x * zero+ let rhs = zero + let ctx = contextualise $ LawContext+ { lawContextLawName = "Multiplicative Right Annihilation", lawContextTcName = "Semiring"+ , lawContextLawBody = "x * zero" `congruency` "zero"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showZ = show (zero :: a);+ in lawWhere+ [ "x * zero" `congruency` "zero, where"+ , "x = " ++ showX+ , "zero = " ++ showZ+ ]+ } + heqCtx lhs rhs ctx++starAsteration :: forall a. StarProp a+starAsteration gen = property $ do+ x <- forAll gen+ let lhs = star x+ let rhs = one + x * star x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "Asteration", lawContextTcName = "Star"+ , lawContextLawBody = "star x" `congruency` "one + x * star x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x; showOne = show (one :: a);+ in lawWhere+ [ "star x" `congruency` "one + x * star x, where"+ , "x = " ++ showX+ , "one = " ++ showOne+ ]+ }+ heqCtx lhs rhs ctx ++starAplus :: forall a. StarProp a+starAplus gen = property $ do+ x <- forAll gen+ let lhs = aplus x+ let rhs = x * star x+ let ctx = contextualise $ LawContext+ { lawContextLawName = "APlus", lawContextTcName = "Star"+ , lawContextLawBody = "aplus x" `congruency` "x * star x"+ , lawContextReduced = reduced lhs rhs+ , lawContextTcProp =+ let showX = show x+ in lawWhere+ [ "aplus x" `congruency` "x * star x, where"+ , "x = " ++ showX+ ]+ }+ heqCtx lhs rhs ctx + +#endif