{-# OPTIONS -fglasgow-exts #-}
-----------------------------------------------------------------------------
-- Copyright 2008, Open Universiteit Nederland. This file is distributed 
-- under the terms of the GNU General Public License. For more information, 
-- see the file "LICENSE.txt", which is included the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
module Common.LogicRules where

import qualified Data.Set as S
import Common.Logic
import Common.GuardedRewriting


p |- q = p +-> q
makeRuleList _ = map synthesise
buggyRule = id
makeRule _ = synthesise

{- logicRules :: [LogicRule]
logicRules = [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd, ruleFalseZeroAnd, ruleDeMorganOr, ruleDeMorganAnd
             , ruleNotBoolConst, ruleNotNot, ruleAndOverOr, ruleOrOverAnd
             , ruleDefImpl, ruleDefEquiv
             , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
	     , ruleComplOr, ruleComplAnd
	     , ruleIdempOr, ruleIdempAnd
	     , ruleAbsorpOr, ruleAbsorpAnd
	     , ruleCommOr, ruleCommAnd
             ] 

logicBuggyRules :: [LogicRule]
logicBuggyRules = [ buggyRuleCommImp, buggyRuleAssImp
                  ] -}
                  
ruleComplOr :: [Rule Logic]
ruleComplOr = makeRuleList "ComplOr"
   [ \x -> (x :||: Not x)  |-  T
   , \x -> (Not x :||: x)  |-  T
   ]

ruleComplAnd :: [Rule Logic]
ruleComplAnd = makeRuleList "ComplAnd"
   [ \x -> (x :&&: Not x)  |-  F
   , \x -> (Not x :&&: x)  |-  F
   ]

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

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

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

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

ruleTrueZeroOr :: [Rule Logic]
ruleTrueZeroOr = makeRuleList "TrueZeroOr"
   [ \x -> (T :||: x)  |-  T
   , \x -> (x :||: T)  |-  T
   ]

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

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

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

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

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

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

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

ruleOrOverAnd :: [Rule Logic]
ruleOrOverAnd = makeRuleList "OrOverAnd"
   [ \x y z -> (x :||: (y :&&: z))  |-  ((x :||: y) :&&: (x :||: z))
   , \x y z -> ((x :&&: y) :||: z)  |-  ((x :||: z) :&&: (y :||: z))
   ]
 
ruleIdempOr :: Rule Logic
ruleIdempOr = makeRule "IdempOr" $
    \x -> (x :||: x)  |-  x
   
    
ruleIdempAnd :: Rule Logic
ruleIdempAnd = makeRule "IdempAnd" $
    \x -> (x :&&: x)  |-  x
    
    
ruleAbsorpOr :: Rule Logic
ruleAbsorpOr = makeRule "AbsorpOr" $
    \x y -> (x :||: (x :&&: y))  |-  x
    
    
ruleAbsorpAnd :: Rule Logic
ruleAbsorpAnd = makeRule "AbsorpAnd" $
    \x y -> (x :&&: (x :||: y))  |-  x 
    
ruleCommOr :: Rule Logic
ruleCommOr = makeRule "CommOr" $
    \x y -> (x :||: y)  |-  (y :||: x) 
    
    
ruleCommAnd :: Rule Logic
ruleCommAnd = makeRule "CommAnd" $
    \x y -> (x :&&: y)  |-  (y :&&: x)
    

-- Buggy rules:

buggyRuleCommImp :: Rule Logic
buggyRuleCommImp = buggyRule $ makeRule "CommImp" $
    \x y -> (x :->: y)  |-  (y :->: x) --this does not hold: T->T => T->x

    
buggyRuleAssImp :: [Rule Logic]
buggyRuleAssImp = buggyRule $ makeRuleList "AssImp"
   [ \x y z -> (x :->: (y :->: z))  |-  ((x :->: y) :->: z)
   , \x y z -> ((x :->: y) :->: z)  |-  (x :->: (y :->: z))
   ]
    
buggyRuleIdemImp :: Rule Logic
buggyRuleIdemImp = buggyRule $ makeRule "IdemImp" $
    \x -> (x :->: x)  |-  x 
    
buggyRuleIdemEqui :: Rule Logic
buggyRuleIdemEqui = buggyRule $ makeRule "IdemEqui"  $
    \x -> (x :<->: x)  |-  x 
    
buggyRuleEquivElim :: [Rule Logic]
buggyRuleEquivElim = buggyRule $ makeRuleList "BuggyEquivElim"
    [ \x y -> (x :<->: y) |- ((x :&&: y) :||: Not (x :&&: y))
    , \x y -> (x :<->: y) |- ((x :||: y) :&&: (Not x :||: Not y))
    , \x y -> (x :<->: y) |- ((x :&&: y) :||: (Not x :&&:  y))
    , \x y -> (x :<->: y) |- ((x :&&: y) :||: ( x :&&: Not y))
    , \x y -> (x :<->: y) |- ((x :&&: y) :&&: (Not x :&&: Not y))
    ]
    
buggyRuleImplElim :: Rule Logic
buggyRuleImplElim = buggyRule $ makeRule "BuggyImplElim" $
    \x y -> (x :->: y) |- Not (x :||: y) 
    
buggyRuleDeMorgan :: [Rule Logic]
buggyRuleDeMorgan = buggyRule $ makeRuleList "BuggyDeMorgan"
    [ \x y -> (Not (x :&&: y)) |-  (Not x :||: y)
    , \x y -> (Not (x :&&: y)) |-  (x :||: Not y)
    , \x y -> (Not (x :&&: y)) |- (Not (Not x :||: Not y))
    , \x y -> (Not (x :||: y)) |-  (Not x :&&: y)
    , \x y -> (Not (x :||: y)) |-  (x :&&: Not y)
    , \x y -> (Not (x :||: y)) |- (Not (Not x :&&: Not y)) --note the firstNot both formulas!  
    ]
buggyRuleNotOverImpl :: Rule Logic
buggyRuleNotOverImpl = buggyRule $ makeRule "BuggyNotOverImpl" $
    \x y -> (Not(x :->: y)) |- (Not x :->: Not y)   
    
buggyRuleParenth :: [Rule Logic]
buggyRuleParenth = buggyRule $ makeRuleList "BuggyParenth"
    [ \x y -> (Not (x :&&: y)) |-  (Not x :&&: y)
    , \x y -> (Not (x :||: y)) |-  (Not x :||: y)
    , \x y -> (Not (x :<->: y)) |- (Not(x :&&: y) :||: (Not x :&&: Not y))
    , \x y -> (Not(Not x :&&: y)) |- (x :&&: y) 
    , \x y -> (Not(Not x :||: y)) |- (x :||: y)
    , \x y -> (Not(Not x :->: y)) |- (x :->: y)
    , \x y -> (Not(Not x :<->: y)) |- (x :<->: y)
    ]
    
buggyRuleAssoc :: [Rule Logic]
buggyRuleAssoc = buggyRule $ makeRuleList "BuggyAssoc"
    [ \x y z -> (x :||: (y :&&: z)) |- ((x :||: y) :&&: z)
    , \x y z -> ((x :||: y) :&&: z) |- (x :||: (y :&&: z))
    , \x y z -> ((x :&&: y) :||: z) |- (x :&&: (y :||: z))
    , \x y z -> (x :&&: (y :||: z)) |- ((x :&&: y) :||: z)
    ]