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 _ = []