slightly better equation solver with support for conditionals, expression parsing, and pretty-printing. unfortunately very ugly

leqn.hs

{-# LANGUAGE DeriveFunctor #-}

import Text.ParserCombinators.Parsec
import Data.Functor.Foldable
import qualified Data.Set as S

data FormF a = Var Char
             | Not a
             | And a a
             | Or  a a
             | If  a a deriving Functor
type Form = Fix FormF

pset :: Ord a => S.Set a -> S.Set (S.Set a)
pset xs | S.null xs = S.singleton S.empty
        | otherwise = S.union xs' $ S.map (S.insert x) xs'
  where x   = S.findMin xs
        xs' = pset $ S.deleteMin xs

free :: Form -> S.Set Char
free = cata alg
  where alg (Var v)     = S.singleton v
        alg (Not e)     = e
        alg (And e1 e2) = e1 `S.union` e2
        alg (Or  e1 e2) = e1 `S.union` e2
        alg (If  e1 e2) = e1 `S.union` e2

sat :: S.Set Char -> Form -> Bool
sat s = cata alg
  where alg (Var v)     = v `S.member` s
        alg (Not e)     = not e
        alg (And e1 e2) = e1 && e2
        alg (Or  e1 e2) = e1 || e2
        alg (If  e1 e2) = not e1 || e2

solve :: Form -> S.Set (S.Set Char)
solve f = S.filter (flip sat f) . pset . free $ f

op  f = return . Fix . f
op2 f = return $ (Fix .) . f

var    = lower >>= op Var
parens = between (char '(') (char ')') expr
prim   = neg <|> var <|> parens
neg    = char '!' >> prim >>= op Not
conj   = chainl1 prim (char '&' >> op2 And)
disj   = chainl1 conj (char '|' >> op2 Or)
expr   = chainl1 disj (string "=>" >> op2 If)

main = getLine >>= print . compute >> main
  where compute s = case parse expr "" s of
                      Right x -> solve x
                      Left  y -> error $ show y