Boolean formula validator

validN.hs

cartprod :: [[x]] -> [[x]]
cartprod [] = [[]]
cartprod (xs:xss) = [ x:s | x <- xs, s <- cartprod xss ]


data Env a = Env [(String, a)] deriving Show

get :: Env a -> String -> a
get (Env ((var, val):t)) v | v == var  = val
                           | otherwise = get (Env t) v
                                         
data Binop = And | Or | Implies deriving (Eq, Show)
data Unop = Not deriving (Eq, Show)

data Formula = Var [Char] | Con Bool
             | Exp2 Binop Formula Formula
             | Exp1 Unop Formula
               deriving (Eq, Show)

vars :: Formula -> [String]
vars f = uniq $ vars' f
         where
           vars' (Con _) = []
           vars' (Var x) = [x]
           vars' (Exp1 _ f) = vars' f
           vars' (Exp2 _ f1 f2) = (++) (vars' f1) (vars' f2)

remove :: Eq x => x -> [x] -> [x]
remove _ [] = []
remove x (h:t) | x == h    = remove x t
               | otherwise = h : remove x t

uniq :: Eq x => [x] -> [x]
uniq [] = []
uniq (h:t) = h : uniq (remove h t)

(<|>) = Exp2 Or
(<&>) = Exp2 And
n = Exp1 Not
a `to` b = n a <|> b

infix 2 <|> 
infix 3 <&> 

a = Var "a"
b = Var "b"
c = Var "c"

f = (a <&> b) <|> (n a <&> n b)
k = a `to` (b `to` a)

index _ [] = undefined
index e ls = index' 0 e ls
  where
    index' n e (h:t) | e == h     = n
                     | otherwise  = index' (n+1) e t

toEnv :: [String] -> [a] -> Env a
-- toEnv vars vals = Env $ (\v -> vals !! index v vars)
toEnv vars vals  = Env $ zip vars vals

allEnvs :: Formula -> [Env Bool]
allEnvs formula = [ toEnv (vars formula) vals | vals <-
                       cartprod (take nvars (repeat [True, False])) ]
  where nvars = length $ vars formula

ev :: Env Bool -> Formula -> Bool
ev env (Var s) = get env s
ev env (Con b) = b
ev env (Exp1 Not f) = not $ ev env f
ev env (Exp2 And f g) = (ev env f) && (ev env g)
ev env (Exp2 Or f g)  = (ev env f) || (ev env g)
  
allVals f = [ ev env f | env <- allEnvs f ]

isValid f = and $ allVals f

t = a <|> n a

listMaybe :: [a] -> Maybe a
listMaybe [] = Nothing
listMaybe (x:_) = Just x

firstWhere f  = listMaybe . (filter f)

falsify f = firstWhere (\env -> ev env f == False) $ allEnvs f