module Data.BoolExpr
(
Boolean(..)
,BoolExpr(..)
,reduceBoolExpr
,evalBoolExpr
,Signed(..)
,constants
,CNF(..),Conj(..)
,boolTreeToCNF
,reduceCNF
,Disj(..),DNF(..)
,boolTreeToDNF
,reduceDNF
,dualize
,pushNotInwards
)
where
import Control.Applicative
import Data.Monoid (Monoid(..))
import Data.Foldable (Foldable(..))
import Data.Traversable
infix /\
infix \/
class Boolean f where
( /\ ) :: f a -> f a -> f a
( \/ ) :: f a -> f a -> f a
bNot :: f a -> f a
bTrue :: f a
bFalse :: f a
bConst :: a -> f a
data BoolExpr a = BAnd (BoolExpr a) (BoolExpr a)
| BOr (BoolExpr a) (BoolExpr a)
| BNot (BoolExpr a)
| BTrue
| BFalse
| BConst a
deriving (Eq, Ord, Show)
data Signed a = Positive a | Negative a
deriving (Eq, Ord, Show, Read)
instance Functor BoolExpr where
fmap f (BAnd a b) = BAnd (fmap f a) (fmap f b)
fmap f (BOr a b) = BOr (fmap f a) (fmap f b)
fmap f (BNot t) = BNot (fmap f t)
fmap _ BTrue = BTrue
fmap _ BFalse = BFalse
fmap f (BConst x) = BConst (f x)
instance Traversable BoolExpr where
traverse f (BAnd a b) = BAnd <$> traverse f a <*> traverse f b
traverse f (BOr a b) = BOr <$> traverse f a <*> traverse f b
traverse f (BNot t) = BNot <$> traverse f t
traverse _ BTrue = pure BTrue
traverse _ BFalse = pure BFalse
traverse f (BConst x) = BConst <$> f x
instance Foldable BoolExpr where
foldMap = foldMapDefault
instance Boolean BoolExpr where
( /\ ) = BAnd
( \/ ) = BOr
bNot = BNot
bTrue = BTrue
bFalse = BFalse
bConst = BConst
fromBoolExpr :: Boolean f => BoolExpr a -> f a
fromBoolExpr (BAnd l r) = fromBoolExpr l /\ fromBoolExpr r
fromBoolExpr (BOr l r) = fromBoolExpr l \/ fromBoolExpr r
fromBoolExpr (BNot t) = bNot $ fromBoolExpr t
fromBoolExpr BTrue = bTrue
fromBoolExpr BFalse = bFalse
fromBoolExpr (BConst c) = bConst c
newtype Disj a = Disj { unDisj :: [a] }
deriving (Show, Functor, Monoid)
newtype Conj a = Conj { unConj :: [a] }
deriving (Show, Functor, Monoid)
newtype CNF a = CNF { unCNF :: Conj (Disj a) }
deriving (Show, Monoid)
newtype DNF a = DNF { unDNF :: Disj (Conj a) }
deriving (Show, Monoid)
instance Functor CNF where
fmap f (CNF x) = CNF (fmap (fmap f) x)
instance Boolean CNF where
l /\ r = l `mappend` r
l \/ r = CNF $ Conj [ x `mappend` y | x <- unConj $ unCNF l
, y <- unConj $ unCNF r ]
bNot = error "bNot on CNF"
bTrue = CNF $ Conj[]
bFalse = CNF $ Conj[Disj[]]
bConst x = CNF $ Conj[Disj[x]]
instance Functor DNF where
fmap f (DNF x) = DNF (fmap (fmap f) x)
instance Boolean DNF where
l /\ r = DNF $ Disj [ x `mappend` y | x <- unDisj $ unDNF l
, y <- unDisj $ unDNF r ]
l \/ r = l `mappend` r
bNot = error "bNot on CNF"
bTrue = DNF $ Disj[Conj[]]
bFalse = DNF $ Disj[]
bConst x = DNF $ Disj[Conj[x]]
reduceBoolExpr :: BoolExpr Bool -> Bool
reduceBoolExpr (BAnd a b) = reduceBoolExpr a && reduceBoolExpr b
reduceBoolExpr (BOr a b) = reduceBoolExpr a || reduceBoolExpr b
reduceBoolExpr (BNot a) = not $ reduceBoolExpr a
reduceBoolExpr BTrue = True
reduceBoolExpr BFalse = False
reduceBoolExpr (BConst c) = c
evalBoolExpr :: (a -> Bool) -> (BoolExpr a -> Bool)
evalBoolExpr f = reduceBoolExpr . fmap (f$)
constants :: BoolExpr a -> [Signed a]
constants = go True
where go sign (BAnd a b) = go sign a ++ go sign b
go sign (BOr a b) = go sign a ++ go sign b
go sign (BNot t) = go (not sign) t
go _ BTrue = []
go _ BFalse = []
go sign (BConst x) = [if sign then Positive x else Negative x]
dualize :: NegateConstant a -> BoolExpr a -> BoolExpr a
dualize neg (BAnd l r) = BOr (dualize neg l) (dualize neg r)
dualize neg (BOr l r) = BAnd (dualize neg l) (dualize neg r)
dualize _ BTrue = BFalse
dualize _ BFalse = BTrue
dualize neg (BConst c) = neg c
dualize _ (BNot _) = error "dualize: impossible"
type NegateConstant a = a -> BoolExpr a
pushNotInwards :: NegateConstant a -> BoolExpr a -> BoolExpr a
pushNotInwards neg (BAnd l r) = BAnd (pushNotInwards neg l) (pushNotInwards neg r)
pushNotInwards neg (BOr l r) = BOr (pushNotInwards neg l) (pushNotInwards neg r)
pushNotInwards neg (BNot t) = dualize neg $ pushNotInwards neg t
pushNotInwards _ BTrue = BTrue
pushNotInwards _ BFalse = BFalse
pushNotInwards _ b@(BConst _) = b
boolTreeToCNF :: NegateConstant a -> BoolExpr a -> CNF a
boolTreeToCNF neg = fromBoolExpr . pushNotInwards neg
reduceCNF :: CNF Bool -> Bool
reduceCNF = all (or . unDisj) . unConj . unCNF
boolTreeToDNF :: (a -> BoolExpr a) -> BoolExpr a -> DNF a
boolTreeToDNF neg = fromBoolExpr . pushNotInwards neg
reduceDNF :: DNF Bool -> Bool
reduceDNF = any (and . unConj) . unDisj . unDNF