{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.BoolExpr
-- Copyright   :  (c) Masahiro Sakai 2014-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Boolean expression over a given type of atoms
--
-----------------------------------------------------------------------------
module ToySolver.Data.BoolExpr
  (
  -- * BoolExpr type
    BoolExpr (..)

  -- * Operations
  , 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

-- | Boolean expression over a given type of atoms
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