{-# 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

import Data.List ( nub, intersperse )
import Data.Data

import GHC.Utils.Monad
import GHC.Utils.Outputable
import GHC.Utils.Binary
import GHC.Parser.Annotation ( LocatedL )
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
forall a. Eq a => BooleanFormula a -> BooleanFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BooleanFormula a -> BooleanFormula a -> Bool
$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
Eq, BooleanFormula a -> DataType
BooleanFormula a -> Constr
forall {a}. Data a => Typeable (BooleanFormula a)
forall a. Data a => BooleanFormula a -> DataType
forall a. Data a => BooleanFormula a -> Constr
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 (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> BooleanFormula a -> m (BooleanFormula a)
gmapQi :: forall u.
Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> BooleanFormula a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanFormula a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanFormula a -> r
gmapT :: (forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> 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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
dataTypeOf :: BooleanFormula a -> DataType
$cdataTypeOf :: forall a. Data a => BooleanFormula a -> DataType
toConstr :: BooleanFormula a -> Constr
$ctoConstr :: forall a. Data a => BooleanFormula a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> 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)
Data, 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
<$ :: forall a b. a -> BooleanFormula b -> BooleanFormula a
$c<$ :: forall a b. a -> BooleanFormula b -> BooleanFormula a
fmap :: forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
$cfmap :: forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
Functor, 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
product :: forall a. Num a => BooleanFormula a -> a
$cproduct :: forall a. Num a => BooleanFormula a -> a
sum :: forall a. Num a => BooleanFormula a -> a
$csum :: forall a. Num a => BooleanFormula a -> a
minimum :: forall a. Ord a => BooleanFormula a -> a
$cminimum :: forall a. Ord a => BooleanFormula a -> a
maximum :: forall a. Ord a => BooleanFormula a -> a
$cmaximum :: forall a. Ord a => BooleanFormula a -> a
elem :: forall a. Eq a => a -> BooleanFormula a -> Bool
$celem :: forall a. Eq a => a -> BooleanFormula a -> Bool
length :: forall a. BooleanFormula a -> Int
$clength :: forall a. BooleanFormula a -> Int
null :: forall a. BooleanFormula a -> Bool
$cnull :: forall a. BooleanFormula a -> Bool
toList :: forall a. BooleanFormula a -> [a]
$ctoList :: forall a. BooleanFormula a -> [a]
foldl1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
foldr1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
fold :: forall m. Monoid m => BooleanFormula m -> m
$cfold :: forall m. Monoid m => BooleanFormula m -> m
Foldable, Functor BooleanFormula
Foldable 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)
sequence :: forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
traverse :: 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)
Traversable)

mkVar :: a -> BooleanFormula a
mkVar :: forall a. a -> BooleanFormula a
mkVar = forall a. a -> BooleanFormula a
Var

mkFalse, mkTrue :: BooleanFormula a
mkFalse :: forall a. BooleanFormula a
mkFalse = forall a. [LBooleanFormula a] -> BooleanFormula a
Or []
mkTrue :: forall a. BooleanFormula a
mkTrue = 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 = forall a. BooleanFormula a
mkFalse
mkBool Bool
True  = 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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. BooleanFormula a
mkFalse (forall a. [LBooleanFormula a] -> BooleanFormula a
mkAnd' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM 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)) = 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 [])) = forall a. Maybe a
Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
  fromAnd GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x = 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] = forall l e. GenLocated l e -> e
unLoc GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x
  mkAnd' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs = 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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. BooleanFormula a
mkTrue (forall a. [LBooleanFormula a] -> BooleanFormula a
mkOr' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM 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)) = forall a. a -> Maybe a
Just [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs
  fromOr (L SrcSpanAnn' (EpAnn AnnList)
_ (And [])) = forall a. Maybe a
Nothing
  fromOr GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x = 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] = forall l e. GenLocated l e -> e
unLoc GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)
x
  mkOr' [GenLocated (SrcSpanAnn' (EpAnn AnnList)) (BooleanFormula a)]
xs = 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs
eval a -> Bool
f (Or [LBooleanFormula a]
xs)  = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs
eval a -> Bool
f (Parens LBooleanFormula a
x) = forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (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 -> forall a. a -> BooleanFormula a
Var a
a
  Just Bool
b  -> forall a. Bool -> BooleanFormula a
mkBool Bool
b
simplify a -> Maybe Bool
f (And [LBooleanFormula a]
xs) = forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd (forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpanAnn' (EpAnn AnnList)
l BooleanFormula a
x) -> forall l e. l -> e -> GenLocated l e
L SrcSpanAnn' (EpAnn AnnList)
l (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) = forall a. Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr (forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpanAnn' (EpAnn AnnList)
l BooleanFormula a
x) -> forall l e. l -> e -> GenLocated l e
L SrcSpanAnn' (EpAnn AnnList)
l (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) = forall a.
Eq a =>
(a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify a -> Maybe Bool
f (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
    | forall a. BooleanFormula a -> Bool
isTrue BooleanFormula a
bf' = forall a. Maybe a
Nothing
    | Bool
otherwise  = forall a. a -> Maybe a
Just BooleanFormula a
bf'
  where
  f' :: a -> Maybe Bool
f' a
x = if a -> Bool
f a
x then forall a. a -> Maybe a
Just Bool
True else forall a. Maybe a
Nothing
  bf' :: BooleanFormula a
bf' = 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 forall a. Eq a => a -> a -> Bool
== a
y
And [LBooleanFormula a]
xs `impliesAtom` a
y = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\LBooleanFormula a
x -> (forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
x -> (forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y) [LBooleanFormula a]
xs
Parens LBooleanFormula a
x `impliesAtom` a
y = (forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
x) 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 = forall a. Uniquable a => Clause a -> Clause a -> Bool
go (forall a. UniqSet a -> [BooleanFormula a] -> Clause a
Clause forall a. UniqSet a
emptyUniqSet [BooleanFormula a
e1]) (forall a. UniqSet a -> [BooleanFormula a] -> Clause a
Clause 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 | forall a. Uniquable a => a -> Clause a -> Bool
memberClauseAtoms a
x Clause a
r -> Bool
True
                  | Bool
otherwise -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go (forall a. Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms Clause a
l a
x) { clauseExprs :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
hyps } Clause a
r
            Parens LBooleanFormula a
hyp' -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
hyp'forall a. a -> [a] -> [a]
:[BooleanFormula a]
hyps }     Clause a
r
            And [LBooleanFormula a]
hyps'  -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = forall a b. (a -> b) -> [a] -> [b]
map forall l e. GenLocated l e -> e
unLoc [LBooleanFormula a]
hyps' forall a. [a] -> [a] -> [a]
++ [BooleanFormula a]
hyps } Clause a
r
            Or [LBooleanFormula a]
hyps'   -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
hyp' -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
hyp'forall a. a -> [a] -> [a]
:[BooleanFormula a]
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 | forall a. Uniquable a => a -> Clause a -> Bool
memberClauseAtoms a
x Clause a
l -> Bool
True
                  | Bool
otherwise -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l (forall a. Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms Clause a
r a
x) { clauseExprs :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
cons }
            Parens LBooleanFormula a
con' -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs :: [BooleanFormula a]
clauseExprs = forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
con'forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }
            And [LBooleanFormula a]
cons'   -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\LBooleanFormula a
con' -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs :: [BooleanFormula a]
clauseExprs = forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
con'forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }) [LBooleanFormula a]
cons'
            Or [LBooleanFormula a]
cons'    -> forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l Clause a
r { clauseExprs :: [BooleanFormula a]
clauseExprs = forall a b. (a -> b) -> [a] -> [b]
map forall l e. GenLocated l e -> e
unLoc [LBooleanFormula a]
cons' forall a. [a] -> [a] -> [a]
++ [BooleanFormula a]
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 :: UniqSet a
clauseAtoms = forall a. Uniquable a => UniqSet a -> a -> UniqSet a
addOneToUniqSet (forall a. Clause a -> UniqSet a
clauseAtoms Clause a
c) a
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 forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` 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 forall a. Ord a => a -> a -> Bool
> Rational
0) forall a b. (a -> b) -> a -> b
$ SDoc
empty
  go Rational
p (And [LBooleanFormula a]
xs) = Rational -> [SDoc] -> SDoc
pprAnd Rational
p (forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula a -> SDoc
go Rational
3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
  go Rational
_ (Or  []) = SDoc -> SDoc
keyword forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"FALSE"
  go Rational
p (Or  [LBooleanFormula a]
xs) = Rational -> [SDoc] -> SDoc
pprOr Rational
p (forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula a -> SDoc
go Rational
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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 = forall a.
(Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' Rational -> a -> SDoc
pprVar forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr
  where
  pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p forall a. Ord a => a -> a -> Bool
> a
3) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma
  pprOr :: a -> [SDoc] -> SDoc
pprOr  a
p = Bool -> SDoc -> SDoc
cparen (a
p forall a. Ord a => a -> a -> Bool
> a
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse SDoc
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 = forall a.
(Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' forall {a} {p}. Outputable a => p -> a -> SDoc
pprVar forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr Rational
0
  where
  pprVar :: p -> a -> SDoc
pprVar p
_ = SDoc -> SDoc
quotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
ppr
  pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p forall a. Ord a => a -> a -> Bool
> a
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
pprAnd'
  pprAnd' :: [SDoc] -> SDoc
pprAnd' [] = SDoc
empty
  pprAnd' [SDoc
x,SDoc
y] = SDoc
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"and" SDoc -> SDoc -> SDoc
<+> SDoc
y
  pprAnd' xs :: [SDoc]
xs@(SDoc
_:[SDoc]
_) = [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma (forall a. [a] -> [a]
init [SDoc]
xs)) SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
", and" SDoc -> SDoc -> SDoc
<+> forall a. [a] -> a
last [SDoc]
xs
  pprOr :: a -> [SDoc] -> SDoc
pprOr a
p [SDoc]
xs = Bool -> SDoc -> SDoc
cparen (a
p forall a. Ord a => a -> a -> Bool
> a
1) forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"either" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep (forall a. a -> [a] -> [a]
intersperse (String -> SDoc
text String
"or") [SDoc]
xs)

instance (OutputableBndr a) => Outputable (BooleanFormula a) where
  ppr :: BooleanFormula a -> SDoc
ppr = forall a. OutputableBndr a => BooleanFormula a -> SDoc
pprBooleanFormulaNormal

pprBooleanFormulaNormal :: (OutputableBndr a)
                        => BooleanFormula a -> SDoc
pprBooleanFormulaNormal :: forall a. OutputableBndr a => BooleanFormula a -> SDoc
pprBooleanFormulaNormal = forall a. OutputableBndr a => BooleanFormula a -> SDoc
go
  where
    go :: BooleanFormula a -> SDoc
go (Var a
x)    = forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc a
x
    go (And [LBooleanFormula a]
xs)   = [SDoc] -> SDoc
fsep forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma (forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula a -> SDoc
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
    go (Or [])    = SDoc -> SDoc
keyword forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"FALSE"
    go (Or [LBooleanFormula a]
xs)    = [SDoc] -> SDoc
fsep forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse SDoc
vbar (forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula a -> SDoc
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
    go (Parens LBooleanFormula a
x) = SDoc -> SDoc
parens (BooleanFormula a -> SDoc
go forall a b. (a -> b) -> a -> b
$ 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ BinHandle
bh (Or  [LBooleanFormula a]
xs)   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ BinHandle
bh (Parens LBooleanFormula a
x) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
3 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh 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 -> forall a. a -> BooleanFormula a
Var    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      Word8
1 -> forall a. [LBooleanFormula a] -> BooleanFormula a
And    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      Word8
2 -> forall a. [LBooleanFormula a] -> BooleanFormula a
Or     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      Word8
_ -> forall a. LBooleanFormula a -> BooleanFormula a
Parens forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => BinHandle -> IO a
get BinHandle
bh