{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoDeriveAnyClass #-}
module Data.BoolExpr (
Boolean (..),
BoolExpr (..),
reduceBoolExpr,
evalBoolExpr,
Eval (..),
runEvalId,
Signed (..),
negateSigned,
evalSigned,
constants,
negateConstant,
CNF (..),
Conj (..),
boolTreeToCNF,
Disj (..),
DNF (..),
boolTreeToDNF,
dualize,
fromBoolExpr,
pushNotInwards,
)
where
import Control.Monad (ap)
import Data.Aeson
import Data.Char (toLower)
import Data.Traversable
import GHC.Generics (Generic)
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, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Signed a) x -> Signed a
forall a x. Signed a -> Rep (Signed a) x
$cto :: forall a x. Rep (Signed a) x -> Signed a
$cfrom :: forall a x. Signed a -> Rep (Signed a) x
Generic, 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 9 /\
infix 9 \/
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
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, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (BoolExpr a) x -> BoolExpr a
forall a x. BoolExpr a -> Rep (BoolExpr a) x
$cto :: forall a x. Rep (BoolExpr a) x -> BoolExpr a
$cfrom :: forall a x. BoolExpr a -> Rep (BoolExpr a) x
Generic, 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 )
encodingOptions :: Options
encodingOptions :: Options
encodingOptions =
Options
defaultOptions
{ sumEncoding :: SumEncoding
sumEncoding = SumEncoding
ObjectWithSingleField
, constructorTagModifier :: ShowS
constructorTagModifier = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower
}
instance (ToJSON a) => ToJSON (Signed a) where
toJSON :: Signed a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
instance (ToJSON a) => ToJSON (BoolExpr a) where
toJSON :: BoolExpr a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
instance (ToJSON a) => ToJSON (DNF a) where
toJSON :: DNF a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
instance (ToJSON a) => ToJSON (CNF a) where
toJSON :: CNF a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
instance (ToJSON a) => ToJSON (Conj a) where
toJSON :: Conj a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
instance (ToJSON a) => ToJSON (Disj a) where
toJSON :: Disj a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
encodingOptions
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
(/\) = forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
BAnd
\/ :: forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
(\/) = 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 a. Eval b a -> Eval b a -> Eval b a
(/\) = forall b a. (b -> b -> b) -> Eval b a -> Eval b a -> Eval b a
liftE2 Bool -> Bool -> Bool
(&&)
\/ :: forall a. Eval b a -> Eval b a -> Eval b a
(\/) = 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))
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
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.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Disj a) x -> Disj a
forall a x. Disj a -> Rep (Disj a) x
$cto :: forall a x. Rep (Disj a) x -> Disj a
$cfrom :: forall a x. Disj a -> Rep (Disj a) x
Generic, 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)
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.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Conj a) x -> Conj a
forall a x. Conj a -> Rep (Conj a) x
$cto :: forall a x. Rep (Conj a) x -> Conj a
$cfrom :: forall a x. Conj a -> Rep (Conj a) x
Generic, 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)
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, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (CNF a) x -> CNF a
forall a x. CNF a -> Rep (CNF a) x
$cto :: forall a x. Rep (CNF a) x -> CNF a
$cfrom :: forall a x. CNF a -> Rep (CNF a) x
Generic, 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)
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, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (DNF a) x -> DNF a
forall a x. DNF a -> Rep (DNF a) x
$cto :: forall a x. Rep (DNF a) x -> DNF a
$cfrom :: forall a x. DNF a -> Rep (DNF a) x
Generic, 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]]
reduceBoolExpr :: BoolExpr Bool -> Bool
reduceBoolExpr :: BoolExpr Bool -> Bool
reduceBoolExpr = forall a. (a -> Bool) -> BoolExpr a -> Bool
evalBoolExpr forall a. a -> a
id
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
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
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
boolTreeToCNF :: BoolExpr a -> CNF a
boolTreeToCNF :: forall a. BoolExpr a -> CNF a
boolTreeToCNF = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards
boolTreeToDNF :: BoolExpr a -> DNF a
boolTreeToDNF :: forall a. BoolExpr a -> DNF a
boolTreeToDNF = forall (f :: * -> *) a. Boolean f => BoolExpr a -> f a
pushNotInwards
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
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