{-# 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 Logic.Rules where

import qualified Data.Set as S
import Logic.Formula
import Representations
import Rewriting hiding (Var)

instance Rewrite Logic 

instance View Logic where
  type PF Logic =
     Sum (K String)   ( -- var
     Sum (Prod Id Id) ( -- implication
     Sum (Prod Id Id) ( -- equivalence
     Sum (Prod Id Id) ( -- and (conjunction)
     Sum (Prod Id Id) ( -- or (disjunction)
     Sum Id           ( -- not
     Sum Unit         ( -- true
         Unit)))))))    -- false

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

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

{- 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 :: [Rule1 Logic]
ruleComplOr = makeRuleList "ComplOr"
   [ \x -> (x :||: Not x)  |-  T
   , \x -> (Not x :||: x)  |-  T
   ]

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

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

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

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

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

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

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

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

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

ruleDeMorganAnd :: Rule2 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 :: Rule1 Logic
ruleNotNot = makeRule "NotNot" $ 
   \x -> (Not (Not x))  |-  x

ruleAndOverOr :: [Rule3 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 :: [Rule3 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 :: Rule1 Logic
ruleIdempOr = makeRule "IdempOr" $
    \x -> (x :||: x)  |-  x
   
    
ruleIdempAnd :: Rule1 Logic
ruleIdempAnd = makeRule "IdempAnd" $
    \x -> (x :&&: x)  |-  x
    
    
ruleAbsorpOr :: Rule2 Logic
ruleAbsorpOr = makeRule "AbsorpOr" $
    \x y -> (x :||: (x :&&: y))  |-  x
    
    
ruleAbsorpAnd :: Rule2 Logic
ruleAbsorpAnd = makeRule "AbsorpAnd" $
    \x y -> (x :&&: (x :||: y))  |-  x 
    
ruleCommOr :: Rule2 Logic
ruleCommOr = makeRule "CommOr" $
    \x y -> (x :||: y)  |-  (y :||: x) 
    
    
ruleCommAnd :: Rule2 Logic
ruleCommAnd = makeRule "CommAnd" $
    \x y -> (x :&&: y)  |-  (y :&&: x)
    

-- Buggy rules:

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

    
buggyRuleAssImp :: [Rule3 Logic]
buggyRuleAssImp = buggyRule $ makeRuleList "AssImp"
   [ \x y z -> (x :->: (y :->: z))  |-  ((x :->: y) :->: z)
   , \x y z -> ((x :->: y) :->: z)  |-  (x :->: (y :->: z))
   ]
    
buggyRuleIdemImp :: Rule1 Logic
buggyRuleIdemImp = buggyRule $ makeRule "IdemImp" $
    \x -> (x :->: x)  |-  x 
    
buggyRuleIdemEqui :: Rule1 Logic
buggyRuleIdemEqui = buggyRule $ makeRule "IdemEqui"  $
    \x -> (x :<->: x)  |-  x 
    
buggyRuleEquivElim :: [Rule2 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 :: Rule2 Logic
buggyRuleImplElim = buggyRule $ makeRule "BuggyImplElim" $
    \x y -> (x :->: y) |- Not (x :||: y) 
    
buggyRuleDeMorgan :: [Rule2 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 in both formulas!  
    ]
buggyRuleNotOverImpl :: Rule2 Logic
buggyRuleNotOverImpl = buggyRule $ makeRule "BuggyNotOverImpl" $
    \x y -> (Not(x :->: y)) |- (Not x :->: Not y)   
    
buggyRuleParenth :: [Rule2 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 :: [Rule3 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)
    ]