{-# 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 in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
module LogicRules where

import qualified Data.Set as S
import Logic

import Representations
import Rules hiding (Var)


instance PFView Logic where
  type PF Logic =
     Sum (Sum (Sum (K String)   (Prod Id Id)) 
              (Sum (Prod Id Id) (Prod Id Id)))
         (Sum (Sum (Prod Id Id) Id) 
              (Sum Unit Unit))

  from (Var x)     = In (Inl (Inl (Inl (K x))))
  from (p :<->: q) = In (Inl (Inl (Inr (Prod (Id (from p)) (Id (from q))))))
  from (p :->: q)  = In (Inl (Inr (Inl (Prod (Id (from p)) (Id (from q))))))
  from (p :&&: q)  = In (Inl (Inr (Inr (Prod (Id (from p)) (Id (from q))))))
  from (p :||: q)  = In (Inr (Inl (Inl (Prod (Id (from p)) (Id (from q))))))
  from (Not p)     = In (Inr (Inl (Inr (Id (from p)))))
  from T           = In (Inr (Inr (Inl Unit)))
  from F           = In (Inr (Inr (Inr Unit)))

  to (In (Inl (Inl (Inl (K x))))) = Var x
  to (In (Inl (Inl (Inr (Prod (Id p) (Id q)))))) = to p :<->: to q
  to (In (Inl (Inr (Inl (Prod (Id p) (Id q)))))) = to p :->: to q
  to (In (Inl (Inr (Inr (Prod (Id p) (Id q)))))) = to p :&&: to q
  to (In (Inr (Inl (Inl (Prod (Id p) (Id q)))))) = to p :||: to q
  to (In (Inr (Inl (Inr (Id p))))) = Not (to p)
  to (In (Inr (Inr (Inl Unit)))) = T
  to (In (Inr (Inr (Inr Unit)))) = F

p |- q = p :~> q
makeRuleList _ = map rule
buggyRule = id
makeRule _ = rule

{- 
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] 
-}

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