{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable  #-}

--------------------------------------------------------------------------------
-- | Boolean formulas without quantifiers and without negation.
-- Such a formula consists of variables, conjunctions (and), and disjunctions (or).
--
-- This module is used to represent minimal complete definitions for classes.
--
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

----------------------------------------------------------------------
-- Boolean formula type and smart constructors
----------------------------------------------------------------------

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 []

-- Convert a Bool to a BooleanFormula
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

-- Make a conjunction, and try to simplify
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
  -- See Note [Simplification of BooleanFormulas]
  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
     -- assume that xs are already simplified
     -- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xs
  fromAnd (L SrcSpanAnn' (EpAnn AnnList)
_ (Or [])) = Maybe [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
forall a. Maybe a
Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
  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
  -- See Note [Simplification of BooleanFormulas]
  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


{-
Note [Simplification of BooleanFormulas]
~~~~~~~~~~~~~~~~~~~~~~
The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
 1. Collapsing nested ands and ors, so
     `(mkAnd [x, And [y,z]]`
    is represented as
     `And [x,y,z]`
    Implemented by `fromAnd`/`fromOr`
 2. Collapsing trivial ands and ors, so
     `mkAnd [x]` becomes just `x`.
    Implemented by mkAnd' / mkOr'
 3. Conjunction with false, disjunction with true is simplified, i.e.
     `mkAnd [mkFalse,x]` becomes `mkFalse`.
 4. Common subexpression elimination:
     `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.

This simplification is not exhaustive, in the sense that it will not produce
the smallest possible equivalent expression. For example,
`Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
is not. A general simplifier would need to use something like BDDs.

The reason behind the (crude) simplifier is to make for more user friendly
error messages. E.g. for the code
  > class Foo a where
  >     {-# MINIMAL bar, (foo, baq | foo, quux) #-}
  > instance Foo Int where
  >     bar = ...
  >     baz = ...
  >     quux = ...
We don't show a ridiculous error message like
    Implement () and (either (`foo' and ()) or (`foo' and ()))
-}

----------------------------------------------------------------------
-- Evaluation and simplification
----------------------------------------------------------------------

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 a boolean formula.
-- The argument function should give the truth of the atoms, or Nothing if undecided.
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)

-- Test if a boolean formula is satisfied when the given values are assigned to the atoms
-- if it is, returns Nothing
-- if it is not, return (Just remainder)
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

-- prop_simplify:
--   eval f x == True   <==>  isTrue  (simplify (Just . f) x)
--   eval f x == False  <==>  isFalse (simplify (Just . f) x)

-- If the boolean formula holds, does that mean that the given atom is always true?
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
           -- we have all of xs, so one of them implying y is enough
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

-- A small sequent calculus proof engine.
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

----------------------------------------------------------------------
-- Pretty printing
----------------------------------------------------------------------

-- Pretty print a BooleanFormula,
-- using the arguments as pretty printers for Var, And and Or respectively
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)

-- Pretty print in source syntax, "a | b | c,d,e"
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

-- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
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)


----------------------------------------------------------------------
-- Binary
----------------------------------------------------------------------

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