module Data.Logic.Classes.Combine
( Combinable(..)
, Combination(..)
, combine
, BinOp(..)
, binop
, (∧)
, (∨)
, (⇒)
, (⇔)
, (==>)
, (<=>)
, prettyBinOp
) where
import Data.Generics (Data, Typeable)
import Data.Logic.Classes.Negate (Negatable, (.~.))
import Data.Logic.Classes.Pretty (Pretty(pretty))
import Text.PrettyPrint (Doc, text)
class (Negatable formula) => Combinable formula where
(.|.) :: formula -> formula -> formula
(.&.) :: formula -> formula -> formula
x .&. y = (.~.) ((.~.) x .|. (.~.) y)
(.<=>.) :: formula -> formula -> formula
x .<=>. y = (x .=>. y) .&. (y .=>. x)
(.=>.) :: formula -> formula -> formula
x .=>. y = ((.~.) x .|. y)
(.<=.) :: formula -> formula -> formula
x .<=. y = y .=>. x
(.<~>.) :: formula -> formula -> formula
x .<~>. y = ((.~.) x .&. y) .|. (x .&. (.~.) y)
(.~|.) :: formula -> formula -> formula
x .~|. y = (.~.) (x .|. y)
(.~&.) :: formula -> formula -> formula
x .~&. y = (.~.) (x .&. y)
infixl 1 .<=>. , .<~>., ⇔, <=>
infixr 2 .=>., ⇒, ==>
infixr 3 .|., ∨
infixl 4 .&., ∧
data Combination formula
= BinOp formula BinOp formula
| (:~:) formula
deriving (Eq, Ord, Data, Typeable, Show, Read)
combine :: Combinable formula => Combination formula -> formula
combine (BinOp f1 (:<=>:) f2) = f1 .<=>. f2
combine (BinOp f1 (:=>:) f2) = f1 .=>. f2
combine (BinOp f1 (:&:) f2) = f1 .&. f2
combine (BinOp f1 (:|:) f2) = f1 .|. f2
combine ((:~:) f) = (.~.) f
data BinOp
= (:<=>:)
| (:=>:)
| (:&:)
| (:|:)
deriving (Eq, Ord, Data, Typeable, Enum, Bounded, Show, Read)
binop :: Combinable formula => formula -> BinOp -> formula -> formula
binop a (:&:) b = a .&. b
binop a (:|:) b = a .|. b
binop a (:=>:) b = a .=>. b
binop a (:<=>:) b = a .<=>. b
(∧) :: Combinable formula => formula -> formula -> formula
(∧) = (.&.)
(∨) :: Combinable formula => formula -> formula -> formula
(∨) = (.|.)
(⇒) :: Combinable formula => formula -> formula -> formula
(⇒) = (.=>.)
(⇔) :: Combinable formula => formula -> formula -> formula
(⇔) = (.<=>.)
(==>) :: Combinable formula => formula -> formula -> formula
(==>) = (.=>.)
(<=>) :: Combinable formula => formula -> formula -> formula
(<=>) = (.<=>.)
prettyBinOp :: BinOp -> Doc
prettyBinOp (:<=>:) = text "⇔"
prettyBinOp (:=>:) = text "⇒"
prettyBinOp (:&:) = text "∧"
prettyBinOp (:|:) = text "∨"
instance Pretty BinOp where
pretty = prettyBinOp