{-# OPTIONS_GHC -fglasgow-exts #-}

module Logic where

import Regular

data Logic = Var String
           | Logic :<->: Logic            -- equivalence
           | Logic :->:  Logic            -- implication
           | Logic :&&:  Logic            -- and (conjunction)
           | Logic :||:  Logic            -- or (disjunction)
           | Not Logic                    -- not
           | T                            -- true
           | F                            -- false
 deriving (Show, Eq, Ord)

data Var
data (:<->:)
data (:->:)
data (:&&:)
data (:||:)
data Not
data T
data F

instance Constructor Var where conName _ = "Var"
instance Constructor (:<->:) where conName _ = "(:<->:)"
instance Constructor (:->:) where conName _ = "(:->:)"
instance Constructor (:&&:) where conName _ = "(:&&:)"
instance Constructor (:||:) where conName _ = "(:||:)"
instance Constructor Not where conName _ = "Not"
instance Constructor T where conName _ = "T"
instance Constructor F where conName _ = "F"

type PFLogic =    C Var     (K String)
              :+: C (:<->:) (I :*: I)
              :+: C (:->:)  (I :*: I)
              :+: C (:&&:)  (I :*: I)
              :+: C (:||:)  (I :*: I)
              :+: C Not     I
              :+: C T       U
              :+: C F       U

instance Regular Logic where
  type PF Logic = PFLogic
  from (Var x)     = L (C (K x))
  from (p :<->: q) = R (L (C ((I p) :*: (I q))))
  from (p :->: q)  = R (R (L (C ((I p) :*: (I q)))))
  from (p :&&: q)  = R (R (R (L (C ((I p) :*: (I q))))))
  from (p :||: q)  = R (R (R (R (L (C ((I p) :*: (I q)))))))
  from (Not p)     = R (R (R (R (R (L (C (I p)))))))
  from T           = R (R (R (R (R (R (L (C U)))))))
  from F           = R (R (R (R (R (R (R (C U)))))))

  to (L (C (K x)))                             = Var x
  to (R (L (C ((I p) :*: (I q)))))             = p :<->: q
  to (R (R (L (C ((I p) :*: (I q))))))         = p :->: q
  to (R (R (R (L (C ((I p) :*: (I q)))))))     = p :&&: q
  to (R (R (R (R (L (C ((I p) :*: (I q)))))))) = p :||: q
  to (R (R (R (R (R (L (C (I p))))))))         = Not p
  to (R (R (R (R (R (R (L (C U))))))))         = T
  to (R (R (R (R (R (R (R (C U))))))))         = F