Tautology prover.

import Data.List

type ID = String
type Env = [(ID,Bool)]
data Exp = T | F | Var ID | Not Exp | Exp :+: Exp | Exp :*: Exp
    deriving (Eq)


eval :: Env -> Exp -> Bool
eval env T = True
eval env F = False
eval env (Var x) | Just b <- lookup x env = b
eval env (Not e) = not (eval env e)
eval env (e1 :+: e2) = (eval env e1) || (eval env e2)
eval env (e1 :*: e2) = (eval env e1) && (eval env e2)


vars :: Exp -> [ID]
vars e = nub (go e [])
  where
    go (Var x) acc = x : acc
    go (Not e) acc = go e acc
    go (e1 :+: e2) acc = go e2 (go e1 acc)
    go (e1 :*: e2) acc = go e2 (go e1 acc)
    go _ acc = acc


envs :: [ID] -> [Env]
envs []  = []
envs [x] = [ [(x,False)], [(x,True)] ]
envs (x:xs) = [ (x,False) : env | env <- es ] ++ [ (x,True) : env | env <- es ]
  where es = envs xs


exhaust :: Exp -> [(Bool,Env)]
exhaust e = [ (eval env e, env) | env <- envs . vars $ e ]

showEnvs :: [Env] -> String
showEnvs = glue "\n" . map (glue ", " . map showVar)
  where showVar (x,b) = x ++ "=" ++ show (fromEnum b)
        glue s = concat . intersperse s

isTautology :: Exp -> String
isTautology e =
  case exhaust e of
    [] -> if eval [] e then "OK" else "FAIL"
    xs -> case filter (not . fst) xs of
            [] -> "OK"
            xs -> "FAIL for these environments:\n" ++ showEnvs (map snd xs)


(==>) :: Exp -> Exp -> Exp
e1 ==> e2 = Not (e1 :*: (Not e2))

(<=>) :: Exp -> Exp -> Exp
e1 <=> e2 = (e1 :*: e2) :+: (Not e1 :*: Not e2)

test = ((Var "p" :*: Var "r") :+: (Var "q" :*: Var "s"))
   ==> ((Var "p" :+: Var "q") :*: (Var "r" :+: Var "s"))

main = putStrLn $ isTautology test