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