module PM.Rules where

import Common.Logic

ruleDefImpl (x :->: y) = [Not x :||: y]
ruleDefImpl _ = []

ruleDefEquiv (x :<->: y) = [(x :&&: y) :||: (Not x :&&: Not y)]
ruleDefEquiv _ = []
   
ruleFalseInEquiv (F :<->: x) = [Not x]
ruleFalseInEquiv (x :<->: F) = [Not x]
ruleFalseInEquiv _ = []

ruleTrueInEquiv (T :<->: x) = [x]
ruleTrueInEquiv (x :<->: T) = [x]
ruleTrueInEquiv _ = []

ruleFalseInImpl (F :->: x)  = [T]
ruleFalseInImpl (x :->: F)  = [Not x]
ruleFalseInImpl _ = []
 
ruleTrueInImpl (T :->: x) = [x]
ruleTrueInImpl (x :->: T) = [T]
ruleTrueInImpl _ = []
        
ruleFalseZeroOr (F :||: x) = [x]
ruleFalseZeroOr (x :||: F) = [x]
ruleFalseZeroOr _ = []

ruleTrueZeroOr (T :||: x) = [T]
ruleTrueZeroOr (x :||: T) = [T]
ruleTrueZeroOr _  = []

ruleTrueZeroAnd (T :&&: x) = [x]
ruleTrueZeroAnd (x :&&: T) = [x]
ruleTrueZeroAnd _ = []

ruleFalseZeroAnd (F :&&: x) = [F]
ruleFalseZeroAnd (x :&&: F) = [F]
ruleFalseZeroAnd _ = []

ruleDeMorganOr (Not (x :||: y)) = [Not x :&&: Not y]
ruleDeMorganOr _ = []

ruleDeMorganAnd (Not (x :&&: y))  = [ Not x :||: Not y ]
ruleDeMorganAnd _ = []

ruleNotBoolConst (Not T)  = [ F ]
ruleNotBoolConst (Not F)  = [ T ]
ruleNotBoolConst _ = []

ruleNotNot (Not (Not x)) = [x]
ruleNotNot _ = []

ruleAndOverOr (x :&&: (y :||: z))  = [ (x :&&: y) :||: (x :&&: z) ]
ruleAndOverOr ((x :||: y) :&&: z)  = [ (x :&&: z) :||: (y :&&: z) ]
ruleAndOverOr _ = []

ruleOrOverAnd (x :||: (y :&&: z))  =  [ (x :||: y) :&&: (x :||: z) ]
ruleOrOverAnd ((x :&&: y) :||: z)  =  [ (x :||: z) :&&: (y :||: z) ]
ruleOrOverAnd _ = []