{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.Data.BoolExpr
(
BoolExpr (..)
, fold
, simplify
) where
import Control.DeepSeq
import Control.Monad
import Data.Data
import Data.Hashable
import Data.Traversable
import ToySolver.Data.Boolean
import ToySolver.Data.IntVar
data BoolExpr a
= Atom a
| And [BoolExpr a]
| Or [BoolExpr a]
| Not (BoolExpr a)
| Imply (BoolExpr a) (BoolExpr a)
| Equiv (BoolExpr a) (BoolExpr a)
| ITE (BoolExpr a) (BoolExpr a) (BoolExpr a)
deriving (BoolExpr a -> BoolExpr a -> Bool
forall a. Eq a => BoolExpr a -> BoolExpr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BoolExpr a -> BoolExpr a -> Bool
$c/= :: forall a. Eq a => BoolExpr a -> BoolExpr a -> Bool
== :: BoolExpr a -> BoolExpr a -> Bool
$c== :: forall a. Eq a => BoolExpr a -> BoolExpr a -> Bool
Eq, BoolExpr a -> BoolExpr a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (BoolExpr a)
forall a. Ord a => BoolExpr a -> BoolExpr a -> Bool
forall a. Ord a => BoolExpr a -> BoolExpr a -> Ordering
forall a. Ord a => BoolExpr a -> BoolExpr a -> BoolExpr a
min :: BoolExpr a -> BoolExpr a -> BoolExpr a
$cmin :: forall a. Ord a => BoolExpr a -> BoolExpr a -> BoolExpr a
max :: BoolExpr a -> BoolExpr a -> BoolExpr a
$cmax :: forall a. Ord a => BoolExpr a -> BoolExpr a -> BoolExpr a
>= :: BoolExpr a -> BoolExpr a -> Bool
$c>= :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Bool
> :: BoolExpr a -> BoolExpr a -> Bool
$c> :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Bool
<= :: BoolExpr a -> BoolExpr a -> Bool
$c<= :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Bool
< :: BoolExpr a -> BoolExpr a -> Bool
$c< :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Bool
compare :: BoolExpr a -> BoolExpr a -> Ordering
$ccompare :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Ordering
Ord, Int -> BoolExpr a -> ShowS
forall a. Show a => Int -> BoolExpr a -> ShowS
forall a. Show a => [BoolExpr a] -> ShowS
forall a. Show a => BoolExpr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BoolExpr a] -> ShowS
$cshowList :: forall a. Show a => [BoolExpr a] -> ShowS
show :: BoolExpr a -> String
$cshow :: forall a. Show a => BoolExpr a -> String
showsPrec :: Int -> BoolExpr a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> BoolExpr a -> ShowS
Show, ReadPrec [BoolExpr a]
ReadPrec (BoolExpr a)
ReadS [BoolExpr a]
forall a. Read a => ReadPrec [BoolExpr a]
forall a. Read a => ReadPrec (BoolExpr a)
forall a. Read a => Int -> ReadS (BoolExpr a)
forall a. Read a => ReadS [BoolExpr a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [BoolExpr a]
$creadListPrec :: forall a. Read a => ReadPrec [BoolExpr a]
readPrec :: ReadPrec (BoolExpr a)
$creadPrec :: forall a. Read a => ReadPrec (BoolExpr a)
readList :: ReadS [BoolExpr a]
$creadList :: forall a. Read a => ReadS [BoolExpr a]
readsPrec :: Int -> ReadS (BoolExpr a)
$creadsPrec :: forall a. Read a => Int -> ReadS (BoolExpr a)
Read, Typeable, BoolExpr a -> DataType
BoolExpr a -> Constr
forall {a}. Data a => Typeable (BoolExpr a)
forall a. Data a => BoolExpr a -> DataType
forall a. Data a => BoolExpr a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> BoolExpr a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BoolExpr a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BoolExpr a -> c (BoolExpr a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BoolExpr a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BoolExpr a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BoolExpr a -> c (BoolExpr a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BoolExpr a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BoolExpr a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
gmapT :: (forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BoolExpr a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BoolExpr a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a))
dataTypeOf :: BoolExpr a -> DataType
$cdataTypeOf :: forall a. Data a => BoolExpr a -> DataType
toConstr :: BoolExpr a -> Constr
$ctoConstr :: forall a. Data a => BoolExpr a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BoolExpr a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BoolExpr a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BoolExpr a -> c (BoolExpr a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BoolExpr a -> c (BoolExpr a)
Data)
instance Functor BoolExpr where
fmap :: forall a b. (a -> b) -> BoolExpr a -> BoolExpr b
fmap = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmapDefault
instance Applicative BoolExpr where
pure :: forall a. a -> BoolExpr a
pure = forall a. a -> BoolExpr a
Atom
<*> :: forall a b. BoolExpr (a -> b) -> BoolExpr a -> BoolExpr b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad BoolExpr where
return :: forall a. a -> BoolExpr a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
BoolExpr a
m >>= :: forall a b. BoolExpr a -> (a -> BoolExpr b) -> BoolExpr b
>>= a -> BoolExpr b
f = forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold a -> BoolExpr b
f BoolExpr a
m
instance Foldable BoolExpr where
foldMap :: forall m a. Monoid m => (a -> m) -> BoolExpr a -> m
foldMap = forall (t :: * -> *) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault
instance Traversable BoolExpr where
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f (Atom a
x) = forall a. a -> BoolExpr a
Atom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
traverse a -> f b
f (And [BoolExpr a]
xs) = forall a. [BoolExpr a] -> BoolExpr a
And forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) [BoolExpr a]
xs)
traverse a -> f b
f (Or [BoolExpr a]
xs) = forall a. [BoolExpr a] -> BoolExpr a
Or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) [BoolExpr a]
xs)
traverse a -> f b
f (Not BoolExpr a
x) = forall a. BoolExpr a -> BoolExpr a
Not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
x
traverse a -> f b
f (Imply BoolExpr a
x BoolExpr a
y) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
y
traverse a -> f b
f (Equiv BoolExpr a
x BoolExpr a
y) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Equiv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
y
traverse a -> f b
f (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ITE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f BoolExpr a
e
instance NFData a => NFData (BoolExpr a) where
rnf :: BoolExpr a -> ()
rnf (Atom a
a) = forall a. NFData a => a -> ()
rnf a
a
rnf (And [BoolExpr a]
xs) = forall a. NFData a => a -> ()
rnf [BoolExpr a]
xs
rnf (Or [BoolExpr a]
xs) = forall a. NFData a => a -> ()
rnf [BoolExpr a]
xs
rnf (Not BoolExpr a
x) = forall a. NFData a => a -> ()
rnf BoolExpr a
x
rnf (Imply BoolExpr a
x BoolExpr a
y) = forall a. NFData a => a -> ()
rnf BoolExpr a
x seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf BoolExpr a
y
rnf (Equiv BoolExpr a
x BoolExpr a
y) = forall a. NFData a => a -> ()
rnf BoolExpr a
x seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf BoolExpr a
y
rnf (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = forall a. NFData a => a -> ()
rnf BoolExpr a
c seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf BoolExpr a
t seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf BoolExpr a
e
instance Hashable a => Hashable (BoolExpr a) where
hashWithSalt :: Int -> BoolExpr a -> Int
hashWithSalt Int
s (Atom a
a) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
a
hashWithSalt Int
s (And [BoolExpr a]
xs) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` [BoolExpr a]
xs
hashWithSalt Int
s (Or [BoolExpr a]
xs) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` [BoolExpr a]
xs
hashWithSalt Int
s (Not BoolExpr a
x) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x
hashWithSalt Int
s (Imply BoolExpr a
x BoolExpr a
y) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
y
hashWithSalt Int
s (Equiv BoolExpr a
x BoolExpr a
y) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
y
hashWithSalt Int
s (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6::Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
c forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
t forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
e
instance Complement (BoolExpr a) where
notB :: BoolExpr a -> BoolExpr a
notB = forall a. BoolExpr a -> BoolExpr a
Not
instance MonotoneBoolean (BoolExpr a) where
andB :: [BoolExpr a] -> BoolExpr a
andB = forall a. [BoolExpr a] -> BoolExpr a
And
orB :: [BoolExpr a] -> BoolExpr a
orB = forall a. [BoolExpr a] -> BoolExpr a
Or
instance IfThenElse (BoolExpr a) (BoolExpr a) where
ite :: BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ite = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ITE
instance Boolean (BoolExpr a) where
.=>. :: BoolExpr a -> BoolExpr a -> BoolExpr a
(.=>.) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply
.<=>. :: BoolExpr a -> BoolExpr a -> BoolExpr a
(.<=>.) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Equiv
instance Variables a => Variables (BoolExpr a) where
vars :: BoolExpr a -> VarSet
vars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. Variables a => a -> VarSet
vars
fold :: Boolean b => (atom -> b) -> BoolExpr atom -> b
fold :: forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold atom -> b
f = BoolExpr atom -> b
g
where
g :: BoolExpr atom -> b
g (Atom atom
a) = atom -> b
f atom
a
g (Or [BoolExpr atom]
xs) = forall a. MonotoneBoolean a => [a] -> a
orB (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr atom -> b
g [BoolExpr atom]
xs)
g (And [BoolExpr atom]
xs) = forall a. MonotoneBoolean a => [a] -> a
andB (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr atom -> b
g [BoolExpr atom]
xs)
g (Not BoolExpr atom
x) = forall a. Complement a => a -> a
notB (BoolExpr atom -> b
g BoolExpr atom
x)
g (Imply BoolExpr atom
x BoolExpr atom
y) = BoolExpr atom -> b
g BoolExpr atom
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr atom -> b
g BoolExpr atom
y
g (Equiv BoolExpr atom
x BoolExpr atom
y) = BoolExpr atom -> b
g BoolExpr atom
x forall a. Boolean a => a -> a -> a
.<=>. BoolExpr atom -> b
g BoolExpr atom
y
g (ITE BoolExpr atom
c BoolExpr atom
t BoolExpr atom
e) = forall b a. IfThenElse b a => b -> a -> a -> a
ite (BoolExpr atom -> b
g BoolExpr atom
c) (BoolExpr atom -> b
g BoolExpr atom
t) (BoolExpr atom -> b
g BoolExpr atom
e)
{-# RULES
"fold/fmap" forall f g e. fold f (fmap g e) = fold (f.g) e
#-}
instance Eval m a Bool => Eval m (BoolExpr a) Bool where
eval :: m -> BoolExpr a -> Bool
eval m
m = forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold (forall m e v. Eval m e v => m -> e -> v
eval m
m)
simplify :: BoolExpr a -> BoolExpr a
simplify :: forall a. BoolExpr a -> BoolExpr a
simplify = forall a. Simplify a -> BoolExpr a
runSimplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold (forall a. BoolExpr a -> Simplify a
Simplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> BoolExpr a
Atom)
newtype Simplify a = Simplify{ forall a. Simplify a -> BoolExpr a
runSimplify :: BoolExpr a }
instance Complement (Simplify a) where
notB :: Simplify a -> Simplify a
notB (Simplify (Not BoolExpr a
x)) = forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
x
notB (Simplify BoolExpr a
x) = forall a. BoolExpr a -> Simplify a
Simplify (forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
x)
instance MonotoneBoolean (Simplify a) where
orB :: [Simplify a] -> Simplify a
orB [Simplify a]
xs
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. BoolExpr a -> Bool
isTrue [BoolExpr a]
ys = forall a. BoolExpr a -> Simplify a
Simplify forall a. MonotoneBoolean a => a
true
| Bool
otherwise = forall a. BoolExpr a -> Simplify a
Simplify forall a b. (a -> b) -> a -> b
$ forall a. [BoolExpr a] -> BoolExpr a
Or [BoolExpr a]
ys
where
ys :: [BoolExpr a]
ys = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall {a}. BoolExpr a -> [BoolExpr a]
f BoolExpr a
x | Simplify BoolExpr a
x <- [Simplify a]
xs]
f :: BoolExpr a -> [BoolExpr a]
f (Or [BoolExpr a]
zs) = [BoolExpr a]
zs
f BoolExpr a
z = [BoolExpr a
z]
andB :: [Simplify a] -> Simplify a
andB [Simplify a]
xs
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. BoolExpr a -> Bool
isFalse [BoolExpr a]
ys = forall a. BoolExpr a -> Simplify a
Simplify forall a. MonotoneBoolean a => a
false
| Bool
otherwise = forall a. BoolExpr a -> Simplify a
Simplify forall a b. (a -> b) -> a -> b
$ forall a. [BoolExpr a] -> BoolExpr a
And [BoolExpr a]
ys
where
ys :: [BoolExpr a]
ys = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall {a}. BoolExpr a -> [BoolExpr a]
f BoolExpr a
x | Simplify BoolExpr a
x <- [Simplify a]
xs]
f :: BoolExpr a -> [BoolExpr a]
f (And [BoolExpr a]
zs) = [BoolExpr a]
zs
f BoolExpr a
z = [BoolExpr a
z]
instance IfThenElse (Simplify a) (Simplify a) where
ite :: Simplify a -> Simplify a -> Simplify a -> Simplify a
ite (Simplify BoolExpr a
c) (Simplify BoolExpr a
t) (Simplify BoolExpr a
e)
| forall a. BoolExpr a -> Bool
isTrue BoolExpr a
c = forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
t
| forall a. BoolExpr a -> Bool
isFalse BoolExpr a
c = forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
e
| Bool
otherwise = forall a. BoolExpr a -> Simplify a
Simplify (forall a. BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e)
instance Boolean (Simplify a) where
Simplify BoolExpr a
x .=>. :: Simplify a -> Simplify a -> Simplify a
.=>. Simplify BoolExpr a
y
| forall a. BoolExpr a -> Bool
isFalse BoolExpr a
x = forall a. MonotoneBoolean a => a
true
| forall a. BoolExpr a -> Bool
isTrue BoolExpr a
y = forall a. MonotoneBoolean a => a
true
| forall a. BoolExpr a -> Bool
isTrue BoolExpr a
x = forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
y
| forall a. BoolExpr a -> Bool
isFalse BoolExpr a
y = forall a. Complement a => a -> a
notB (forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
x)
| Bool
otherwise = forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
y)
isTrue :: BoolExpr a -> Bool
isTrue :: forall a. BoolExpr a -> Bool
isTrue (And []) = Bool
True
isTrue BoolExpr a
_ = Bool
False
isFalse :: BoolExpr a -> Bool
isFalse :: forall a. BoolExpr a -> Bool
isFalse (Or []) = Bool
True
isFalse BoolExpr a
_ = Bool
False