module Data.Boolean.BF
(
BF(..)
) where
import Data.Boolean
data BF = BFtrue
| BFfalse
| BFvar String
| BF `BFand` BF
| BF `BFor` BF
| BF `BFxor` BF
| BF `BFimplies` BF
| BF `BFiff` BF
| BFneg BF
| BFexists [BF] BF
| BFforall [BF] BF
| BFsubst [(BF, BF)] BF
deriving (Eq, Show)
instance BooleanVariable BF where
bvar = BFvar
unbvar (BFvar v) = v
unbvar _ = error $ "BF.unbvar: not a variable."
instance Boolean BF where
false = BFfalse
true = BFtrue
(/\) = BFand
(\/) = BFor
xor = BFxor
(-->) = BFimplies
(<->) = BFiff
neg = BFneg
instance QBF BF where
data Group BF = MkGroup { unMkGroup :: [BF] }
mkGroup = MkGroup
exists = BFexists . unMkGroup
forall = BFforall . unMkGroup
instance Substitution BF where
data Subst BF = MkBFpair [(BF, BF)]
mkSubst = MkBFpair
substitute (MkBFpair s) = BFsubst s