{-# 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
(BoolExpr a -> BoolExpr a -> Bool)
-> (BoolExpr a -> BoolExpr a -> Bool) -> Eq (BoolExpr a)
forall a. Eq a => BoolExpr a -> BoolExpr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: BoolExpr a -> BoolExpr a -> Bool
Eq, Eq (BoolExpr a)
Eq (BoolExpr a) =>
(BoolExpr a -> BoolExpr a -> Ordering)
-> (BoolExpr a -> BoolExpr a -> Bool)
-> (BoolExpr a -> BoolExpr a -> Bool)
-> (BoolExpr a -> BoolExpr a -> Bool)
-> (BoolExpr a -> BoolExpr a -> Bool)
-> (BoolExpr a -> BoolExpr a -> BoolExpr a)
-> (BoolExpr a -> BoolExpr a -> BoolExpr a)
-> Ord (BoolExpr a)
BoolExpr a -> BoolExpr a -> Bool
BoolExpr a -> BoolExpr a -> Ordering
BoolExpr a -> BoolExpr a -> BoolExpr a
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
$ccompare :: forall a. Ord a => BoolExpr a -> BoolExpr a -> Ordering
compare :: BoolExpr a -> BoolExpr a -> Ordering
$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
>= :: BoolExpr a -> BoolExpr a -> Bool
$cmax :: forall a. Ord a => BoolExpr a -> BoolExpr a -> BoolExpr a
max :: BoolExpr a -> BoolExpr a -> BoolExpr a
$cmin :: forall a. Ord a => BoolExpr a -> BoolExpr a -> BoolExpr a
min :: BoolExpr a -> BoolExpr a -> BoolExpr a
Ord, Int -> BoolExpr a -> ShowS
[BoolExpr a] -> ShowS
BoolExpr a -> String
(Int -> BoolExpr a -> ShowS)
-> (BoolExpr a -> String)
-> ([BoolExpr a] -> ShowS)
-> Show (BoolExpr a)
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
$cshowsPrec :: forall a. Show a => Int -> BoolExpr a -> ShowS
showsPrec :: Int -> BoolExpr a -> ShowS
$cshow :: forall a. Show a => BoolExpr a -> String
show :: BoolExpr a -> String
$cshowList :: forall a. Show a => [BoolExpr a] -> ShowS
showList :: [BoolExpr a] -> ShowS
Show, ReadPrec [BoolExpr a]
ReadPrec (BoolExpr a)
Int -> ReadS (BoolExpr a)
ReadS [BoolExpr a]
(Int -> ReadS (BoolExpr a))
-> ReadS [BoolExpr a]
-> ReadPrec (BoolExpr a)
-> ReadPrec [BoolExpr a]
-> Read (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
$creadsPrec :: forall a. Read a => Int -> ReadS (BoolExpr a)
readsPrec :: Int -> ReadS (BoolExpr a)
$creadList :: forall a. Read a => ReadS [BoolExpr a]
readList :: ReadS [BoolExpr a]
$creadPrec :: forall a. Read a => ReadPrec (BoolExpr a)
readPrec :: ReadPrec (BoolExpr a)
$creadListPrec :: forall a. Read a => ReadPrec [BoolExpr a]
readListPrec :: ReadPrec [BoolExpr a]
Read, Typeable, Typeable (BoolExpr a)
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (BoolExpr a))
-> (BoolExpr a -> Constr)
-> (BoolExpr a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (BoolExpr a)))
-> ((forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r)
-> (forall u. (forall d. Data d => d -> u) -> BoolExpr a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a))
-> Data (BoolExpr a)
BoolExpr a -> Constr
BoolExpr a -> DataType
(forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
forall a. Data a => Typeable (BoolExpr a)
forall a. Data a => BoolExpr a -> Constr
forall a. Data a => BoolExpr a -> DataType
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 u. Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u
forall u. (forall d. Data d => d -> u) -> BoolExpr a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BoolExpr a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BoolExpr a)
$ctoConstr :: forall a. Data a => BoolExpr a -> Constr
toConstr :: BoolExpr a -> Constr
$cdataTypeOf :: forall a. Data a => BoolExpr a -> DataType
dataTypeOf :: BoolExpr a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BoolExpr a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BoolExpr a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
gmapT :: (forall b. Data b => b -> b) -> BoolExpr a -> BoolExpr a
$cgmapQl :: 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
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BoolExpr a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BoolExpr a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BoolExpr a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BoolExpr a -> m (BoolExpr a)
Data)

instance Functor BoolExpr where
  fmap :: forall a b. (a -> b) -> BoolExpr a -> BoolExpr b
fmap = (a -> b) -> BoolExpr a -> BoolExpr b
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmapDefault

instance Applicative BoolExpr where
  pure :: forall a. a -> BoolExpr a
pure = a -> BoolExpr a
forall a. a -> BoolExpr a
Atom
  <*> :: forall a b. BoolExpr (a -> b) -> BoolExpr a -> BoolExpr 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 = a -> BoolExpr a
forall a. a -> BoolExpr a
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 = (a -> BoolExpr b) -> BoolExpr a -> BoolExpr b
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 = (a -> m) -> BoolExpr a -> m
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) = b -> BoolExpr b
forall a. a -> BoolExpr a
Atom (b -> BoolExpr b) -> f b -> f (BoolExpr b)
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) = [BoolExpr b] -> BoolExpr b
forall a. [BoolExpr a] -> BoolExpr a
And ([BoolExpr b] -> BoolExpr b) -> f [BoolExpr b] -> f (BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f (BoolExpr b)] -> f [BoolExpr b]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ((BoolExpr a -> f (BoolExpr b)) -> [BoolExpr a] -> [f (BoolExpr b)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f) [BoolExpr a]
xs)
  traverse a -> f b
f (Or [BoolExpr a]
xs) = [BoolExpr b] -> BoolExpr b
forall a. [BoolExpr a] -> BoolExpr a
Or ([BoolExpr b] -> BoolExpr b) -> f [BoolExpr b] -> f (BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f (BoolExpr b)] -> f [BoolExpr b]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ((BoolExpr a -> f (BoolExpr b)) -> [BoolExpr a] -> [f (BoolExpr b)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f) [BoolExpr a]
xs)
  traverse a -> f b
f (Not BoolExpr a
x) = BoolExpr b -> BoolExpr b
forall a. BoolExpr a -> BoolExpr a
Not (BoolExpr b -> BoolExpr b) -> f (BoolExpr b) -> f (BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
x
  traverse a -> f b
f (Imply BoolExpr a
x BoolExpr a
y) = BoolExpr b -> BoolExpr b -> BoolExpr b
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply (BoolExpr b -> BoolExpr b -> BoolExpr b)
-> f (BoolExpr b) -> f (BoolExpr b -> BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
x f (BoolExpr b -> BoolExpr b) -> f (BoolExpr b) -> f (BoolExpr b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
y
  traverse a -> f b
f (Equiv BoolExpr a
x BoolExpr a
y) = BoolExpr b -> BoolExpr b -> BoolExpr b
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Equiv (BoolExpr b -> BoolExpr b -> BoolExpr b)
-> f (BoolExpr b) -> f (BoolExpr b -> BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
x f (BoolExpr b -> BoolExpr b) -> f (BoolExpr b) -> f (BoolExpr b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
y
  traverse a -> f b
f (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = BoolExpr b -> BoolExpr b -> BoolExpr b -> BoolExpr b
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ITE (BoolExpr b -> BoolExpr b -> BoolExpr b -> BoolExpr b)
-> f (BoolExpr b) -> f (BoolExpr b -> BoolExpr b -> BoolExpr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
c f (BoolExpr b -> BoolExpr b -> BoolExpr b)
-> f (BoolExpr b) -> f (BoolExpr b -> BoolExpr b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
t f (BoolExpr b -> BoolExpr b) -> f (BoolExpr b) -> f (BoolExpr b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> BoolExpr a -> f (BoolExpr b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f BoolExpr a
e

instance NFData a => NFData (BoolExpr a) where
  rnf :: BoolExpr a -> ()
rnf (Atom a
a) = a -> ()
forall a. NFData a => a -> ()
rnf a
a
  rnf (And [BoolExpr a]
xs) = [BoolExpr a] -> ()
forall a. NFData a => a -> ()
rnf [BoolExpr a]
xs
  rnf (Or [BoolExpr a]
xs) = [BoolExpr a] -> ()
forall a. NFData a => a -> ()
rnf [BoolExpr a]
xs
  rnf (Not BoolExpr a
x) = BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
x
  rnf (Imply BoolExpr a
x BoolExpr a
y) = BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
x () -> () -> ()
forall a b. a -> b -> b
`seq` BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
y
  rnf (Equiv BoolExpr a
x BoolExpr a
y) = BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
x () -> () -> ()
forall a b. a -> b -> b
`seq` BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
y
  rnf (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
c () -> () -> ()
forall a b. a -> b -> b
`seq` BoolExpr a -> ()
forall a. NFData a => a -> ()
rnf BoolExpr a
t () -> () -> ()
forall a b. a -> b -> b
`seq` BoolExpr a -> ()
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0::Int) Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
a
  hashWithSalt Int
s (And [BoolExpr a]
xs) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1::Int) Int -> [BoolExpr a] -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` [BoolExpr a]
xs
  hashWithSalt Int
s (Or [BoolExpr a]
xs)  = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2::Int) Int -> [BoolExpr a] -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` [BoolExpr a]
xs
  hashWithSalt Int
s (Not BoolExpr a
x)  = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3::Int) Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x
  hashWithSalt Int
s (Imply BoolExpr a
x BoolExpr a
y) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
4::Int) Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
y
  hashWithSalt Int
s (Equiv BoolExpr a
x BoolExpr a
y) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
5::Int) Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
x Int -> BoolExpr a -> Int
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 Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
6::Int) Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
c Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
t Int -> BoolExpr a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BoolExpr a
e

instance Complement (BoolExpr a) where
  notB :: BoolExpr a -> BoolExpr a
notB = BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a
Not

instance MonotoneBoolean (BoolExpr a) where
  andB :: [BoolExpr a] -> BoolExpr a
andB = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
And
  orB :: [BoolExpr a] -> BoolExpr a
orB  = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
Or

instance IfThenElse (BoolExpr a) (BoolExpr a) where
  ite :: BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ite = BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
ITE

instance Boolean (BoolExpr a) where
  .=>. :: BoolExpr a -> BoolExpr a -> BoolExpr a
(.=>.) = BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply
  .<=>. :: BoolExpr a -> BoolExpr a -> BoolExpr a
(.<=>.) = 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 = (a -> VarSet) -> BoolExpr a -> VarSet
forall m a. Monoid m => (a -> m) -> BoolExpr a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> VarSet
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) = [b] -> b
forall a. MonotoneBoolean a => [a] -> a
orB ((BoolExpr atom -> b) -> [BoolExpr atom] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map BoolExpr atom -> b
g [BoolExpr atom]
xs)
    g (And [BoolExpr atom]
xs) = [b] -> b
forall a. MonotoneBoolean a => [a] -> a
andB ((BoolExpr atom -> b) -> [BoolExpr atom] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map BoolExpr atom -> b
g [BoolExpr atom]
xs)
    g (Not BoolExpr atom
x) = b -> b
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 b -> b -> b
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 b -> b -> b
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) = b -> b -> b -> b
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 = (a -> Bool) -> BoolExpr a -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold (m -> a -> Bool
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 = Simplify a -> BoolExpr a
forall a. Simplify a -> BoolExpr a
runSimplify (Simplify a -> BoolExpr a)
-> (BoolExpr a -> Simplify a) -> BoolExpr a -> BoolExpr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Simplify a) -> BoolExpr a -> Simplify a
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold (BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a -> Simplify a) -> (a -> BoolExpr a) -> a -> Simplify a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> BoolExpr a
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)) = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
x
  notB (Simplify BoolExpr a
x) = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
x)

instance MonotoneBoolean (Simplify a) where
  orB :: [Simplify a] -> Simplify a
orB [Simplify a]
xs
    | (BoolExpr a -> Bool) -> [BoolExpr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isTrue [BoolExpr a]
ys = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
forall a. MonotoneBoolean a => a
true
    | Bool
otherwise = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a -> Simplify a) -> BoolExpr a -> Simplify a
forall a b. (a -> b) -> a -> b
$ [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
Or [BoolExpr a]
ys
    where
      ys :: [BoolExpr a]
ys = [[BoolExpr a]] -> [BoolExpr a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [BoolExpr a -> [BoolExpr a]
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
    | (BoolExpr a -> Bool) -> [BoolExpr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isFalse [BoolExpr a]
ys = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
forall a. MonotoneBoolean a => a
false
    | Bool
otherwise = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a -> Simplify a) -> BoolExpr a -> Simplify a
forall a b. (a -> b) -> a -> b
$ [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
And [BoolExpr a]
ys
    where
      ys :: [BoolExpr a]
ys = [[BoolExpr a]] -> [BoolExpr a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [BoolExpr a -> [BoolExpr a]
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)
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isTrue BoolExpr a
c  = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
t
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isFalse BoolExpr a
c = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
e
    | Bool
otherwise = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a
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
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isFalse BoolExpr a
x = Simplify a
forall a. MonotoneBoolean a => a
true
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isTrue BoolExpr a
y  = Simplify a
forall a. MonotoneBoolean a => a
true
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isTrue BoolExpr a
x  = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
y
    | BoolExpr a -> Bool
forall a. BoolExpr a -> Bool
isFalse BoolExpr a
y = Simplify a -> Simplify a
forall a. Complement a => a -> a
notB (BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify BoolExpr a
x)
    | Bool
otherwise = BoolExpr a -> Simplify a
forall a. BoolExpr a -> Simplify a
Simplify (BoolExpr a
x BoolExpr a -> BoolExpr a -> BoolExpr a
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