Boolean expression optimizer.

optimize.hs

import Data.Char

data Expr
  = Nand Expr Expr
  | And Expr Expr
  | Or Expr Expr
  | Not Expr
  | Input Int
  deriving (Eq)

instance Show Expr where
  show (Input n)  = [chr $ 64 + n]
  show (Not e)    = '!' : show e
  show (Or a b)   = "(" ++ show a ++ " | " ++ show b ++ ")"
  show (And a b)  = "(" ++ show a ++ " & " ++ show b ++ ")"
  show (Nand a b) = show (Not $ And a b)

expl :: Expr -> Expr
expl (And x y) =
  let z = Nand (expl x) (expl y)
  in Nand z z
expl (Or x y)  =
  let x' = expl x
      y' = expl y
  in Nand (Nand x' x') (Nand y' y')
expl (Not x)   =
  let x' = expl x
  in Nand x' x'
expl e         = e

optimize :: Expr -> Expr
optimize (Nand x@(Input _) y@(Nand _ _)) = Nand x (optimize y)
optimize (Nand x@(Nand _ _) y@(Input _)) = Nand (optimize x) y
optimize e@(Nand x@(Input _) y@(Input _))
  | x == y    = Not x
  | otherwise = e
optimize (Nand x y) =
  let pullor e'@(Or a'' b'') f'@(Or c'' d'')
        | a'' == c'' = Or a'' (And b'' d'')
        | a'' == d'' = Or a'' (And b'' c'')
        | b'' == c'' = Or b'' (And a'' d'')
        | b'' == d'' = Or b'' (And a'' c'')
        | otherwise  = And e' f'
      pullor e' f' = And e' f'
      optimize' x'@(Nand a b) y'@(Nand c d)
        | x' == y'         =
          let optnot (Not n')     = n'
              optnot (Nand a' b') = pullor a' b'
              optnot n'           = Not n'
          in optnot (optimize x')
        | a == b && c == d =
          let optor
                | a == c    = optimize a
                | otherwise =
                    let expnot g f h i
                          | g == h    = Or g i
                          | g == i    = Or g h
                          | otherwise = Or g f
                        pullnot e f@(And (Not a'') b'') = expnot e f a'' b''
                        pullnot f@(And (Not a'') b'') e = expnot e f a'' b''
                        pullnot e f                     = Or e f
                        optfac g f h i
                          | g `elem` [h, i] = g
                          | otherwise       = pullnot g f
                        redor e f@(And a'' b'')         = optfac e f a'' b''
                        redor f@(And a'' b'') e         = optfac e f a'' b''
                        redor (Not a'') (Not b'')       = Not $ And a'' b''
                        redor e f                       = Or e f
                    in redor (optimize a) (optimize c)
          in optor
        | otherwise        =
          let redand
                | a == c && b == d = optand (optimize a) (optimize b)
                | a == d && b == c = optand (optimize a) (optimize b)
                | otherwise        = Nand (optimize x') (optimize y')
              optand x'' y''
                | x'' == y'' = optimize x''
                | otherwise  = pullor x'' y''
          in redand
      optimize' x' y' = Nand (optimize x') (optimize y')
  in optimize' x y
optimize e = e

main :: IO ()
main =
  let before = And (Or (Input 2) (Input 3)) (Not (Or (Input 1) (And (Not (Input 1)) (Input 2))))
      mash   = expl before
      after  = optimize mash
  in putStrLn "Before:"  >> print before
  >> putStrLn "\nMash:"  >> print mash
  >> putStrLn "\nAfter:" >> print after