module ApplyRule where

import Test.QuickCheck

import Generics.Regular.Rewriting

import Base


applyRuleTests = 
  [ notTRuleTest1, notTRuleTest2
  , notFRuleTest1, notFRuleTest2
  , andContrRuleTest1, andContrRuleTest2
  , orTautRuleTest1, orTautRuleTest2 
  , deMorganAndRuleTest1, deMorganAndRuleTest2
  , deMorganOrRuleTest1, deMorganOrRuleTest2
  ]


notTRuleTest1 = 
  label "notTRule" $ 
  applyRule notTRule (Not T) == F

notTRuleTest2 = 
  label "notTRule" $ 
  applyRule notTRule (Not F) == Not F

notFRuleTest1 = 
  label "notFRule" $ 
  applyRule notFRule (Not F) == T

notFRuleTest2 = 
  label "notFRule" $ 
  applyRule notFRule (Not T) == Not T

andContrRuleTest1 = 
  label "andContrRule" $ 
  applyRule andContrRule (T :&&: (Not T)) == F

andContrRuleTest2 = 
  label "andContrRule" $ 
  applyRule andContrRule (T :&&: (Not F)) == T :&&: (Not F)

orTautRuleTest1 = 
  label "orTautRule" $ 
  applyRule orTautRule (T :||: (Not T)) == T

orTautRuleTest2 = 
  label "orTautRule" $ 
  applyRule orTautRule (T :||: (Not F)) == T :||: (Not F)

deMorganAndRuleTest1 = 
  label "deMorganAndRule" $ 
  applyRule deMorganAndRule (Not (T :&&: F)) == Not T :||: Not F

deMorganAndRuleTest2 = 
  label "deMorganAndRule" $ 
  applyRule deMorganAndRule (Not (T :||: F)) == Not (T :||: F)

deMorganOrRuleTest1 = 
  label "deMorganOrRule" $ 
  applyRule deMorganOrRule (Not (T :||: F)) == Not T :&&: Not F

deMorganOrRuleTest2 = 
  label "deMorganOrRule" $ 
  applyRule deMorganOrRule (Not (T :&&: F)) == Not (T :&&: F)