{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
module SimplifyLaws (simplifyLaws) where
import Test.Tasty
import Test.Tasty.QuickCheck as QC
import Data.Algebra.Boolean.CoBoolean
import Data.Algebra.Boolean.NormalForm
simplifyProperty :: (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool)) => nf (Either a Bool) -> Bool
simplifyProperty nf = toBooleanWith toBoolean (simplify f nf) == (toBooleanWith toBoolean nf :: Bool)
where f (Right b) = Just b
f (Left _) = Nothing
simplifyLaws :: forall a nf. (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool), Show (nf (Either a Bool)), Arbitrary (nf (Either a Bool))) => nf (Either a Bool) -> TestTree
simplifyLaws _ = QC.testProperty "simplify property" prop
where prop :: nf (Either a Bool) -> Bool
prop = simplifyProperty