-- :load "C:\\HaskellProgs\\tautology_checker.hs" 

data Prop = Const Bool| Var Char | Not Prop | And Prop Prop | Imply Prop Prop
             deriving (Eq,Ord,Show,Read)
			 
p1 :: Prop
p1 = And (Var 'A') (Not (Var 'A'))

p2 :: Prop
p2 = Imply (And (Var 'A') (Var 'B')) (Var 'A')

p3 :: Prop
p3 = Imply (Var 'A') (And (Var 'A') (Var 'B'))

p4 :: Prop
p4 = Imply (And (Var 'A') (Imply (Var 'A') (Var 'B'))) (Var 'B')

------------------------------------------			 

type Subst = [(Char, Bool)]

eval :: Subst -> Prop -> Bool
eval _ (Const b) = b
eval s (Var x) = find x s
eval s (Not p) = not (eval s p)
eval s (And p q) = eval s p && eval s q
eval s (Imply p q) = eval s p <= eval s q


find x s = head [v| (y,v) <- s,x==y ]

vars :: Prop -> [Char ]
vars (Const _ ) = [ ]
vars (Var x) = [x ]
vars (Not p) = vars p
vars (And p q) = vars p ++ vars q
vars (Imply p q) = vars p ++ vars q

bools 0 = [[]]
bools (n+1) = let temp = bools n
               in
			   (distribute True temp) ++ (distribute False temp)
						   
distribute _ [] = []
distribute b (h:t) = (b:h):(distribute b t)

element x [] = False
element x (h:t) = x==h || (element x t)

rmdups [] = []
rmdups (h:t) | element h t = rmdups t
             | otherwise   = h:(rmdups t)
			 
			 
substs :: Prop -> [Subst ]
substs p = map (zip vs) (bools (length vs))
              where 
			     vs = rmdups (vars p)			 

isTaut :: Prop -> Bool
isTaut p = and [eval s p | s <- substs p ]