module Uni.Rules where

import Common.Logic

x:y:z:_ = metaVars

(|-) :: Logic -> Logic -> (Logic -> [Logic]) 
(lhs |- rhs) a = case matchLogic lhs a of 
                    Just s  -> [s |-> rhs]
                    Nothing -> []

makeRuleList _ fs a = take 1 $ concatMap ($ a) fs
makeRule _ = id

ruleDefImpl = makeRule "DefImpl" $
   (x :->: y)  |-  (Not x :||: y)

ruleDefEquiv = makeRule "DefEquiv" $
   (x :<->: y)  |-  ((x :&&: y) :||: (Not x :&&: Not y))
   
ruleFalseInEquiv = makeRuleList "FalseInEquiv"
   [ (F :<->: x)  |-  (Not x)
   , (x :<->: F)  |-  (Not x)
   ]

ruleTrueInEquiv = makeRuleList "TrueInEquiv"
   [ (T :<->: x)  |-  x
   , (x :<->: T)  |-  x
   ]

ruleFalseInImpl = makeRuleList "FalseInImpl"
   [ (F :->: x)  |-  T
   , (x :->: F)  |- (Not x)
   ]
 
ruleTrueInImpl = makeRuleList "TrueInImpl"
   [  (T :->: x)  |-  x
   ,  (x :->: T)  |-  T
   ]
        
ruleFalseZeroOr = makeRuleList "FalseZeroOr"
   [ (F :||: x)  |-  x
   , (x :||: F)  |-  x
   ]
ruleTrueZeroOr = makeRuleList "TrueZeroOr"
   [ (T :||: x)  |-  T
   , (x :||: T)  |-  T
   ]

ruleTrueZeroAnd = makeRuleList "TrueZeroAnd"
   [ (T :&&: x)  |-  x
   , (x :&&: T)  |-  x
   ]

ruleFalseZeroAnd = makeRuleList "FalseZeroAnd"
   [ (F :&&: x)  |-  F
   , (x :&&: F)  |-  F
   ]

ruleDeMorganOr = makeRule "DeMorganOr" $
   (Not (x :||: y))  |-  (Not x :&&: Not y)

ruleDeMorganAnd = makeRule "DeMorganAnd" $
   (Not (x :&&: y))  |-  (Not x :||: Not y)

ruleNotBoolConst = makeRuleList "NotBoolConst"
   [ (Not T)  |-  F
   , (Not F)  |-  T
   ]

ruleNotNot = makeRule "NotNot" $ 
   (Not (Not x))  |-  x

ruleAndOverOr = makeRuleList "AndOverOr"
   [ (x :&&: (y :||: z))  |-  ((x :&&: y) :||: (x :&&: z))
   , ((x :||: y) :&&: z)  |-  ((x :&&: z) :||: (y :&&: z))
   ]

ruleOrOverAnd = makeRuleList "OrOverAnd"
   [ (x :||: (y :&&: z))  |-  ((x :||: y) :&&: (x :||: z))
   , ((x :&&: y) :||: z)  |-  ((x :||: z) :&&: (y :||: z))
   ]