{-# 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 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.Types.SrcLoc
import GHC.Types.Unique
import GHC.Types.Unique.Set

----------------------------------------------------------------------
-- 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
External instance of the constraint type Eq SrcSpan
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq a
External instance of the constraint type Eq SrcSpan
External instance of the constraint type forall l e. (Eq l, Eq e) => Eq (GenLocated l e)
External instance of the constraint type forall l e. (Eq l, Eq e) => Eq (GenLocated l e)
External instance of the constraint type Eq SrcSpan
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq a
External instance of the constraint type forall a. Eq a => Eq [a]
External instance of the constraint type forall a. Eq a => Eq [a]
External instance of the constraint type forall l e. (Eq l, Eq e) => Eq (GenLocated l e)
External instance of the constraint type Eq SrcSpan
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq a
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq a
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)
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type Data SrcSpan
External instance of the constraint type Data SrcSpan
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type Data SrcSpan
External instance of the constraint type forall l e. (Data l, Data e) => Data (GenLocated l e)
Evidence bound by a type signature of the constraint type Typeable t
External instance of the constraint type forall l e. (Data l, Data e) => Data (GenLocated l e)
External instance of the constraint type Data SrcSpan
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type forall a. Data a => Data [a]
External instance of the constraint type forall l e. (Data l, Data e) => Data (GenLocated l e)
External instance of the constraint type Data SrcSpan
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type forall l e. (Data l, Data e) => Data (GenLocated l e)
External instance of the constraint type Data SrcSpan
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type forall a. Data a => Data [a]
External instance of the constraint type forall a. Data a => Data [a]
External instance of the constraint type forall l e. (Data l, Data e) => Data (GenLocated l e)
External instance of the constraint type Data SrcSpan
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type forall a. Data a => Typeable a
Evidence bound by a type signature of the constraint type Data a
External instance of the constraint type forall a. Data a => Typeable a
External instance of the constraint type forall a. Data a => Typeable a
Evidence bound by a type signature of the constraint type Data a
Instance of class: Data of the constraint type forall a. Data a => Data (BooleanFormula a)
Evidence bound by a type signature of the constraint type Data 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
Instance of class: Functor of the constraint type Functor BooleanFormula
External instance of the constraint type forall l. Functor (GenLocated l)
External instance of the constraint type Functor []
Instance of class: Functor of the constraint type Functor BooleanFormula
Instance of class: Functor of the constraint type Functor BooleanFormula
External instance of the constraint type forall l. Functor (GenLocated l)
External instance of the constraint type forall l. Functor (GenLocated l)
External instance of the constraint type Functor []
External instance of the constraint type Functor []
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
Instance of class: Foldable of the constraint type Foldable BooleanFormula
External instance of the constraint type forall l. Foldable (GenLocated l)
External instance of the constraint type Foldable []
Instance of class: Foldable of the constraint type Foldable BooleanFormula
External instance of the constraint type forall l. Foldable (GenLocated l)
External instance of the constraint type Foldable []
Instance of class: Foldable of the constraint type Foldable BooleanFormula
External instance of the constraint type forall l. Foldable (GenLocated l)
External instance of the constraint type forall l. Foldable (GenLocated l)
External instance of the constraint type Foldable []
External instance of the constraint type Foldable []
Evidence bound by a type signature of the constraint type Monoid m
Instance of class: Foldable of the constraint type Foldable BooleanFormula
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)
External instance of the constraint type forall (f :: * -> *). Applicative f => Functor f
Instance of class: Traversable of the constraint type Traversable BooleanFormula
External instance of the constraint type forall l. Traversable (GenLocated l)
External instance of the constraint type forall l. Traversable (GenLocated l)
External instance of the constraint type Traversable []
External instance of the constraint type Traversable []
External instance of the constraint type forall (f :: * -> *). Applicative f => Functor f
Evidence bound by a type signature of the constraint type Applicative f
Evidence bound by a type signature of the constraint type Applicative f
Instance of class: Foldable of the constraint type Foldable BooleanFormula
Instance of class: Functor of the constraint type Functor BooleanFormula
Instance of class: Functor of the constraint type Functor BooleanFormula
Instance of class: Traversable of the constraint type Traversable BooleanFormula
Instance of class: Foldable of the constraint type Foldable 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 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 :: [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]
External instance of the constraint type forall l e. (Eq l, Eq e) => Eq (GenLocated l e)
External instance of the constraint type Eq SrcSpan
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq 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]
External instance of the constraint type Monad Maybe
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 SrcSpan
_ (And [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 SrcSpan
_ (Or [])) = Maybe [LBooleanFormula a]
forall a. Maybe a
Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
  fromAnd LBooleanFormula a
x = [LBooleanFormula a] -> Maybe [LBooleanFormula a]
forall a. a -> Maybe a
Just [LBooleanFormula a
x]
  mkAnd' :: [GenLocated SrcSpan (BooleanFormula a)] -> BooleanFormula a
mkAnd' [GenLocated SrcSpan (BooleanFormula a)
x] = GenLocated SrcSpan (BooleanFormula a) -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (BooleanFormula a)
x
  mkAnd' [GenLocated SrcSpan (BooleanFormula a)]
xs = [GenLocated SrcSpan (BooleanFormula a)] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
And [GenLocated SrcSpan (BooleanFormula 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]
External instance of the constraint type forall l e. (Eq l, Eq e) => Eq (GenLocated l e)
External instance of the constraint type Eq SrcSpan
Instance of class: Eq of the constraint type forall a. Eq a => Eq (BooleanFormula a)
Evidence bound by a type signature of the constraint type Eq 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]
External instance of the constraint type Monad Maybe
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 SrcSpan
_ (Or [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 SrcSpan
_ (And [])) = Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. Maybe a
Nothing
  fromOr 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' :: [GenLocated SrcSpan (BooleanFormula a)] -> BooleanFormula a
mkOr' [GenLocated SrcSpan (BooleanFormula a)
x] = GenLocated SrcSpan (BooleanFormula a) -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (BooleanFormula a)
x
  mkOr' [GenLocated SrcSpan (BooleanFormula a)]
xs = [GenLocated SrcSpan (BooleanFormula a)] -> BooleanFormula a
forall a. [LBooleanFormula a] -> BooleanFormula a
Or [GenLocated SrcSpan (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 :: BooleanFormula a -> Bool
isFalse (Or []) = Bool
True
isFalse BooleanFormula a
_ = Bool
False

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

eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval :: (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
External instance of the constraint type Foldable []
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
External instance of the constraint type Foldable []
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 :: (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
Evidence bound by a type signature of the constraint type Eq a
mkAnd ((LBooleanFormula a -> LBooleanFormula a)
-> [LBooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpan
l 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
Evidence bound by a type signature of the constraint type Eq 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
Evidence bound by a type signature of the constraint type Eq a
mkOr ((LBooleanFormula a -> LBooleanFormula a)
-> [LBooleanFormula a] -> [LBooleanFormula a]
forall a b. (a -> b) -> [a] -> [b]
map (\(L SrcSpan
l 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
Evidence bound by a type signature of the constraint type Eq 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
Evidence bound by a type signature of the constraint type Eq 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 :: (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
Evidence bound by a type signature of the constraint type Eq 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 :: BooleanFormula a -> a -> Bool
`impliesAtom` a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Evidence bound by a type signature of the constraint type Eq a
== 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
External instance of the constraint type Foldable []
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
Evidence bound by a type signature of the constraint type Eq a
`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
External instance of the constraint type Foldable []
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
Evidence bound by a type signature of the constraint type Eq a
`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
Evidence bound by a type signature of the constraint type Eq a
`impliesAtom` a
y

implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
implies :: 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
Evidence bound by a type signature of the constraint type Uniquable a
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 = 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
Evidence bound by a type signature of the constraint type Uniquable a
memberClauseAtoms a
x Clause a
r -> Bool
True
                  | Bool
otherwise -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go (Clause a -> a -> Clause a
forall a. Uniquable a => Clause a -> a -> Clause a
Evidence bound by a type signature of the constraint type Uniquable a
extendClauseAtoms Clause a
l a
x) { clauseExprs :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
hyps } Clause a
r
            Parens LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
hyp'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
hyps }     Clause a
r
            And [LBooleanFormula a]
hyps'  -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
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 l e. GenLocated l e -> e
unLoc [LBooleanFormula a]
hyps' [BooleanFormula a] -> [BooleanFormula a] -> [BooleanFormula a]
forall a. [a] -> [a] -> [a]
++ [BooleanFormula a]
hyps } Clause a
r
            Or [LBooleanFormula a]
hyps'   -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
External instance of the constraint type Foldable []
all (\LBooleanFormula a
hyp' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go Clause a
l { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
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 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
Evidence bound by a type signature of the constraint type Uniquable a
memberClauseAtoms a
x Clause a
l -> Bool
True
                  | Bool
otherwise -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go Clause a
l (Clause a -> a -> Clause a
forall a. Uniquable a => Clause a -> a -> Clause a
Evidence bound by a type signature of the constraint type Uniquable a
extendClauseAtoms Clause a
r a
x) { clauseExprs :: [BooleanFormula a]
clauseExprs = [BooleanFormula a]
cons }
            Parens LBooleanFormula a
con' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go Clause a
l Clause a
r { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
con'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }
            And [LBooleanFormula a]
cons'   -> (LBooleanFormula a -> Bool) -> [LBooleanFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
External instance of the constraint type Foldable []
all (\LBooleanFormula a
con' -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
go Clause a
l Clause a
r { clauseExprs :: [BooleanFormula a]
clauseExprs = LBooleanFormula a -> BooleanFormula a
forall l e. GenLocated l e -> e
unLoc LBooleanFormula a
con'BooleanFormula a -> [BooleanFormula a] -> [BooleanFormula a]
forall a. a -> [a] -> [a]
:[BooleanFormula a]
cons }) [LBooleanFormula a]
cons'
            Or [LBooleanFormula a]
cons'    -> Clause a -> Clause a -> Bool
forall a. Uniquable a => Clause a -> Clause a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
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 l e. GenLocated l e -> e
unLoc [LBooleanFormula a]
cons' [BooleanFormula a] -> [BooleanFormula a] -> [BooleanFormula a]
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 {
        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 Clause a
c a
x = Clause a
c { clauseAtoms :: UniqSet a
clauseAtoms = UniqSet a -> a -> UniqSet a
forall a. Uniquable a => UniqSet a -> a -> UniqSet a
Evidence bound by a type signature of the constraint type Uniquable 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 a
x Clause a
c = a
x a -> UniqSet a -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
Evidence bound by a type signature of the constraint type Uniquable a
`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' 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
External instance of the constraint type forall a. Integral a => Ord (Ratio a)
External instance of the constraint type Integral Integer
> Rational
0) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
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
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 :: (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
External instance of the constraint type forall a. Integral a => Num (Ratio a)
External instance of the constraint type Integral Integer
External instance of the constraint type forall a. Integral a => Ord (Ratio a)
External instance of the constraint type Integral Integer
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
External instance of the constraint type forall a. Integral a => Num (Ratio a)
External instance of the constraint type Integral Integer
External instance of the constraint type forall a. Integral a => Ord (Ratio a)
External instance of the constraint type Integral Integer
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
Evidence bound by a type signature of the constraint type Ord a
> a
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  a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
Evidence bound by a type signature of the constraint type Ord a
> a
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
Evidence bound by a type signature of the constraint type Outputable a
pprVar Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
External instance of the constraint type forall a. Integral a => Num (Ratio a)
External instance of the constraint type Integral Integer
External instance of the constraint type forall a. Integral a => Ord (Ratio a)
External instance of the constraint type Integral Integer
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
External instance of the constraint type forall a. Integral a => Num (Ratio a)
External instance of the constraint type Integral Integer
External instance of the constraint type forall a. Integral a => Ord (Ratio a)
External instance of the constraint type Integral Integer
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
Evidence bound by a type signature of the constraint type Outputable a
ppr
  pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
Evidence bound by a type signature of the constraint type Ord a
> a
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' [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 ([SDoc] -> [SDoc]
forall a. [a] -> [a]
init [SDoc]
xs)) SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
", and" SDoc -> SDoc -> 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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
Evidence bound by a type signature of the constraint type Ord a
> a
1) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"either" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep (SDoc -> [SDoc] -> [SDoc]
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 = BooleanFormula a -> SDoc
forall a. OutputableBndr a => BooleanFormula a -> SDoc
Evidence bound by a type signature of the constraint type OutputableBndr a
pprBooleanFormulaNormal

pprBooleanFormulaNormal :: (OutputableBndr a)
                        => BooleanFormula a -> SDoc
pprBooleanFormulaNormal :: BooleanFormula a -> SDoc
pprBooleanFormulaNormal = BooleanFormula a -> SDoc
forall a. OutputableBndr a => BooleanFormula a -> SDoc
Evidence bound by a type signature of the constraint type OutputableBndr a
go
  where
    go :: BooleanFormula a -> SDoc
go (Var a
x)    = a -> SDoc
forall a. OutputableBndr a => a -> SDoc
Evidence bound by a type signature of the constraint type OutputableBndr a
pprPrefixOcc a
x
    go (And [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 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
text String
"FALSE"
    go (Or [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 l e. GenLocated l e -> e
unLoc) [LBooleanFormula a]
xs)
    go (Parens 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 -> 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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
External instance of the constraint type Monad IO
>> BinHandle -> a -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
Evidence bound by a type signature of the constraint type Binary a
put_ BinHandle
bh a
x
  put_ BinHandle
bh (And [LBooleanFormula a]
xs)   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
External instance of the constraint type Monad IO
>> BinHandle -> [LBooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
External instance of the constraint type forall a. Binary a => Binary [a]
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ BinHandle
bh (Or  [LBooleanFormula a]
xs)   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
External instance of the constraint type Monad IO
>> BinHandle -> [LBooleanFormula a] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
External instance of the constraint type forall a. Binary a => Binary [a]
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
put_ BinHandle
bh [LBooleanFormula a]
xs
  put_ BinHandle
bh (Parens LBooleanFormula a
x) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
3 IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
External instance of the constraint type Monad IO
>> BinHandle -> LBooleanFormula a -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
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 -> 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
External instance of the constraint type Functor IO
<$> BinHandle -> IO a
forall a. Binary a => BinHandle -> IO a
Evidence bound by a type signature of the constraint type Binary a
get BinHandle
bh
      Word8
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
External instance of the constraint type Functor IO
<$> BinHandle -> IO [LBooleanFormula a]
forall a. Binary a => BinHandle -> IO a
External instance of the constraint type forall a. Binary a => Binary [a]
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
get BinHandle
bh
      Word8
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
External instance of the constraint type Functor IO
<$> BinHandle -> IO [LBooleanFormula a]
forall a. Binary a => BinHandle -> IO a
External instance of the constraint type forall a. Binary a => Binary [a]
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
get BinHandle
bh
      Word8
_ -> 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
External instance of the constraint type Functor IO
<$> BinHandle -> IO (LBooleanFormula a)
forall a. Binary a => BinHandle -> IO a
External instance of the constraint type forall a. Binary a => Binary (Located a)
Instance of class: Binary of the constraint type forall a. Binary a => Binary (BooleanFormula a)
Evidence bound by a type signature of the constraint type Binary a
get BinHandle
bh