TautologyCheckerHaskell

import Data.List (nub) -- The function 'nub' removes duplicates from a list

data Prop = Const Bool
          | Var Char
          | Not Prop
          | And Prop Prop
          | Imply Prop Prop
          | Or Prop Prop
          | Equiv Prop Prop
  deriving (Show)

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

find :: (Eq k) => k -> Assoc k v -> v
find k [] = error "Key not found!"
find k ((k',x):xs)
  | k == k'   = x
  | otherwise = find k xs

type Subst = Assoc 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
eval s (Or p q) = eval s p || eval s q
eval s (Equiv p q) = eval s p == eval s q

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
vars (Or p q) = vars p ++ vars q
vars (Equiv p q) = vars p ++ vars q


bools :: Int -> [[Bool]]
bools 0       = [[]]
bools n | n>0 = map (False:) bss ++ map (True:) bss
  where bss = bools (n-1)

substs :: Prop -> [Subst]
substs p = map (zip vs) (bools (length vs))
  where vs = nub (vars p)

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


isSat :: Prop -> Maybe Subst
isSat p = if maybe then Just (head [s | s <- substs p, eval s p]) else Nothing
  where maybe =  or [eval s p | s <- substs p]