{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}
--------------------------------------------------------------------
-- |
-- Module    : Data.BoolExpr
-- Copyright : (c) Nicolas Pouillard 2008,2009
-- License   : BSD3
--
-- Maintainer: Nicolas Pouillard <nicolas.pouillard@gmail.com>
-- Stability : provisional
-- Portability:
--
-- Boolean expressions and various representations.
--------------------------------------------------------------------

module Data.BoolExpr
  (-- * A boolean class
   Boolean(..)
   -- * Generic functions derived from Boolean
  ,bAnd
  ,bAll
  ,bOr
  ,bAny
   -- * Boolean trees
  ,BoolExpr(..)
  ,reduceBoolExpr
  ,evalBoolExpr
   -- * Boolean evaluation semantic
  ,Eval(..)
  ,runEvalId
   -- * Signed constants
  ,Signed(..)
  ,negateSigned
  ,evalSigned
  ,reduceSigned
  ,constants
  ,negateConstant
   -- * Conjunctive Normal Form
  ,CNF(..),Conj(..)
  ,fromCNF
  ,boolTreeToCNF
  ,reduceCNF
   -- * Disjunctive Normal Form
  ,Disj(..),DNF(..)
  ,fromDNF
  ,boolTreeToDNF
  ,reduceDNF
   -- * Other transformations
  ,dualize
  ,fromBoolExpr
  ,pushNotInwards
  )
  where

-- import Test.QuickCheck hiding (Positive)
-- import Control.Applicative
import Control.Monad (ap)
import Data.Traversable


-- | Signed values are either positive or negative.
data Signed a = Positive a | Negative a
  deriving (Signed a -> Signed a -> Bool
forall a. Eq a => Signed a -> Signed a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Signed a -> Signed a -> Bool
$c/= :: forall a. Eq a => Signed a -> Signed a -> Bool
== :: Signed a -> Signed a -> Bool
$c== :: forall a. Eq a => Signed a -> Signed a -> Bool
Eq, Signed a -> Signed a -> Bool
Signed a -> Signed 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 (Signed a)
forall a. Ord a => Signed a -> Signed a -> Bool
forall a. Ord a => Signed a -> Signed a -> Ordering
forall a. Ord a => Signed a -> Signed a -> Signed a
min :: Signed a -> Signed a -> Signed a
$cmin :: forall a. Ord a => Signed a -> Signed a -> Signed a
max :: Signed a -> Signed a -> Signed a
$cmax :: forall a. Ord a => Signed a -> Signed a -> Signed a
>= :: Signed a -> Signed a -> Bool
$c>= :: forall a. Ord a => Signed a -> Signed a -> Bool
> :: Signed a -> Signed a -> Bool
$c> :: forall a. Ord a => Signed a -> Signed a -> Bool
<= :: Signed a -> Signed a -> Bool
$c<= :: forall a. Ord a => Signed a -> Signed a -> Bool
< :: Signed a -> Signed a -> Bool
$c< :: forall a. Ord a => Signed a -> Signed a -> Bool
compare :: Signed a -> Signed a -> Ordering
$ccompare :: forall a. Ord a => Signed a -> Signed a -> Ordering
Ord, Int -> Signed a -> ShowS
forall a. Show a => Int -> Signed a -> ShowS
forall a. Show a => [Signed a] -> ShowS
forall a. Show a => Signed a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Signed a] -> ShowS
$cshowList :: forall a. Show a => [Signed a] -> ShowS
show :: Signed a -> String
$cshow :: forall a. Show a => Signed a -> String
showsPrec :: Int -> Signed a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Signed a -> ShowS
Show, ReadPrec [Signed a]
ReadPrec (Signed a)
ReadS [Signed a]
forall a. Read a => ReadPrec [Signed a]
forall a. Read a => ReadPrec (Signed a)
forall a. Read a => Int -> ReadS (Signed a)
forall a. Read a => ReadS [Signed a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Signed a]
$creadListPrec :: forall a. Read a => ReadPrec [Signed a]
readPrec :: ReadPrec (Signed a)
$creadPrec :: forall a. Read a => ReadPrec (Signed a)
readList :: ReadS [Signed a]
$creadList :: forall a. Read a => ReadS [Signed a]
readsPrec :: Int -> ReadS (Signed a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Signed a)
Read)

instance Functor Signed where
  fmap :: forall a b. (a -> b) -> Signed a -> Signed b
fmap a -> b
f (Positive a
x) = forall a. a -> Signed a
Positive (a -> b
f a
x)
  fmap a -> b
f (Negative a
x) = forall a. a -> Signed a
Negative (a -> b
f a
x)

instance Traversable Signed where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Signed a -> f (Signed b)
traverse a -> f b
f (Positive a
x) = forall a. a -> Signed a
Positive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
  traverse a -> f b
f (Negative a
x) = forall a. a -> Signed a
Negative forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x

instance Foldable Signed where
  foldMap :: forall m a. Monoid m => (a -> m) -> Signed a -> m
foldMap = forall (t :: * -> *) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault

instance Applicative Signed where
  pure :: forall a. a -> Signed a
pure  = forall a. a -> Signed a
Positive
  <*> :: forall a b. Signed (a -> b) -> Signed a -> Signed b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Signed where
  Positive a
x >>= :: forall a b. Signed a -> (a -> Signed b) -> Signed b
>>= a -> Signed b
f = a -> Signed b
f a
x
  Negative a
x >>= a -> Signed b
f = forall a. Signed a -> Signed a
negateSigned forall a b. (a -> b) -> a -> b
$ a -> Signed b
f a
x

infix /\
infix \/

-- | A boolean type class.
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 :: Signed a -> f a

-- | Generalized 'Data.Foldable.and'.
bAnd :: (Foldable t, Boolean f) => t (f b) -> f b
bAnd :: forall (t :: * -> *) (f :: * -> *) b.
(Foldable t, Boolean f) =>
t (f b) -> f b
bAnd = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
(/\) forall (f :: * -> *) a. Boolean f => f a
bTrue

-- | Generalized 'Data.Foldable.all'.
bAll :: (Foldable t, Boolean f) => (a -> f b) -> t a -> f b
bAll :: forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAll a -> f b
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x f b
y -> a -> f b
f a
x forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
/\ f b
y) forall (f :: * -> *) a. Boolean f => f a
bTrue

-- | Generalized 'Data.Foldable.or'.
bOr :: (Foldable t, Boolean f) => t (f b) -> f b
bOr :: forall (t :: * -> *) (f :: * -> *) b.
(Foldable t, Boolean f) =>
t (f b) -> f b
bOr = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
(\/) forall (f :: * -> *) a. Boolean f => f a
bFalse

-- | Generalized 'Data.Foldable.any'.
bAny :: (Foldable t, Boolean f) => (a -> f b) -> t a -> f b
bAny :: forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAny a -> f b
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x f b
y -> a -> f b
f a
x forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
\/ f b
y) forall (f :: * -> *) a. Boolean f => f a
bFalse

-- | Syntax of boolean expressions parameterized over a
-- set of leaves, named constants.
data BoolExpr a = BAnd (BoolExpr a) (BoolExpr a)
                | BOr  (BoolExpr a) (BoolExpr a)
                | BNot (BoolExpr a)
                | BTrue
                | BFalse
                | BConst (Signed 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) {-! derive : Arbitrary !-}

instance Functor BoolExpr where
  fmap :: forall a b. (a -> b) -> BoolExpr a -> BoolExpr b
fmap a -> b
f (BAnd BoolExpr a
a BoolExpr a
b) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoolExpr a
a) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoolExpr a
b)
  fmap a -> b
f (BOr  BoolExpr a
a BoolExpr a
b) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BOr  (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoolExpr a
a) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoolExpr a
b)
  fmap a -> b
f (BNot BoolExpr a
t  ) = forall a. BoolExpr a -> BoolExpr a
BNot (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoolExpr a
t)
  fmap a -> b
_  BoolExpr a
BTrue     = forall a. BoolExpr a
BTrue
  fmap a -> b
_  BoolExpr a
BFalse    = forall a. BoolExpr a
BFalse
  fmap a -> b
f (BConst Signed a
x) = forall a. Signed a -> BoolExpr a
BConst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Signed a
x)

instance Traversable BoolExpr where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BoolExpr a -> f (BoolExpr b)
traverse a -> f b
f (BAnd BoolExpr a
a BoolExpr a
b) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd 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
a 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
b
  traverse a -> f b
f (BOr  BoolExpr a
a BoolExpr a
b) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BOr  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
a 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
b
  traverse a -> f b
f (BNot BoolExpr a
t  ) = forall a. BoolExpr a -> BoolExpr a
BNot 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
t
  traverse a -> f b
_  BoolExpr a
BTrue     = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. BoolExpr a
BTrue
  traverse a -> f b
_  BoolExpr a
BFalse    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. BoolExpr a
BFalse
  traverse a -> f b
f (BConst Signed a
x) = forall a. Signed a -> BoolExpr a
BConst 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 Signed a
x

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 Boolean BoolExpr where
  ( /\ ) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd
  ( \/ ) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BOr
  bNot :: forall a. BoolExpr a -> BoolExpr a
bNot   = forall a. BoolExpr a -> BoolExpr a
BNot
  bTrue :: forall a. BoolExpr a
bTrue  = forall a. BoolExpr a
BTrue
  bFalse :: forall a. BoolExpr a
bFalse = forall a. BoolExpr a
BFalse
  bConst :: forall a. Signed a -> BoolExpr a
bConst = forall a. Signed a -> BoolExpr a
BConst

newtype Eval b a = Eval { forall b a. Eval b a -> (a -> b) -> b
runEval :: (a -> b) -> b }

runEvalId :: Eval a a -> a
runEvalId :: forall a. Eval a a -> a
runEvalId Eval a a
e = forall b a. Eval b a -> (a -> b) -> b
runEval Eval a a
e forall a. a -> a
id

instance b ~ Bool => Boolean (Eval b) where
  ( /\ ) = forall b a. (b -> b -> b) -> Eval b a -> Eval b a -> Eval b a
liftE2 Bool -> Bool -> Bool
(&&)
  ( \/ ) = forall b a. (b -> b -> b) -> Eval b a -> Eval b a -> Eval b a
liftE2 Bool -> Bool -> Bool
(||)
  bNot :: forall a. Eval b a -> Eval b a
bNot   = forall b a. (b -> b) -> Eval b a -> Eval b a
liftE  Bool -> Bool
not
  bTrue :: forall a. Eval b a
bTrue  = forall b a. ((a -> b) -> b) -> Eval b a
Eval forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True
  bFalse :: forall a. Eval b a
bFalse = forall b a. ((a -> b) -> b) -> Eval b a
Eval forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
False
  bConst :: forall a. Signed a -> Eval b a
bConst = forall b a. ((a -> b) -> b) -> Eval b a
Eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> Signed a -> Bool
evalSigned

liftE :: (b -> b) -> Eval b a -> Eval b a
liftE :: forall b a. (b -> b) -> Eval b a -> Eval b a
liftE b -> b
f (Eval (a -> b) -> b
x) = forall b a. ((a -> b) -> b) -> Eval b a
Eval (b -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> b
x)

liftE2 :: (b -> b -> b) -> Eval b a -> Eval b a -> Eval b a
liftE2 :: forall b a. (b -> b -> b) -> Eval b a -> Eval b a -> Eval b a
liftE2 b -> b -> b
f (Eval (a -> b) -> b
x) (Eval (a -> b) -> b
y) = forall b a. ((a -> b) -> b) -> Eval b a
Eval (\a -> b
e -> b -> b -> b
f ((a -> b) -> b
x a -> b
e) ((a -> b) -> b
y a -> b
e))


-- | Turns a boolean tree into any boolean type.
fromBoolExpr :: Boolean f => BoolExpr a -> f a
fromBoolExpr :: forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr (BAnd BoolExpr a
l BoolExpr a
r) = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
/\ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
r
fromBoolExpr (BOr  BoolExpr a
l BoolExpr a
r) = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
\/ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
r
fromBoolExpr (BNot BoolExpr a
t  ) = forall (f :: * -> *) a. Boolean f => f a -> f a
bNot forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
t
fromBoolExpr  BoolExpr a
BTrue     = forall (f :: * -> *) a. Boolean f => f a
bTrue
fromBoolExpr  BoolExpr a
BFalse    = forall (f :: * -> *) a. Boolean f => f a
bFalse
fromBoolExpr (BConst Signed a
c) = forall (f :: * -> *) a. Boolean f => Signed a -> f a
bConst Signed a
c

--- | Disjunction of atoms ('a')
newtype Disj a = Disj { forall a. Disj a -> [a]
unDisj :: [a] }
  deriving (Int -> Disj a -> ShowS
forall a. Show a => Int -> Disj a -> ShowS
forall a. Show a => [Disj a] -> ShowS
forall a. Show a => Disj a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Disj a] -> ShowS
$cshowList :: forall a. Show a => [Disj a] -> ShowS
show :: Disj a -> String
$cshow :: forall a. Show a => Disj a -> String
showsPrec :: Int -> Disj a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Disj a -> ShowS
Show, forall a b. a -> Disj b -> Disj a
forall a b. (a -> b) -> Disj a -> Disj b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Disj b -> Disj a
$c<$ :: forall a b. a -> Disj b -> Disj a
fmap :: forall a b. (a -> b) -> Disj a -> Disj b
$cfmap :: forall a b. (a -> b) -> Disj a -> Disj b
Functor, NonEmpty (Disj a) -> Disj a
Disj a -> Disj a -> Disj a
forall b. Integral b => b -> Disj a -> Disj a
forall a. NonEmpty (Disj a) -> Disj a
forall a. Disj a -> Disj a -> Disj a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> Disj a -> Disj a
stimes :: forall b. Integral b => b -> Disj a -> Disj a
$cstimes :: forall a b. Integral b => b -> Disj a -> Disj a
sconcat :: NonEmpty (Disj a) -> Disj a
$csconcat :: forall a. NonEmpty (Disj a) -> Disj a
<> :: Disj a -> Disj a -> Disj a
$c<> :: forall a. Disj a -> Disj a -> Disj a
Semigroup, Disj a
[Disj a] -> Disj a
Disj a -> Disj a -> Disj a
forall a. Semigroup (Disj a)
forall a. Disj a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [Disj a] -> Disj a
forall a. Disj a -> Disj a -> Disj a
mconcat :: [Disj a] -> Disj a
$cmconcat :: forall a. [Disj a] -> Disj a
mappend :: Disj a -> Disj a -> Disj a
$cmappend :: forall a. Disj a -> Disj a -> Disj a
mempty :: Disj a
$cmempty :: forall a. Disj a
Monoid)

--- | Conjunction of atoms ('a')
newtype Conj a = Conj { forall a. Conj a -> [a]
unConj :: [a] }
  deriving (Int -> Conj a -> ShowS
forall a. Show a => Int -> Conj a -> ShowS
forall a. Show a => [Conj a] -> ShowS
forall a. Show a => Conj a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Conj a] -> ShowS
$cshowList :: forall a. Show a => [Conj a] -> ShowS
show :: Conj a -> String
$cshow :: forall a. Show a => Conj a -> String
showsPrec :: Int -> Conj a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Conj a -> ShowS
Show, forall a b. a -> Conj b -> Conj a
forall a b. (a -> b) -> Conj a -> Conj b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Conj b -> Conj a
$c<$ :: forall a b. a -> Conj b -> Conj a
fmap :: forall a b. (a -> b) -> Conj a -> Conj b
$cfmap :: forall a b. (a -> b) -> Conj a -> Conj b
Functor, NonEmpty (Conj a) -> Conj a
Conj a -> Conj a -> Conj a
forall b. Integral b => b -> Conj a -> Conj a
forall a. NonEmpty (Conj a) -> Conj a
forall a. Conj a -> Conj a -> Conj a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> Conj a -> Conj a
stimes :: forall b. Integral b => b -> Conj a -> Conj a
$cstimes :: forall a b. Integral b => b -> Conj a -> Conj a
sconcat :: NonEmpty (Conj a) -> Conj a
$csconcat :: forall a. NonEmpty (Conj a) -> Conj a
<> :: Conj a -> Conj a -> Conj a
$c<> :: forall a. Conj a -> Conj a -> Conj a
Semigroup, Conj a
[Conj a] -> Conj a
Conj a -> Conj a -> Conj a
forall a. Semigroup (Conj a)
forall a. Conj a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [Conj a] -> Conj a
forall a. Conj a -> Conj a -> Conj a
mconcat :: [Conj a] -> Conj a
$cmconcat :: forall a. [Conj a] -> Conj a
mappend :: Conj a -> Conj a -> Conj a
$cmappend :: forall a. Conj a -> Conj a -> Conj a
mempty :: Conj a
$cmempty :: forall a. Conj a
Monoid)

--- | Conjunctive Normal Form
newtype CNF a = CNF { forall a. CNF a -> Conj (Disj (Signed a))
unCNF :: Conj (Disj (Signed a)) }
  deriving (Int -> CNF a -> ShowS
forall a. Show a => Int -> CNF a -> ShowS
forall a. Show a => [CNF a] -> ShowS
forall a. Show a => CNF a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CNF a] -> ShowS
$cshowList :: forall a. Show a => [CNF a] -> ShowS
show :: CNF a -> String
$cshow :: forall a. Show a => CNF a -> String
showsPrec :: Int -> CNF a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CNF a -> ShowS
Show, NonEmpty (CNF a) -> CNF a
CNF a -> CNF a -> CNF a
forall b. Integral b => b -> CNF a -> CNF a
forall a. NonEmpty (CNF a) -> CNF a
forall a. CNF a -> CNF a -> CNF a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> CNF a -> CNF a
stimes :: forall b. Integral b => b -> CNF a -> CNF a
$cstimes :: forall a b. Integral b => b -> CNF a -> CNF a
sconcat :: NonEmpty (CNF a) -> CNF a
$csconcat :: forall a. NonEmpty (CNF a) -> CNF a
<> :: CNF a -> CNF a -> CNF a
$c<> :: forall a. CNF a -> CNF a -> CNF a
Semigroup, CNF a
[CNF a] -> CNF a
CNF a -> CNF a -> CNF a
forall a. Semigroup (CNF a)
forall a. CNF a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [CNF a] -> CNF a
forall a. CNF a -> CNF a -> CNF a
mconcat :: [CNF a] -> CNF a
$cmconcat :: forall a. [CNF a] -> CNF a
mappend :: CNF a -> CNF a -> CNF a
$cmappend :: forall a. CNF a -> CNF a -> CNF a
mempty :: CNF a
$cmempty :: forall a. CNF a
Monoid)

--- | Disjunctive Normal Form
newtype DNF a = DNF { forall a. DNF a -> Disj (Conj (Signed a))
unDNF :: Disj (Conj (Signed a)) }
  deriving (Int -> DNF a -> ShowS
forall a. Show a => Int -> DNF a -> ShowS
forall a. Show a => [DNF a] -> ShowS
forall a. Show a => DNF a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DNF a] -> ShowS
$cshowList :: forall a. Show a => [DNF a] -> ShowS
show :: DNF a -> String
$cshow :: forall a. Show a => DNF a -> String
showsPrec :: Int -> DNF a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DNF a -> ShowS
Show, NonEmpty (DNF a) -> DNF a
DNF a -> DNF a -> DNF a
forall b. Integral b => b -> DNF a -> DNF a
forall a. NonEmpty (DNF a) -> DNF a
forall a. DNF a -> DNF a -> DNF a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> DNF a -> DNF a
stimes :: forall b. Integral b => b -> DNF a -> DNF a
$cstimes :: forall a b. Integral b => b -> DNF a -> DNF a
sconcat :: NonEmpty (DNF a) -> DNF a
$csconcat :: forall a. NonEmpty (DNF a) -> DNF a
<> :: DNF a -> DNF a -> DNF a
$c<> :: forall a. DNF a -> DNF a -> DNF a
Semigroup, DNF a
[DNF a] -> DNF a
DNF a -> DNF a -> DNF a
forall a. Semigroup (DNF a)
forall a. DNF a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [DNF a] -> DNF a
forall a. DNF a -> DNF a -> DNF a
mconcat :: [DNF a] -> DNF a
$cmconcat :: forall a. [DNF a] -> DNF a
mappend :: DNF a -> DNF a -> DNF a
$cmappend :: forall a. DNF a -> DNF a -> DNF a
mempty :: DNF a
$cmempty :: forall a. DNF a
Monoid)

instance Functor CNF where
  fmap :: forall a b. (a -> b) -> CNF a -> CNF b
fmap a -> b
f (CNF Conj (Disj (Signed a))
x) = forall a. Conj (Disj (Signed a)) -> CNF a
CNF (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) Conj (Disj (Signed a))
x)

instance Boolean CNF where
  CNF a
l /\ :: forall a. CNF a -> CNF a -> CNF a
/\ CNF a
r = CNF a
l forall a. Monoid a => a -> a -> a
`mappend` CNF a
r
  CNF a
l \/ :: forall a. CNF a -> CNF a -> CNF a
\/ CNF a
r = forall a. Conj (Disj (Signed a)) -> CNF a
CNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Conj a
Conj [ Disj (Signed a)
x forall a. Monoid a => a -> a -> a
`mappend` Disj (Signed a)
y | Disj (Signed a)
x <- forall a. Conj a -> [a]
unConj forall a b. (a -> b) -> a -> b
$ forall a. CNF a -> Conj (Disj (Signed a))
unCNF CNF a
l
                                      , Disj (Signed a)
y <- forall a. Conj a -> [a]
unConj forall a b. (a -> b) -> a -> b
$ forall a. CNF a -> Conj (Disj (Signed a))
unCNF CNF a
r ]
  bNot :: forall a. CNF a -> CNF a
bNot     = forall a. HasCallStack => String -> a
error String
"bNot on CNF"
  bTrue :: forall a. CNF a
bTrue    = forall a. Conj (Disj (Signed a)) -> CNF a
CNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Conj a
Conj[]
  bFalse :: forall a. CNF a
bFalse   = forall a. Conj (Disj (Signed a)) -> CNF a
CNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Conj a
Conj[forall a. [a] -> Disj a
Disj[]]
  bConst :: forall a. Signed a -> CNF a
bConst Signed a
x = forall a. Conj (Disj (Signed a)) -> CNF a
CNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Conj a
Conj[forall a. [a] -> Disj a
Disj[Signed a
x]]


instance Functor DNF where
  fmap :: forall a b. (a -> b) -> DNF a -> DNF b
fmap a -> b
f (DNF Disj (Conj (Signed a))
x) = forall a. Disj (Conj (Signed a)) -> DNF a
DNF (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) Disj (Conj (Signed a))
x)

instance Boolean DNF where
  DNF a
l /\ :: forall a. DNF a -> DNF a -> DNF a
/\ DNF a
r = forall a. Disj (Conj (Signed a)) -> DNF a
DNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Disj a
Disj [ Conj (Signed a)
x forall a. Monoid a => a -> a -> a
`mappend` Conj (Signed a)
y | Conj (Signed a)
x <- forall a. Disj a -> [a]
unDisj forall a b. (a -> b) -> a -> b
$ forall a. DNF a -> Disj (Conj (Signed a))
unDNF DNF a
l
                                      , Conj (Signed a)
y <- forall a. Disj a -> [a]
unDisj forall a b. (a -> b) -> a -> b
$ forall a. DNF a -> Disj (Conj (Signed a))
unDNF DNF a
r ]
  DNF a
l \/ :: forall a. DNF a -> DNF a -> DNF a
\/ DNF a
r = DNF a
l forall a. Monoid a => a -> a -> a
`mappend` DNF a
r
  bNot :: forall a. DNF a -> DNF a
bNot     = forall a. HasCallStack => String -> a
error String
"bNot on CNF"
  bTrue :: forall a. DNF a
bTrue    = forall a. Disj (Conj (Signed a)) -> DNF a
DNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Disj a
Disj[forall a. [a] -> Conj a
Conj[]]
  bFalse :: forall a. DNF a
bFalse   = forall a. Disj (Conj (Signed a)) -> DNF a
DNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Disj a
Disj[]
  bConst :: forall a. Signed a -> DNF a
bConst Signed a
x = forall a. Disj (Conj (Signed a)) -> DNF a
DNF forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Disj a
Disj[forall a. [a] -> Conj a
Conj[Signed a
x]]

-- | Reduce a boolean tree annotated by booleans to a single boolean.
reduceBoolExpr :: BoolExpr Bool -> Bool
reduceBoolExpr :: BoolExpr Bool -> Bool
reduceBoolExpr = forall a. (a -> Bool) -> BoolExpr a -> Bool
evalBoolExpr forall a. a -> a
id

-- Given a evaluation function of constants, returns an evaluation
-- function over boolean trees.
--
-- Note that since 'BoolExpr' is a functor, one can simply use
-- 'reduceBoolExpr':
--
-- @
-- evalBoolExpr f = reduceBoolExpr . fmap (f$)
-- @
evalBoolExpr :: (a -> Bool) -> (BoolExpr a -> Bool)
evalBoolExpr :: forall a. (a -> Bool) -> BoolExpr a -> Bool
evalBoolExpr a -> Bool
env BoolExpr a
expr = forall b a. Eval b a -> (a -> b) -> b
runEval (forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
expr) a -> Bool
env

-- | Returns constants used in a given boolean tree, these
-- constants are returned signed depending one how many
-- negations stands over a given constant.
constants :: BoolExpr a -> [Signed a]
constants :: forall a. BoolExpr a -> [Signed a]
constants = forall {a}. Bool -> BoolExpr a -> [Signed a]
go Bool
True
  where go :: Bool -> BoolExpr a -> [Signed a]
go Bool
sign (BAnd BoolExpr a
a BoolExpr a
b) = Bool -> BoolExpr a -> [Signed a]
go Bool
sign BoolExpr a
a forall a. [a] -> [a] -> [a]
++ Bool -> BoolExpr a -> [Signed a]
go Bool
sign BoolExpr a
b
        go Bool
sign (BOr  BoolExpr a
a BoolExpr a
b) = Bool -> BoolExpr a -> [Signed a]
go Bool
sign BoolExpr a
a forall a. [a] -> [a] -> [a]
++ Bool -> BoolExpr a -> [Signed a]
go Bool
sign BoolExpr a
b
        go Bool
sign (BNot BoolExpr a
t)   = Bool -> BoolExpr a -> [Signed a]
go (Bool -> Bool
not Bool
sign) BoolExpr a
t
        go Bool
_     BoolExpr a
BTrue     = []
        go Bool
_     BoolExpr a
BFalse    = []
        go Bool
sign (BConst Signed a
x) = [if Bool
sign then Signed a
x else forall a. Signed a -> Signed a
negateSigned Signed a
x]


dualize :: Boolean f => BoolExpr a -> f a
dualize :: forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize (BAnd BoolExpr a
l BoolExpr a
r) = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
\/ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize BoolExpr a
r
dualize (BOr  BoolExpr a
l BoolExpr a
r) = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
/\ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize BoolExpr a
r
dualize  BoolExpr a
BTrue     = forall (f :: * -> *) a. Boolean f => f a
bFalse
dualize  BoolExpr a
BFalse    = forall (f :: * -> *) a. Boolean f => f a
bTrue
dualize (BConst Signed a
c) = forall (f :: * -> *) a. Boolean f => Signed a -> f a
negateConstant Signed a
c
dualize (BNot BoolExpr a
e)   = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
fromBoolExpr BoolExpr a
e
-- When dualize is used by pushNotInwards not BNot remain,
-- hence it makes sense to assert that dualize does not
-- have to work on BNot. However `dualize` can be freely
-- used as a fancy `bNot`.
-- dualize (BNot _)   = error "dualize: impossible"


-- | Push the negations inwards as much as possible.
-- The resulting boolean tree no longer use negations.

pushNotInwards :: Boolean f => BoolExpr a -> f a
pushNotInwards :: forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards (BAnd BoolExpr a
l BoolExpr a
r)   = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
/\ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards BoolExpr a
r
pushNotInwards (BOr  BoolExpr a
l BoolExpr a
r)   = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards BoolExpr a
l forall (f :: * -> *) a. Boolean f => f a -> f a -> f a
\/ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards BoolExpr a
r
pushNotInwards (BNot BoolExpr a
t  )   = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
dualize forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards BoolExpr a
t
pushNotInwards  BoolExpr a
BTrue       = forall (f :: * -> *) a. Boolean f => f a
bTrue
pushNotInwards  BoolExpr a
BFalse      = forall (f :: * -> *) a. Boolean f => f a
bFalse
pushNotInwards (BConst Signed a
c)   = forall (f :: * -> *) a. Boolean f => Signed a -> f a
bConst Signed a
c

-- | Convert a 'CNF' (a boolean expression in conjunctive normal form)
-- to any other form supported by 'Boolean'.
fromCNF :: Boolean f => CNF a -> f a
fromCNF :: forall (f :: * -> *) a. Boolean f => CNF a -> f a
fromCNF = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAll (forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAny forall (f :: * -> *) a. Boolean f => Signed a -> f a
bConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Disj a -> [a]
unDisj) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Conj a -> [a]
unConj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. CNF a -> Conj (Disj (Signed a))
unCNF

-- | Convert a 'DNF' (a boolean expression in disjunctive normal form)
-- to any other form supported by 'Boolean'.
fromDNF :: Boolean f => DNF a -> f a
fromDNF :: forall (f :: * -> *) a. Boolean f => DNF a -> f a
fromDNF = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAny (forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Boolean f) =>
(a -> f b) -> t a -> f b
bAll forall (f :: * -> *) a. Boolean f => Signed a -> f a
bConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Conj a -> [a]
unConj) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Disj a -> [a]
unDisj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. DNF a -> Disj (Conj (Signed a))
unDNF

-- | Convert a boolean tree to a conjunctive normal form.
boolTreeToCNF :: BoolExpr a -> CNF a
boolTreeToCNF :: forall a. BoolExpr a -> CNF a
boolTreeToCNF = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards

-- | Convert a boolean tree to a disjunctive normal form.
boolTreeToDNF :: BoolExpr a -> DNF a
boolTreeToDNF :: forall a. BoolExpr a -> DNF a
boolTreeToDNF = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards

-- | Reduce a boolean expression in conjunctive normal form to a single
-- boolean.
reduceCNF :: CNF Bool -> Bool
reduceCNF :: CNF Bool -> Bool
reduceCNF = forall a. Eval a a -> a
runEvalId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Boolean f => CNF a -> f a
fromCNF

-- | Reduce a boolean expression in disjunctive normal form to a single
-- boolean.
reduceDNF :: DNF Bool -> Bool
reduceDNF :: DNF Bool -> Bool
reduceDNF = forall a. Eval a a -> a
runEvalId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Boolean f => DNF a -> f a
fromDNF

evalSigned :: (a -> Bool) -> Signed a -> Bool
evalSigned :: forall a. (a -> Bool) -> Signed a -> Bool
evalSigned a -> Bool
f (Positive a
x) = a -> Bool
f a
x
evalSigned a -> Bool
f (Negative a
x) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a -> Bool
f a
x

reduceSigned :: Signed Bool -> Bool
reduceSigned :: Signed Bool -> Bool
reduceSigned = forall a. (a -> Bool) -> Signed a -> Bool
evalSigned forall a. a -> a
id

negateSigned :: Signed a -> Signed a
negateSigned :: forall a. Signed a -> Signed a
negateSigned (Positive a
x) = forall a. a -> Signed a
Negative a
x
negateSigned (Negative a
x) = forall a. a -> Signed a
Positive a
x

negateConstant :: Boolean f => Signed a -> f a
negateConstant :: forall (f :: * -> *) a. Boolean f => Signed a -> f a
negateConstant = forall (f :: * -> *) a. Boolean f => Signed a -> f a
bConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Signed a -> Signed a
negateSigned

{-
prop_reduceBoolExpr_EQ_reduceCNF t = reduceBoolExpr t == reduceCNF (boolTreeToCNF t)

prop_reduceBoolExpr_EQ_reduceCNF_Bool = prop_reduceBoolExpr_EQ_reduceCNF (BConst . not)

prop_reduceBoolExpr_EQ_reduceDNF t = reduceBoolExpr t == reduceDNF (boolTreeToDNF t)

prop_reduceBoolExpr_EQ_reduceDNF_Bool = prop_reduceBoolExpr_EQ_reduceDNF (BConst . not)

{-* Generated by DrIFT : Look, but Don't Touch. *-}
instance (Arbitrary a) => Arbitrary (BoolExpr a) where
    arbitrary = do x <- choose (1::Int,6) -- :: Int inserted manually
                   case x of
                     1 -> do  v1 <- arbitrary
                              v2 <- arbitrary
                              return (BAnd v1 v2)
                     2 -> do  v1 <- arbitrary
                              v2 <- arbitrary
                              return (BOr v1 v2)
                     3 -> do  v1 <- arbitrary
                              return (BNot v1)
                     4 -> do  return (BTrue )
                     5 -> do  return (BFalse )
                     6 -> do  v1 <- arbitrary
                              return (BConst v1)
    --coarbitrary = error "coarbitrary not yet supported" -- quickcheck2
-}