module Gen.Rules where

import Data.Maybe
import Common.Logic
import Common.GuardedRewriting


(|-) :: Logic -> Logic -> Template Logic
p |- q = p +-> q // True

makeRuleList _ = rewriteMl . map synthesise
makeRule s x = makeRuleList s [x]

--rewriteMl :: [Rule (Pat (PF Logic))] -> Logic -> [Logic]
rewriteMl rs p = take 1 $ catMaybes $ map (`rewriteM` p) rs

-- This main function is defined to solve a bug in GHC
main :: IO ()
main = do let resultsPP = zipWith undefined [1..] ([] :: [Logic])
          putStr (unlines resultsPP)   

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

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

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

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

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

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

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

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

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

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

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

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