{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

module Base where

import Generics.Regular.Rewriting


data Prop = T 
          | F 
          | Not Prop 
          | Prop :&&: Prop 
          | Prop :||: Prop 
          deriving (Eq, Show)

instance Regular Prop where
  type PF Prop = Unit :+: Unit :+: Id :+: Id :*: Id :+: Id :*: Id

  from T          = L Unit
  from F          = R (L Unit)
  from (Not p)    = R (R (L (Id p)))
  from (p :&&: q) = R (R (R (L (Id p :*: Id q))))
  from (p :||: q) = R (R (R (R (Id p :*: Id q))))

  to (L Unit)                        = T
  to (R (L Unit))                    = F
  to (R (R (L (Id p))))              = Not p
  to (R (R (R (L (Id p :*: Id q))))) = p :&&: q 
  to (R (R (R (R (Id p :*: Id q))))) = p :||: q

instance Rewrite Prop


notTRule :: RuleSpec Prop
notTRule = 
  Not T :~> F

notFRule :: RuleSpec Prop
notFRule = 
  Not F :~> T

andContrRule :: Prop -> RuleSpec Prop
andContrRule = 
  \p -> p :&&: Not p :~> F

orTautRule :: Prop -> RuleSpec Prop
orTautRule = 
  \p -> p :||: Not p :~> T

deMorganAndRule :: Prop -> Prop -> RuleSpec Prop
deMorganAndRule = 
  \p q -> Not (p :&&: q) :~> Not p :||: Not q

deMorganOrRule :: Prop -> Prop -> RuleSpec Prop
deMorganOrRule = 
  \p q -> Not (p :||: q) :~> Not p :&&: Not q

unboundRule :: Prop -> Prop -> RuleSpec Prop
unboundRule =
  \p q -> p :~> q

boundRule :: Prop -> RuleSpec Prop
boundRule =
  \p -> p :~> p

orFRule :: Prop -> RuleSpec Prop
orFRule = 
  \p -> p :||: F :~> p