{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
             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 BooleanFormula (
        BooleanFormula(..), LBooleanFormula,
        mkFalse, mkTrue, mkAnd, mkOr, mkVar,
        isFalse, isTrue,
        eval, simplify, isUnsatisfied,
        implies, impliesAtom,
        pprBooleanFormula, pprBooleanFormulaNice
  ) where

import GhcPrelude

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

import MonadUtils
import Outputable
import Binary
import SrcLoc
import Unique
import UniqSet

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

type LBooleanFormula a = Located (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
/= :: 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, Typeable (BooleanFormula a)
DataType
Constr
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 -> DataType
BooleanFormula a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (BooleanFormula a))
(forall b. Data b => b -> b)
-> BooleanFormula a -> BooleanFormula a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanFormula a -> c (BooleanFormula a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanFormula a)
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 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))
$cParens :: Constr
$cOr :: Constr
$cAnd :: Constr
$cVar :: Constr
$tBooleanFormula :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> BooleanFormula a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanFormula a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (BooleanFormula a)
Data, a -> BooleanFormula b -> BooleanFormula a
(a -> b) -> BooleanFormula a -> BooleanFormula b
(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
<$ :: a -> BooleanFormula b -> BooleanFormula a
$c<$ :: forall a b. a -> BooleanFormula b -> BooleanFormula a
fmap :: (a -> b) -> BooleanFormula a -> BooleanFormula b
$cfmap :: forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
Functor, BooleanFormula a -> Bool
(a -> m) -> BooleanFormula a -> m
(a -> b -> b) -> b -> BooleanFormula a -> b
(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
product :: BooleanFormula a -> a
$cproduct :: forall a. Num a => BooleanFormula a -> a
sum :: BooleanFormula a -> a
$csum :: forall a. Num a => BooleanFormula a -> a
minimum :: BooleanFormula a -> a
$cminimum :: forall a. Ord a => BooleanFormula a -> a
maximum :: BooleanFormula a -> a
$cmaximum :: forall a. Ord a => BooleanFormula a -> a
elem :: a -> BooleanFormula a -> Bool
$celem :: forall a. Eq a => a -> BooleanFormula a -> Bool
length :: BooleanFormula a -> Int
$clength :: forall a. BooleanFormula a -> Int
null :: BooleanFormula a -> Bool
$cnull :: forall a. BooleanFormula a -> Bool
toList :: BooleanFormula a -> [a]
$ctoList :: forall a. BooleanFormula a -> [a]
foldl1 :: (a -> a -> a) -> BooleanFormula a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
foldr1 :: (a -> a -> a) -> BooleanFormula a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> BooleanFormula a -> a
foldl' :: (b -> a -> b) -> b -> BooleanFormula a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
foldl :: (b -> a -> b) -> b -> BooleanFormula a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> BooleanFormula a -> b
foldr' :: (a -> b -> b) -> b -> BooleanFormula a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
foldr :: (a -> b -> b) -> b -> BooleanFormula a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> BooleanFormula a -> b
foldMap' :: (a -> m) -> BooleanFormula a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
foldMap :: (a -> m) -> BooleanFormula a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> BooleanFormula a -> m
fold :: BooleanFormula m -> m
$cfold :: forall m. Monoid m => BooleanFormula m -> m
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
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
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 :: BooleanFormula (m a) -> m (BooleanFormula a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
BooleanFormula (m a) -> m (BooleanFormula a)
mapM :: (a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> BooleanFormula a -> m (BooleanFormula b)
sequenceA :: BooleanFormula (f a) -> f (BooleanFormula a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
BooleanFormula (f a) -> f (BooleanFormula a)
traverse :: (a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> BooleanFormula a -> f (BooleanFormula b)
$cp2Traversable :: Foldable BooleanFormula
$cp1Traversable :: Functor BooleanFormula
Traversable)

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

mkFalse, mkTrue :: BooleanFormula a
mkFalse :: BooleanFormula a
mkFalse = [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or []
mkTrue :: 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 :: Bool -> BooleanFormula a
mkBool False = BooleanFormula a
forall a. BooleanFormula a
mkFalse
mkBool True  = BooleanFormula a
forall a. BooleanFormula a
mkTrue

-- Make a conjunction, and try to simplify
mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd :: [LBooleanFormula a] -> BooleanFormula a
mkAnd = BooleanFormula a
-> ([LBooleanFormula a] -> BooleanFormula a)
-> Maybe [LBooleanFormula a]
-> BooleanFormula a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula a
forall a. BooleanFormula a
mkFalse ([LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
mkAnd' ([LBooleanFormula a] -> BooleanFormula a)
-> ([LBooleanFormula a] -> [LBooleanFormula a])
-> [LBooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LBooleanFormula a] -> [LBooleanFormula a]
forall a. Eq a => [a] -> [a]
nub) (Maybe [LBooleanFormula a] -> BooleanFormula a)
-> ([LBooleanFormula a] -> Maybe [LBooleanFormula a])
-> [LBooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LBooleanFormula a -> Maybe [LBooleanFormula a])
-> [LBooleanFormula a] -> Maybe [LBooleanFormula a]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM LBooleanFormula a -> Maybe [LBooleanFormula a]
forall a. LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd
  where
  -- See Note [Simplification of BooleanFormulas]
  fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
  fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd (L _ (And xs :: [LBooleanFormula a]
xs)) = [LBooleanFormula a] -> Maybe [LBooleanFormula a]
forall a. a -> Maybe a
Just [LBooleanFormula a]
xs
     -- assume that xs are already simplified
     -- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xs
  fromAnd (L _ (Or [])) = Maybe [LBooleanFormula a]
forall a. Maybe a
Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
  fromAnd x :: LBooleanFormula a
x = [LBooleanFormula a] -> Maybe [LBooleanFormula a]
forall a. a -> Maybe a
Just [LBooleanFormula a
x]
  mkAnd' :: [LBooleanFormula a] -> BooleanFormula a
mkAnd' [x :: LBooleanFormula a
x] = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
x
  mkAnd' xs :: [LBooleanFormula a]
xs = [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And [LBooleanFormula a]
xs

mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr :: [LBooleanFormula a] -> BooleanFormula a
mkOr = BooleanFormula a
-> ([LBooleanFormula a] -> BooleanFormula a)
-> Maybe [LBooleanFormula a]
-> BooleanFormula a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula a
forall a. BooleanFormula a
mkTrue ([LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
mkOr' ([LBooleanFormula a] -> BooleanFormula a)
-> ([LBooleanFormula a] -> [LBooleanFormula a])
-> [LBooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LBooleanFormula a] -> [LBooleanFormula a]
forall a. Eq a => [a] -> [a]
nub) (Maybe [LBooleanFormula a] -> BooleanFormula a)
-> ([LBooleanFormula a] -> Maybe [LBooleanFormula a])
-> [LBooleanFormula a]
-> BooleanFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LBooleanFormula a -> Maybe [LBooleanFormula a])
-> [LBooleanFormula a] -> Maybe [LBooleanFormula a]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM LBooleanFormula a -> Maybe [LBooleanFormula a]
forall a. LBooleanFormula a -> Maybe [LBooleanFormula a]
fromOr
  where
  -- See Note [Simplification of BooleanFormulas]
  fromOr :: GenLocated SrcSpan (BooleanFormula a)
-> Maybe [GenLocated SrcSpan (BooleanFormula a)]
fromOr (L _ (Or xs :: [GenLocated SrcSpan (BooleanFormula a)]
xs)) = [GenLocated SrcSpan (BooleanFormula a)]
-> Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated SrcSpan (BooleanFormula a)]
xs
  fromOr (L _ (And [])) = Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. Maybe a
Nothing
  fromOr x :: GenLocated SrcSpan (BooleanFormula a)
x = [GenLocated SrcSpan (BooleanFormula a)]
-> Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -> Maybe a
Just [GenLocated SrcSpan (BooleanFormula a)
x]
  mkOr' :: [LBooleanFormula a] -> BooleanFormula a
mkOr' [x :: LBooleanFormula a
x] = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
x
  mkOr' xs :: [LBooleanFormula a]
xs = [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or [LBooleanFormula 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 :: BooleanFormula a -> Bool
isFalse (Or []) = Bool
True
isFalse _ = Bool
False

isTrue :: BooleanFormula a -> Bool
isTrue :: BooleanFormula a -> Bool
isTrue (And []) = Bool
True
isTrue _ = Bool
False

eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval f :: a -> Bool
f (Var x :: a
x)  = a -> Bool
f a
x
eval f :: a -> Bool
f (And xs :: [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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs
eval f :: a -> Bool
f (Or xs :: [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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs
eval f :: a -> Bool
f (Parens x :: LBooleanFormula a
x) = (a -> Bool) -> BooleanFormula a -> Bool
forall a. (a -> Bool) -> BooleanFormula a -> Bool
eval a -> Bool
f (LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
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 :: (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify f :: a -> Maybe Bool
f (Var a :: a
a) = case a -> Maybe Bool
f a
a of
  Nothing -> a -> BooleanFormula a
forall a. a -> BooleanFormula a
Var a
a
  Just b :: Bool
b  -> Bool -> BooleanFormula a
forall a. Bool -> BooleanFormula a
mkBool Bool
b
simplify f :: a -> Maybe Bool
f (And xs :: [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 l :: SrcSpan
l x :: BooleanFormula a
x) -> SrcSpan -> BooleanFormula a -> LBooleanFormula a
forall l e. l -> e -> GenLocated l e
L SrcSpan
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 f :: a -> Maybe Bool
f (Or xs :: [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 l :: SrcSpan
l x :: BooleanFormula a
x) -> SrcSpan -> BooleanFormula a -> LBooleanFormula a
forall l e. l -> e -> GenLocated l e
L SrcSpan
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 f :: a -> Maybe Bool
f (Parens x :: 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 -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
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 :: (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
isUnsatisfied f :: a -> Bool
f bf :: 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' x :: 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 x :: a
x  impliesAtom :: BooleanFormula a -> a -> Bool
`impliesAtom` y :: a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
And xs :: [LBooleanFormula a]
xs `impliesAtom` y :: a
y = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\x :: LBooleanFormula a
x -> (LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
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  xs :: [LBooleanFormula a]
xs `impliesAtom` y :: a
y = (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\x :: LBooleanFormula a
x -> (LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
x) BooleanFormula a -> a -> Bool
forall a. Eq a => BooleanFormula a -> a -> Bool
`impliesAtom` a
y) [LBooleanFormula a]
xs
Parens x :: LBooleanFormula a
x `impliesAtom` y :: a
y = (LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
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 :: BooleanFormula a -> BooleanFormula a -> Bool
implies e1 :: BooleanFormula a
e1 e2 :: 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 :: Clause a -> Clause a -> Bool
go l :: Clause a
l@Clause{ clauseExprs :: forall a. Clause a -> [BooleanFormula a]
clauseExprs = hyp :: BooleanFormula a
hyp:hyps :: [BooleanFormula a]
hyps } r :: Clause a
r =
        case BooleanFormula a
hyp of
            Var x :: 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 :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
hyps } Clause a
r
            Parens hyp' :: LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
hyp'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
hyps }     Clause a
r
            And hyps' :: [LBooleanFormula a]
hyps'  -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = (LBooleanFormula a -> BooleanFormula a)
-> [LBooleanFormula a] -> [BooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map LBooleanFormula a -> BooleanFormula a
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LBooleanFormula a]
hyps' [BooleanFormula a] -> [BooleanFormula a] -> [BooleanFormula a]
forall a. [a] -> [a] -> [a]
++ [BooleanFormula a]
hyps } Clause a
r
            Or hyps' :: [LBooleanFormula a]
hyps'   -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\hyp' :: LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
hyp'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
hyps } Clause a
r) [LBooleanFormula a]
hyps'
    go l :: Clause a
l r :: Clause a
r@Clause{ clauseExprs :: forall a. Clause a -> [BooleanFormula a]
clauseExprs = con :: BooleanFormula a
con:cons :: [BooleanFormula a]
cons } =
        case BooleanFormula a
con of
            Var x :: 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 :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
cons }
            Parens con' :: 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 :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
con'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }
            And cons' :: [LBooleanFormula a]
cons'   -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\con' :: 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 :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
con'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }) [LBooleanFormula a]
cons'
            Or cons' :: [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 :: [BooleanFormula a]
clauseExprs = (LBooleanFormula a -> BooleanFormula a)
-> [LBooleanFormula a] -> [BooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map LBooleanFormula a -> BooleanFormula a
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LBooleanFormula a]
cons' [BooleanFormula a] -> [BooleanFormula a] -> [BooleanFormula a]
forall a. [a] -> [a] -> [a]
++ [BooleanFormula a]
cons }
    go _ _ = Bool
False

-- A small sequent calculus proof engine.
data Clause a = Clause {
        Clause a -> UniqSet a
clauseAtoms :: UniqSet a,
        Clause a -> [BooleanFormula a]
clauseExprs :: [BooleanFormula a]
    }
extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms :: Clause a -> a -> Clause a
extendClauseAtoms c :: Clause a
c x :: a
x = Clause a
c { clauseAtoms :: UniqSet a
clauseAtoms = UniqSet a -> a -> UniqSet a
forall a. Uniquable a => UniqSet a -> a -> UniqSet a
addOneToUniqSet (Clause a -> UniqSet a
forall a. Clause a -> UniqSet a
clauseAtoms Clause a
c) a
x }

memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
memberClauseAtoms :: a -> Clause a -> Bool
memberClauseAtoms x :: a
x c :: 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' :: (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula a
-> SDoc
pprBooleanFormula' pprVar :: Rational -> a -> SDoc
pprVar pprAnd :: Rational -> [SDoc] -> SDoc
pprAnd pprOr :: Rational -> [SDoc] -> SDoc
pprOr = Rational -> BooleanFormula a -> SDoc
go
  where
  go :: Rational -> BooleanFormula a -> SDoc
go p :: Rational
p (Var x :: a
x)  = Rational -> a -> SDoc
pprVar Rational
p a
x
  go p :: Rational
p (And []) = Bool -> SDoc -> SDoc
cparen (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
empty
  go p :: Rational
p (And xs :: [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 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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs)
  go _ (Or  []) = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "FALSE"
  go p :: Rational
p (Or  xs :: [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 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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs)
  go p :: Rational
p (Parens x :: LBooleanFormula a
x) = Rational -> BooleanFormula a -> SDoc
go Rational
p (LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
x)

-- Pretty print in source syntax, "a | b | c,d,e"
pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula pprVar :: 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 p :: a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> 3) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma
  pprOr :: a -> [SDoc] -> SDoc
pprOr  p :: a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> 2) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
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
vbar

-- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
pprBooleanFormulaNice :: 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 0
  where
  pprVar :: p -> a -> SDoc
pprVar _ = 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 p :: a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
pprAnd'
  pprAnd' :: [SDoc] -> SDoc
pprAnd' [] = SDoc
empty
  pprAnd' [x :: SDoc
x,y :: SDoc
y] = SDoc
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "and" SDoc -> SDoc -> SDoc
<+> SDoc
y
  pprAnd' xs :: [SDoc]
xs@(_:_) = [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ([SDoc] -> [SDoc]
forall a. [a] -> [a]
init [SDoc]
xs)) SDoc -> SDoc -> SDoc
<> String -> SDoc
text ", and" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
forall a. [a] -> a
last [SDoc]
xs
  pprOr :: a -> [SDoc] -> SDoc
pprOr p :: a
p xs :: [SDoc]
xs = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "either" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep (SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse (String -> SDoc
text "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 :: BooleanFormula a -> SDoc
pprBooleanFormulaNormal = BooleanFormula a -> SDoc
forall a. OutputableBndr a => BooleanFormula a -> SDoc
go
  where
    go :: BooleanFormula a -> SDoc
go (Var x :: a
x)    = a -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc a
x
    go (And xs :: [LBooleanFormula a]
xs)   = [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs)
    go (Or [])    = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "FALSE"
    go (Or xs :: [LBooleanFormula a]
xs)    = [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse SDoc
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 a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LBooleanFormula a]
xs)
    go (Parens x :: LBooleanFormula a
x) = SDoc -> SDoc
parens (BooleanFormula a -> SDoc
go (BooleanFormula a -> SDoc) -> BooleanFormula a -> SDoc
forall a b. (a -> b) -> a -> b
$ LBooleanFormula a -> SrcSpanLess (LBooleanFormula a)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LBooleanFormula a
x)


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

instance Binary a => Binary (BooleanFormula a) where
  put_ :: BinHandle -> BooleanFormula a -> IO ()
put_ bh :: BinHandle
bh (Var x :: a
x)    = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh 0 IO () -> IO () -> IO ()
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_ bh :: BinHandle
bh (And xs :: [LBooleanFormula a]
xs)   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh 1 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [LBooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ bh :: BinHandle
bh (Or  xs :: [LBooleanFormula a]
xs)   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh 2 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [LBooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ bh :: BinHandle
bh (Parens x :: LBooleanFormula a
x) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh 3 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> LBooleanFormula a -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh LBooleanFormula a
x

  get :: BinHandle -> IO (BooleanFormula a)
get bh :: BinHandle
bh = do
    Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
    case Word8
h of
      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
      1 -> [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And    ([LBooleanFormula a] -> BooleanFormula a)
-> IO [LBooleanFormula a] -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [LBooleanFormula a]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      2 -> [LBooleanFormula a] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or     ([LBooleanFormula a] -> BooleanFormula a)
-> IO [LBooleanFormula a] -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [LBooleanFormula a]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      _ -> LBooleanFormula a -> BooleanFormula a
forall a. LBooleanFormula a -> BooleanFormula a
Parens (LBooleanFormula a -> BooleanFormula a)
-> IO (LBooleanFormula a) -> IO (BooleanFormula a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (LBooleanFormula a)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh