module BooleanLaws (monotoneLaws, nonMonotoneLaws) where import Test.Tasty import Test.Tasty.QuickCheck as QC import Prelude hiding ((||),(&&),not) import Data.Algebra.Boolean associativityOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool associativityOrProp eq x y z = (x || (y || z)) `eq` ((x || y) || z) associativityAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool associativityAndProp eq x y z = (x || (y || z)) `eq` ((x || y) || z) commutativeOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool commutativeOrProp eq x y = (x || y) `eq` (y || x) commutativeAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool commutativeAndProp eq x y = (x && y) `eq` (y && x) distributivity1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool distributivity1Prop eq x y z = (x && (y || z)) `eq` ((x && y) || (x && z)) distributivity2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool distributivity2Prop eq x y z = (x || (y && z)) `eq` ((x || y) && (x || z)) identityOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool identityOrProp eq x = (x || false) `eq` x identityAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool identityAndProp eq x = (x && true) `eq` x annihilatorOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool annihilatorOrProp eq x = (x || true) `eq` true annihilatorAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool annihilatorAndProp eq x = (x && false) `eq` false idempotenceOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool idempotenceOrProp eq x = (x || x) `eq` x idempotenceAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool idempotenceAndProp eq x = (x && x) `eq` x absorption1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool absorption1Prop eq x y = (x && (x || y)) `eq` x absorption2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool absorption2Prop eq x y = (x || (x && y)) `eq` x complementationOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool complementationOrProp eq x = (x || not x) `eq` true complementationAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool complementationAndProp eq x = (x && not x) `eq` false doubleNegationProp :: Boolean a => (a -> a -> Bool) -> a -> Bool doubleNegationProp eq x = not (not x) `eq` x deMorgan1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool deMorgan1Prop eq x y = (not x && not y) `eq` not (x || y) deMorgan2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool deMorgan2Prop eq x y = (not x || not y) `eq` not (x && y) monotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree monotoneLaws eq = testGroup "Monotone boolean laws" [ QC.testProperty "associativity or" \$ associativityOrProp eq , QC.testProperty "associativity and" \$ associativityAndProp eq , QC.testProperty "commutativity or" \$ commutativeOrProp eq , QC.testProperty "commutativity and" \$ commutativeAndProp eq , QC.testProperty "distributivity 1" \$ distributivity1Prop eq , QC.testProperty "distributivity 2" \$ distributivity2Prop eq , QC.testProperty "identity or" \$ identityOrProp eq , QC.testProperty "identity and" \$ identityAndProp eq , QC.testProperty "annihilator or" \$ annihilatorOrProp eq , QC.testProperty "annihilator and" \$ annihilatorAndProp eq , QC.testProperty "idempotence or" \$ idempotenceOrProp eq , QC.testProperty "idempotence and" \$ idempotenceAndProp eq , QC.testProperty "absorption 1" \$ absorption1Prop eq , QC.testProperty "absorption 2" \$ absorption2Prop eq ] nonMonotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree nonMonotoneLaws eq = testGroup "Non monotone boolean laws" [ QC.testProperty "complementation or" \$ complementationOrProp eq , QC.testProperty "complementation and" \$ complementationAndProp eq , QC.testProperty "double negation" \$ doubleNegationProp eq , QC.testProperty "de Morgan 1" \$ deMorgan1Prop eq , QC.testProperty "de Morgan 2" \$ deMorgan2Prop eq ]