module LOGIC 
where

infix 1 ==>

(==>) :: Bool -> Bool -> Bool
x ==> y = (not x) || y

infix 1 <=>

(<=>) :: Bool -> Bool -> Bool
x <=> y = x == y 

infixr 2 <+>

(<+>) :: Bool -> Bool -> Bool
x <+> y = x /= y 

p = True
q = False

truthTable :: (Bool -> Bool -> Bool) -> [Bool]
truthTable wff = [ (wff p q) | p <- [True,False],
                               q <- [True,False]]

tt = (\ p q -> not (p ==> q))

satisfiable1 :: (Bool -> Bool) -> Bool
satisfiable1 wff = (wff True) || (wff False)

satisfiable2 :: (Bool -> Bool -> Bool)  -> Bool
satisfiable2 wff = or [ (wff p q) | p <- [True,False],
                                                     q <- [True,False]]

satisfiable3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
satisfiable3 wff = or [ (wff p q r) | p <- [True,False], 
                                                       q <-  [True,False],   
                                                        r  <-  [True,False]] 

s1 = ( \ p -> not p)
s2 = ( \ p q -> (not p) || (not q) )
s3 = ( \ p q r -> (not p) || (not q) && (not r) )

valid1 :: (Bool -> Bool) -> Bool
valid1 bf =  (bf True) && (bf False)

valid2 :: (Bool -> Bool -> Bool) -> Bool
valid2 bf = and [ bf r s| r <- [True,False], 
                           s <- [True,False]] 

v1 = ( \ p -> p || not p )    -- Excluded Middle
v2 = ( \ p -> p ==> p )
v3 = ( \ p q -> p ==> (q ==> p) )
v4 = ( \ p q -> (p ==> q) ==> p )

contradiction1 :: (Bool -> Bool) -> Bool
contradiction1 wff =  not (wff True) && not (wff False)

contradiction2 :: (Bool -> Bool -> Bool)  -> Bool
contradiction2 wff = and [not (wff p q) | p <- [True,False],
                                                                 q <- [True,False]]

contradiction3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
contradiction3 wff = and [ not (wff p q r) | p <- [True,False], 
                                                                    q <-  [True,False],   
                                                                    r  <-  [True,False]] 

c1 = ( \ p -> p && not p)
c2 = ( \ p q -> (p && not p) || (q && not q) )
c3 = ( \ p q r -> (p && not p) || (q && not q) && (r && not r) )

truth1 :: (Bool -> Bool) -> Bool
truth1 wff =  (wff True)

truth2 :: (Bool -> Bool -> Bool)  -> Bool
truth2 wff =   (wff True  True)

t1 = ( \ p -> not p)
t2 = ( \ p q -> (p && q) ||  (not p ==> q))
t3 = ( \ p q -> not p ==> q)
t4 = ( \ p q -> (not p && q) && (not p ==> q) )



logEquiv1 ::  (Bool -> Bool) -> (Bool -> Bool) -> Bool
logEquiv1 bf1 bf2 =  
    (bf1 True  <=> bf2 True) && (bf1 False <=> bf2 False) 

logEquiv2 :: (Bool -> Bool -> Bool) -> 
                    (Bool -> Bool -> Bool) -> Bool
logEquiv2 bf1 bf2 = 
  and [(bf1 p q) <=> (bf2 p q)  |  p <- [True,False], 
                                   q <- [True,False]]

logEquiv3 :: (Bool -> Bool -> Bool -> Bool) ->
                 (Bool -> Bool -> Bool -> Bool) -> Bool
logEquiv3 bf1 bf2 = 
  and [(bf1 p q r) <=> (bf2 p q r) |  p <- [True,False], 
                                      q <- [True,False], 
                                      r <- [True,False]] 

formula3 p q = p 
formula4 p q = (p <+> q) <+> q

formula5 p q = p <=> ((p <+> q) <+> q)

test1  = logEquiv1 id (\ p -> not (not p))
test2a = logEquiv1 id (\ p -> p && p) 
test2b = logEquiv1 id (\ p -> p || p) 
test3a = logEquiv2 (\ p q -> p ==> q) (\ p q -> not p || q)
test3b = logEquiv2 (\ p q -> not (p ==> q)) (\ p q -> p && not q)
test4a = logEquiv2 (\ p q -> not p ==> not q) (\ p q -> q ==> p)
test4b = logEquiv2 (\ p q -> p ==> not q) (\ p q -> q ==> not p)
test4c = logEquiv2 (\ p q -> not p ==> q) (\ p q -> not q ==> p)
test5a = logEquiv2 (\ p q -> p <=> q) 
                   (\ p q -> (p ==> q) && (q ==> p))
test5b = logEquiv2 (\ p q -> p <=> q) 
                   (\ p q -> (p && q) || (not p && not q))
test6a = logEquiv2 (\ p q -> p && q) (\ p q -> q && p)
test6b = logEquiv2 (\ p q -> p || q) (\ p q -> q || p)
test7a = logEquiv2 (\ p q -> not (p && q)) 
                   (\ p q -> not p || not q)
test7b = logEquiv2 (\ p q -> not (p || q)) 
                   (\ p q -> not p && not q)
test8a = logEquiv3 (\ p q r -> p && (q && r)) 
                   (\ p q r -> (p && q) && r)
test8b = logEquiv3 (\ p q r -> p || (q || r)) 
                   (\ p q r -> (p || q) || r)
test9a = logEquiv3 (\ p q r -> p && (q || r)) 
                   (\ p q r -> (p && q) || (p && r))
test9b = logEquiv3 (\ p q r ->  p || (q && r)) 
                   (\ p q r -> (p || q) && (p || r))

-- any, all :: (a->Bool) -> [a] -> Bool
-- any p = or . map p
-- all p = and . map p

every, some :: [a] -> (a -> Bool) -> Bool
every xs p = all p xs 
some  xs p = any p xs