data Prop  = Const Bool | Var Char | Not Prop | And Prop Prop | Or Prop Prop | Imp Prop Prop

type Assoc k v = [(k, v)]

find :: (Eq k) => Assoc k v -> k -> v
find a k = head [v | (k',v) <- a, k == k']

type Subst = Assoc Char Bool

vars :: Prop -> [Char]
vars (Const b) = []
vars (Var x) = [x]
vars (Not p) = vars p
vars (And p q) = vars p ++ vars q
vars (Or p q) = vars p ++ vars q
vars (Imp p q) = vars p ++ vars q

uniq :: (Eq a) => [a] -> [a]
uniq [] = []
uniq (x:xs) = [x] ++ uniq (filter ( /= x) xs) -- (filter (\e -> e /= x) xs)

table :: Int -> [[Bool]]
table 0 = [[]]
table n = map (False:) t ++ map (True:) t -- map (0:) t ++ map (1:) t
          where t = table (n - 1)

subst :: Prop -> [Subst]
subst p =map (zip vs) (table (length vs))
         where vs = uniq $ vars p

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

isTaut :: Prop -> Bool
isTaut p = and [eval s p | s <- substs p] -- foldr (&&) True []

isAntiTaut :: Prop -> Bool
isAntiTaut p = isTaut (not p)


isAntiTaut' :: Prop -> Bool
isAntiTaut' p = and [not eval s p | s <- substs p]

p1 :: Prop
p1 = Imp (And (Var 'A') (Var 'B')) (Var 'A')

p2 :: Prop
p2 = Imp (Var 'A') (Var 'B')

main :: IO()
main = do print $ isTaut p2
          print $ isTaut p1