prednote-0.22.0.0: prednote-test.hs
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Control.Applicative
import qualified Test.QuickCheck as Q
import Test.QuickCheck.All (quickCheckAll)
import Test.QuickCheck.Function
import Test.QuickCheck (Arbitrary, Gen, arbitrary)
import qualified Data.Prednote.Predbox as P
import Data.Prednote.Predbox ((&&&), (|||))
import qualified Data.Text as X
import qualified System.Exit as Exit
instance Arbitrary X.Text where
arbitrary = fmap X.pack (Q.listOf (Q.choose ('!', '~')))
instance Q.CoArbitrary a => Arbitrary (P.Predbox a) where
arbitrary = P.Predbox <$> arbitrary <*> arbitrary <*> arbitrary
instance Q.CoArbitrary a => Arbitrary (P.Node a) where
arbitrary = Q.sized tree
where
tree 0 = fmap P.Predicate arbitrary
tree n = Q.oneof
[ fmap P.And (Q.listOf subtree)
, fmap P.Or (Q.listOf subtree)
, fmap P.Not subtree ]
where
subtree = P.Predbox <$> arbitrary <*> arbitrary
<*> tree (n `div` 2)
-- | And is commutative
prop_andCommutative :: a -> P.Predbox a -> P.Predbox a -> Bool
prop_andCommutative a p1 p2 = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (p1 &&& p2) a
r2 = P.evaluate (p2 &&& p1) a
-- | And is associative
prop_andAssociative :: a -> P.Predbox a -> P.Predbox a -> P.Predbox a -> Bool
prop_andAssociative a p1 p2 p3 = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (p1 &&& (p2 &&& p3)) a
r2 = P.evaluate ((p1 &&& p2) &&& p3) a
-- | Or is commutative
prop_orCommutative :: a -> P.Predbox a -> P.Predbox a -> Bool
prop_orCommutative a p1 p2 = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (p1 ||| p2) a
r2 = P.evaluate (p2 ||| p1) a
-- | Or is associative
prop_orAssociative :: a -> P.Predbox a -> P.Predbox a -> P.Predbox a -> Bool
prop_orAssociative a p1 p2 p3 = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (p1 ||| (p2 ||| p3)) a
r2 = P.evaluate ((p1 ||| p2) ||| p3) a
-- | Anything or'd with True is True
prop_orWithTrue :: a -> P.Predbox a -> Bool
prop_orWithTrue a p1 = P.rBool r1
where
r1 = P.evaluate (p1 ||| P.always) a
-- | Anything and'ed with False is False
prop_andWithFalse :: a -> P.Predbox a -> Bool
prop_andWithFalse a p1 = not $ P.rBool r1
where
r1 = P.evaluate (p1 &&& P.never) a
-- | And Distributivity
prop_andDistributivity :: a -> P.Predbox a -> P.Predbox a -> P.Predbox a -> Bool
prop_andDistributivity x a b c = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (a &&& (b ||| c)) x
r2 = P.evaluate ((a &&& b) ||| (a &&& c)) x
prop_orDistributivity :: a -> P.Predbox a -> P.Predbox a -> P.Predbox a -> Bool
prop_orDistributivity x a b c = P.rBool r1 == P.rBool r2
where
r1 = P.evaluate (a ||| (b &&& c)) x
r2 = P.evaluate ((a ||| b) &&& (a ||| c)) x
runTests = $quickCheckAll
main :: IO ()
main = do
b <- runTests
if b then Exit.exitSuccess else Exit.exitFailure