module Data.Logic.Types.Harrison.Formulas.Propositional
( Formula(..)
) where
import Data.Logic.Classes.Constants (Constants(..))
import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..))
import qualified Data.Logic.Classes.Formula as C
import Data.Logic.Classes.Literal (Literal(..))
import Data.Logic.Classes.Negate (Negatable(..))
import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..), topFixity)
import Data.Logic.Classes.Propositional (PropositionalFormula(..), prettyPropositional, fixityPropositional, foldAtomsPropositional, mapAtomsPropositional)
data Formula a
= F
| T
| Atom a
| Not (Formula a)
| And (Formula a) (Formula a)
| Or (Formula a) (Formula a)
| Imp (Formula a) (Formula a)
| Iff (Formula a) (Formula a)
deriving (Eq, Ord)
instance Negatable (Formula atom) where
negatePrivate T = F
negatePrivate F = T
negatePrivate x = Not x
foldNegation normal inverted (Not x) = foldNegation inverted normal x
foldNegation normal _ x = normal x
instance Constants (Formula a) where
fromBool True = T
fromBool False = F
asBool T = Just True
asBool F = Just False
asBool _ = Nothing
instance Combinable (Formula a) where
a .<=>. b = Iff a b
a .=>. b = Imp a b
a .|. b = Or a b
a .&. b = And a b
instance (Pretty atom, HasFixity atom, Ord atom) => C.Formula (Formula atom) atom where
atomic = Atom
foldAtoms = foldAtomsPropositional
mapAtoms = mapAtomsPropositional
instance (Combinable (Formula atom), Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom where
foldPropositional co tf at formula =
case formula of
T -> tf True
F -> tf False
Not f -> co ((:~:) f)
And f g -> co (BinOp f (:&:) g)
Or f g -> co (BinOp f (:|:) g)
Imp f g -> co (BinOp f (:=>:) g)
Iff f g -> co (BinOp f (:<=>:) g)
Atom x -> at x
instance (HasFixity atom, Pretty atom, Ord atom) => Literal (Formula atom) atom where
foldLiteral neg tf at formula =
case formula of
T -> tf True
F -> tf False
Not f -> neg f
Atom x -> at x
_ -> error ("Unexpected literal " ++ show (pretty formula))
instance (Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom) where
pretty = prettyPropositional pretty topFixity
instance (Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom) where
fixity = fixityPropositional