{-# LANGUAGE ScopedTypeVariables #-}
module CNFSet (tests) where
import BooleanLaws
import NegableLaws
import SimplifyLaws
import BooleanModelLaws
import FreeBoolean
import Test.Tasty
import Test.QuickCheck
import Control.Applicative
import Data.Monoid
import Data.Function (on)
import Data.Algebra.Boolean.Negable (Negable)
import Data.Algebra.Boolean.CNF.Set
instance Arbitrary a => Arbitrary (Sum a) where
arbitrary = Sum <$> arbitrary
instance (Ord a, Negable a, Arbitrary a) => Arbitrary (CNF a) where
arbitrary = fromFreeBoolean <$> arbitrary
tests :: TestTree
tests = testGroup "CNF set implementation"
[ monotoneLaws eq
, nonMonotoneLaws eq
, negableLaws eq
, simplifyLaws (undefined :: CNF (Either Bool Bool))
, booleanModelLaws (undefined :: CNF (Either Bool Bool))
]
eq :: CNF (Maybe (Sum Int)) -> CNF (Maybe (Sum Int)) -> Bool
eq = (==) `on` toBool