{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable #-}
module GHC.Data.BooleanFormula (
BooleanFormula(..), LBooleanFormula,
mkFalse, mkTrue, mkAnd, mkOr, mkVar,
isFalse, isTrue,
eval, simplify, isUnsatisfied,
implies, impliesAtom,
pprBooleanFormula, pprBooleanFormulaNice
) where
import GHC.Prelude hiding ( init, last )
import Data.List ( nub, intersperse )
import Data.List.NonEmpty ( NonEmpty (..), init, last )
import Data.Data
import GHC.Utils.Monad
import GHC.Utils.Outputable
import GHC.Utils.Binary
import GHC.Parser.Annotation ( LocatedL, noLocA )
import GHC.Types.SrcLoc
import GHC.Types.Unique
import GHC.Types.Unique.Set
type LBooleanFormula a = LocatedL (BooleanFormula a)
data BooleanFormula a = Var a | And [LBooleanFormula a] | Or [LBooleanFormula a]
| Parens (LBooleanFormula a)
deriving (BooleanFormula a -> BooleanFormula a -> Bool
(BooleanFormula a -> BooleanFormula a -> Bool)
-> (BooleanFormula a -> BooleanFormula a -> Bool)
-> Eq (BooleanFormula a)
forall a. Eq a => BooleanFormula a -> BooleanFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => BooleanFormula a -> BooleanFormula a -> Bool
== :: BooleanFormula a -> BooleanFormula a -> Bool
$c/= :: forall a. Eq a => BooleanFormula a -> BooleanFormula a -> Bool
/= :: BooleanFormula a -> BooleanFormula a -> Bool
Eq, Typeable (BooleanFormula a)
Typeable (BooleanFormula a) =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BooleanFormula a
-> c (BooleanFormula a))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a))
-> (BooleanFormula a -> Constr)
-> (BooleanFormula a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanFormula a)))
-> ((forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r)
-> (forall u.
(forall d. Data d => d -> u) -> BooleanFormula a -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> BooleanFormula a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a))
-> Data (BooleanFormula a)
BooleanFormula a -> Constr
BooleanFormula a -> DataType
(forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
forall a. Data a => Typeable (BooleanFormula a)
forall a. Data a => BooleanFormula a -> Constr
forall a. Data a => BooleanFormula a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BooleanFormula a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanFormula a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> c (BooleanFormula a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanFormula 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) -> BooleanFormula a -> u
forall u. (forall d. Data d => d -> u) -> BooleanFormula a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> c (BooleanFormula a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanFormula a))
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> c (BooleanFormula a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> c (BooleanFormula a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a)
$ctoConstr :: forall a. Data a => BooleanFormula a -> Constr
toConstr :: BooleanFormula a -> Constr
$cdataTypeOf :: forall a. Data a => BooleanFormula a -> DataType
dataTypeOf :: BooleanFormula a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanFormula a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanFormula a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
gmapT :: (forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanFormula a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BooleanFormula a -> [u]
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BooleanFormula a -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BooleanFormula a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
Data, (forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b)
-> (forall a b. a -> BooleanFormula b -> BooleanFormula a)
-> Functor BooleanFormula
forall a b. a -> BooleanFormula b -> BooleanFormula a
forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
fmap :: forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
$c<$ :: forall a b. a -> BooleanFormula b -> BooleanFormula a
<$ :: forall a b. a -> BooleanFormula b -> BooleanFormula a
Functor, (forall m. Monoid m => BooleanFormula m -> m)
-> (forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m)
-> (forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m)
-> (forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b)
-> (forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b)
-> (forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b)
-> (forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b)
-> (forall a. (a -> a -> a) -> BooleanFormula a -> a)
-> (forall a. (a -> a -> a) -> BooleanFormula a -> a)
-> (forall a. BooleanFormula a -> [a])
-> (forall a. BooleanFormula a -> Bool)
-> (forall a. BooleanFormula a -> Int)
-> (forall a. Eq a => a -> BooleanFormula a -> Bool)
-> (forall a. Ord a => BooleanFormula a -> a)
-> (forall a. Ord a => BooleanFormula a -> a)
-> (forall a. Num a => BooleanFormula a -> a)
-> (forall a. Num a => BooleanFormula a -> a)
-> Foldable BooleanFormula
forall a. Eq a => a -> BooleanFormula a -> Bool
forall a. Num a => BooleanFormula a -> a
forall a. Ord a => BooleanFormula a -> a
forall m. Monoid m => BooleanFormula m -> m
forall a. BooleanFormula a -> Bool
forall a. BooleanFormula a -> Int
forall a. BooleanFormula a -> [a]
forall a. (a -> a -> a) -> BooleanFormula a -> a
forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => BooleanFormula m -> m
fold :: forall m. Monoid m => BooleanFormula m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
foldr :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
foldl :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
foldr1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
foldl1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
$ctoList :: forall a. BooleanFormula a -> [a]
toList :: forall a. BooleanFormula a -> [a]
$cnull :: forall a. BooleanFormula a -> Bool
null :: forall a. BooleanFormula a -> Bool
$clength :: forall a. BooleanFormula a -> Int
length :: forall a. BooleanFormula a -> Int
$celem :: forall a. Eq a => a -> BooleanFormula a -> Bool
elem :: forall a. Eq a => a -> BooleanFormula a -> Bool
$cmaximum :: forall a. Ord a => BooleanFormula a -> a
maximum :: forall a. Ord a => BooleanFormula a -> a
$cminimum :: forall a. Ord a => BooleanFormula a -> a
minimum :: forall a. Ord a => BooleanFormula a -> a
$csum :: forall a. Num a => BooleanFormula a -> a
sum :: forall a. Num a => BooleanFormula a -> a
$cproduct :: forall a. Num a => BooleanFormula a -> a
product :: forall a. Num a => BooleanFormula a -> a
Foldable, Functor BooleanFormula
Foldable BooleanFormula
(Functor BooleanFormula, Foldable BooleanFormula) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b))
-> (forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b))
-> (forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a))
-> Traversable BooleanFormula
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
sequence :: forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
Traversable)
mkVar :: a -> BooleanFormula a
mkVar :: forall a. a -> BooleanFormula a
mkVar = a -> BooleanFormula a
forall a. a -> BooleanFormula a
Var
mkFalse, mkTrue :: BooleanFormula a
mkFalse :: forall a. BooleanFormula a
mkFalse = [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or []
mkTrue :: forall a. BooleanFormula a
mkTrue = [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And []
mkBool :: Bool -> BooleanFormula a
mkBool :: forall a. Bool -> BooleanFormula a
mkBool Bool
False = BooleanFormula a
forall a. BooleanFormula a
mkFalse
mkBool Bool
True = BooleanFormula a
forall a. BooleanFormula a
mkTrue
mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd :: forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd = BooleanFormula a
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula a
forall a. BooleanFormula a
mkFalse ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
mkAnd' ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. Eq a => [a] -> [a]
nub) (Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd
where
fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd :: forall a. LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd (L SrcSpanAnn' (EpAnn AnnList)
_ (And [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs)) = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs
fromAnd (L SrcSpanAnn' (EpAnn AnnList)
_ (Or [])) = Maybe [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. Maybe a
Nothing
fromAnd GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x]
mkAnd' :: [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
mkAnd' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x] = GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x
mkAnd' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs
mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr :: forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr = BooleanFormula a
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula a
forall a. BooleanFormula a
mkTrue ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
mkOr' ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. Eq a => [a] -> [a]
nub) (Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a)
-> ([GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)])
-> [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. LBooleanFormula a -> Maybe [LBooleanFormula a]
fromOr
where
fromOr :: GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
fromOr (L SrcSpanAnn' (EpAnn AnnList)
_ (Or [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs)) = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs
fromOr (L SrcSpanAnn' (EpAnn AnnList)
_ (And [])) = Maybe [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. Maybe a
Nothing
fromOr GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> Maybe
[GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x]
mkOr' :: [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
mkOr' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x] = GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
-> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x
mkOr' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs = [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
-> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs
isFalse :: BooleanFormula a -> Bool
isFalse :: forall a. BooleanFormula a -> Bool
isFalse (Or []) = Bool
True
isFalse BooleanFormula a
_ = Bool
False
isTrue :: BooleanFormula a -> Bool
isTrue :: forall a. BooleanFormula a -> Bool
isTrue (And []) = Bool
True
isTrue BooleanFormula a
_ = Bool
False
eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval :: forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (Var a
x) = a -> Bool
f a
x
eval a -> Bool
f (And [LBooleanFormula a]
xs) = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((a -> Bool) -> BooleanFormula a -> Bool
forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (BooleanFormula a -> Bool)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs
eval a -> Bool
f (Or [LBooleanFormula a]
xs) = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((a -> Bool) -> BooleanFormula a -> Bool
forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (BooleanFormula a -> Bool)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs
eval a -> Bool
f (Parens LBooleanFormula a
x) = (a -> Bool) -> BooleanFormula a -> Bool
forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x)
simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify :: forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f (Var a
a) = case a -> Maybe Bool
f a
a of
Maybe Bool
Nothing -> a -> BooleanFormula a
forall a. a -> BooleanFormula a
Var a
a
Just Bool
b -> Bool -> BooleanFormula a
forall a. Bool -> BooleanFormula a
mkBool Bool
b
simplify a -> Maybe Bool
f (And [LBooleanFormula a]
xs) = [LBooleanFormula a] -> BooleanFormula a
forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd ((LBooleanFormula a -> LBooleanFormula a)
-> [LBooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpanAnn' (EpAnn AnnList)
l BooleanFormula a
x) -> SrcSpanAnn' (EpAnn AnnList)
-> BooleanFormula a -> LBooleanFormula a
forall l e. l -> e -> GenLocated l e
L SrcSpanAnn' (EpAnn AnnList)
l ((a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f BooleanFormula a
x)) [LBooleanFormula a]
xs)
simplify a -> Maybe Bool
f (Or [LBooleanFormula a]
xs) = [LBooleanFormula a] -> BooleanFormula a
forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr ((LBooleanFormula a -> LBooleanFormula a)
-> [LBooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpanAnn' (EpAnn AnnList)
l BooleanFormula a
x) -> SrcSpanAnn' (EpAnn AnnList)
-> BooleanFormula a -> LBooleanFormula a
forall l e. l -> e -> GenLocated l e
L SrcSpanAnn' (EpAnn AnnList)
l ((a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f BooleanFormula a
x)) [LBooleanFormula a]
xs)
simplify a -> Maybe Bool
f (Parens LBooleanFormula a
x) = (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x)
isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
isUnsatisfied :: forall a.
Eq a =>
(a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
isUnsatisfied a -> Bool
f BooleanFormula a
bf
| BooleanFormula a -> Bool
forall a. BooleanFormula a -> Bool
isTrue BooleanFormula a
bf' = Maybe (BooleanFormula a)
forall a. Maybe a
Nothing
| Bool
otherwise = BooleanFormula a -> Maybe (BooleanFormula a)
forall a. a -> Maybe a
Just BooleanFormula a
bf'
where
f' :: a -> Maybe Bool
f' a
x = if a -> Bool
f a
x then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True else Maybe Bool
forall a. Maybe a
Nothing
bf' :: BooleanFormula a
bf' = (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f' BooleanFormula a
bf
impliesAtom :: Eq a => BooleanFormula a -> a -> Bool
Var a
x impliesAtom :: forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
And [LBooleanFormula a]
xs `impliesAtom` a
y = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\LBooleanFormula a
x -> (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) BooleanFormula a -> a -> Bool
forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y) [LBooleanFormula a]
xs
Or [LBooleanFormula a]
xs `impliesAtom` a
y = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
x -> (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) BooleanFormula a -> a -> Bool
forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y) [LBooleanFormula a]
xs
Parens LBooleanFormula a
x `impliesAtom` a
y = (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) BooleanFormula a -> a -> Bool
forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y
implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
implies :: forall a.
Uniquable a =>
BooleanFormula a -> BooleanFormula a -> Bool
implies BooleanFormula a
e1 BooleanFormula a
e2 = Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go (UniqSet a -> [BooleanFormula a] -> Clause a
forall a. UniqSet a -> [BooleanFormula a] -> Clause a
Clause UniqSet a
forall a. UniqSet a
emptyUniqSet [BooleanFormula a
e1]) (UniqSet a -> [BooleanFormula a] -> Clause a
forall a. UniqSet a -> [BooleanFormula a] -> Clause a
Clause UniqSet a
forall a. UniqSet a
emptyUniqSet [BooleanFormula a
e2])
where
go :: Uniquable a => Clause a -> Clause a -> Bool
go :: forall a. Uniquable a => Clause a -> Clause a -> Bool
go l :: Clause a
l@Clause{ clauseExprs :: forall a. Clause a -> [BooleanFormula a]
clauseExprs = BooleanFormula a
hyp:[BooleanFormula a]
hyps } Clause a
r =
case BooleanFormula a
hyp of
Var a
x | a -> Clause a -> Bool
forall a. Uniquable a => a -> Clause a -> Bool
memberClauseAtoms a
x Clause a
r -> Bool
True
| Bool
otherwise -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go (Clause a -> a -> Clause a
forall a. Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms Clause a
l a
x) { clauseExprs = hyps } Clause a
r
Parens LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs = unLoc hyp':hyps } Clause a
r
And [LBooleanFormula a]
hyps' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs = map unLoc hyps' ++ hyps } Clause a
r
Or [LBooleanFormula a]
hyps' -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs = unLoc hyp':hyps } Clause a
r) [LBooleanFormula a]
hyps'
go Clause a
l r :: Clause a
r@Clause{ clauseExprs :: forall a. Clause a -> [BooleanFormula a]
clauseExprs = BooleanFormula a
con:[BooleanFormula a]
cons } =
case BooleanFormula a
con of
Var a
x | a -> Clause a -> Bool
forall a. Uniquable a => a -> Clause a -> Bool
memberClauseAtoms a
x Clause a
l -> Bool
True
| Bool
otherwise -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l (Clause a -> a -> Clause a
forall a. Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms Clause a
r a
x) { clauseExprs = cons }
Parens LBooleanFormula a
con' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs = unLoc con':cons }
And [LBooleanFormula a]
cons' -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
con' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs = unLoc con':cons }) [LBooleanFormula a]
cons'
Or [LBooleanFormula a]
cons' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs = map unLoc cons' ++ cons }
go Clause a
_ Clause a
_ = Bool
False
data Clause a = Clause {
forall a. Clause a -> UniqSet a
clauseAtoms :: UniqSet a,
forall a. Clause a -> [BooleanFormula a]
clauseExprs :: [BooleanFormula a]
}
extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms :: forall a. Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms Clause a
c a
x = Clause a
c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }
memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
memberClauseAtoms :: forall a. Uniquable a => a -> Clause a -> Bool
memberClauseAtoms a
x Clause a
c = a
x a -> UniqSet a -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` Clause a -> UniqSet a
forall a. Clause a -> UniqSet a
clauseAtoms Clause a
c
pprBooleanFormula' :: (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula' :: forall a.
(Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' Rational -> a -> SDoc
pprVar Rational -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
pprOr = Rational -> BooleanFormula a -> SDoc
go
where
go :: Rational -> BooleanFormula a -> SDoc
go Rational
p (Var a
x) = Rational -> a -> SDoc
pprVar Rational
p a
x
go Rational
p (And []) = Bool -> SDoc -> SDoc
cparen (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
forall doc. IsOutput doc => doc
empty
go Rational
p (And [LBooleanFormula a]
xs) = Rational -> [SDoc] -> SDoc
pprAnd Rational
p ((LBooleanFormula a -> SDoc) -> [LBooleanFormula a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula a -> SDoc
go Rational
3 (BooleanFormula a -> SDoc)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
go Rational
_ (Or []) = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"FALSE"
go Rational
p (Or [LBooleanFormula a]
xs) = Rational -> [SDoc] -> SDoc
pprOr Rational
p ((LBooleanFormula a -> SDoc) -> [LBooleanFormula a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula a -> SDoc
go Rational
2 (BooleanFormula a -> SDoc)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
go Rational
p (Parens LBooleanFormula a
x) = Rational -> BooleanFormula a -> SDoc
go Rational
p (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x)
pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula :: forall a.
(Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula Rational -> a -> SDoc
pprVar = (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
forall a.
(Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' Rational -> a -> SDoc
pprVar Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr
where
pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
3) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma
pprOr :: a -> [SDoc] -> SDoc
pprOr a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
2) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse SDoc
forall doc. IsLine doc => doc
vbar
pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
pprBooleanFormulaNice :: forall a. Outputable a => BooleanFormula a -> SDoc
pprBooleanFormulaNice = (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
forall a.
(Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' Rational -> a -> SDoc
forall {a} {p}. Outputable a => p -> a -> SDoc
pprVar Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr Rational
0
where
pprVar :: p -> a -> SDoc
pprVar p
_ = SDoc -> SDoc
quotes (SDoc -> SDoc) -> (a -> SDoc) -> a -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SDoc
forall a. Outputable a => a -> SDoc
ppr
pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
pprAnd'
pprAnd' :: [doc] -> doc
pprAnd' [] = doc
forall doc. IsOutput doc => doc
empty
pprAnd' [doc
x,doc
y] = doc
x doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> doc
forall doc. IsLine doc => String -> doc
text String
"and" doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> doc
y
pprAnd' (doc
x:[doc]
xs) = [doc] -> doc
forall doc. IsLine doc => [doc] -> doc
fsep (doc -> [doc] -> [doc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate doc
forall doc. IsLine doc => doc
comma (NonEmpty doc -> [doc]
forall a. NonEmpty a -> [a]
init (doc
xdoc -> [doc] -> NonEmpty doc
forall a. a -> [a] -> NonEmpty a
:|[doc]
xs))) doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<> String -> doc
forall doc. IsLine doc => String -> doc
text String
", and" doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> NonEmpty doc -> doc
forall a. NonEmpty a -> a
last (doc
xdoc -> [doc] -> NonEmpty doc
forall a. a -> [a] -> NonEmpty a
:|[doc]
xs)
pprOr :: a -> [SDoc] -> SDoc
pprOr a
p [SDoc]
xs = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"either" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep (SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"or") [SDoc]
xs)
instance (OutputableBndr a) => Outputable (BooleanFormula a) where
ppr :: BooleanFormula a -> SDoc
ppr = BooleanFormula a -> SDoc
forall a. OutputableBndr a => BooleanFormula a -> SDoc
pprBooleanFormulaNormal
pprBooleanFormulaNormal :: (OutputableBndr a)
=> BooleanFormula a -> SDoc
pprBooleanFormulaNormal :: forall a. OutputableBndr a => BooleanFormula a -> SDoc
pprBooleanFormulaNormal = BooleanFormula a -> SDoc
forall a. OutputableBndr a => BooleanFormula a -> SDoc
go
where
go :: BooleanFormula a -> SDoc
go (Var a
x) = a -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc a
x
go (And [LBooleanFormula a]
xs) = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma ((LBooleanFormula a -> SDoc) -> [LBooleanFormula a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula a -> SDoc
go (BooleanFormula a -> SDoc)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
go (Or []) = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"FALSE"
go (Or [LBooleanFormula a]
xs) = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse SDoc
forall doc. IsLine doc => doc
vbar ((LBooleanFormula a -> SDoc) -> [LBooleanFormula a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula a -> SDoc
go (BooleanFormula a -> SDoc)
-> (LBooleanFormula a -> BooleanFormula a)
-> LBooleanFormula a
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
go (Parens LBooleanFormula a
x) = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (BooleanFormula a -> SDoc
go (BooleanFormula a -> SDoc) -> BooleanFormula a -> SDoc
forall a b. (a -> b) -> a -> b
$ LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x)
instance Binary a => Binary (BooleanFormula a) where
put_ :: BinHandle -> BooleanFormula a -> IO ()
put_ BinHandle
bh (Var a
x) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> a -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh a
x
put_ BinHandle
bh (And [LBooleanFormula a]
xs) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [BooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc (LBooleanFormula a -> BooleanFormula a)
-> [LBooleanFormula a] -> [BooleanFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LBooleanFormula a]
xs)
put_ BinHandle
bh (Or [LBooleanFormula a]
xs) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [BooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc (LBooleanFormula a -> BooleanFormula a)
-> [LBooleanFormula a] -> [BooleanFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LBooleanFormula a]
xs)
put_ BinHandle
bh (Parens LBooleanFormula a
x) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
3 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> BooleanFormula a -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x)
get :: BinHandle -> IO (BooleanFormula a)
get BinHandle
bh = do
Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
case Word8
h of
Word8
0 -> a -> BooleanFormula a
forall a. a -> BooleanFormula a
Var (a -> BooleanFormula a) -> IO a -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO a
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
Word8
1 -> [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And ([LBooleanFormula a] -> BooleanFormula a)
-> ([BooleanFormula a] -> [LBooleanFormula a])
-> [BooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BooleanFormula a -> LBooleanFormula a)
-> [BooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BooleanFormula a -> LBooleanFormula a
forall a an. a -> LocatedAn an a
noLocA ([BooleanFormula a] -> BooleanFormula a)
-> IO [BooleanFormula a] -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [BooleanFormula a]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
Word8
2 -> [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or ([LBooleanFormula a] -> BooleanFormula a)
-> ([BooleanFormula a] -> [LBooleanFormula a])
-> [BooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BooleanFormula a -> LBooleanFormula a)
-> [BooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BooleanFormula a -> LBooleanFormula a
forall a an. a -> LocatedAn an a
noLocA ([BooleanFormula a] -> BooleanFormula a)
-> IO [BooleanFormula a] -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [BooleanFormula a]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
Word8
_ -> LBooleanFormula a -> BooleanFormula a
forall a. LBooleanFormula a -> BooleanFormula a
Parens (LBooleanFormula a -> BooleanFormula a)
-> (BooleanFormula a -> LBooleanFormula a)
-> BooleanFormula a
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BooleanFormula a -> LBooleanFormula a
forall a an. a -> LocatedAn an a
noLocA (BooleanFormula a -> BooleanFormula a)
-> IO (BooleanFormula a) -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (BooleanFormula a)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh