Cleanup hopcroft

2 files changed, 250 insertions, 318 deletions

diff --git a/src/Lib.hs b/src/Lib.hs
index 0e093e3..7bd27d2 100644
--- a/src/Lib.hs
+++ b/src/Lib.hs
@@ -1,88 +1,85 @@
 {-# LANGUAGE TupleSections #-}
-{-# LANGUAGE BangPatterns #-}
 
 module Lib where
 
-import           Data.Char                      ( chr
-                                                , ord
-                                                )
-import qualified Data.List                     as L
-import qualified Data.Map                      as M
-import           Data.Maybe                     ( fromJust )
-import qualified Data.Set                      as S
-import           Debug.Trace                    ( traceShowId
-                                                , traceShow
-                                                )
-import           Parser
-import qualified Text.Parsec                   as Parsec
+import qualified Data.List as L
+import qualified Data.Map as M
+import Data.Maybe (fromJust)
+import qualified Data.Set as S
+import Parser
+  ( Addend (..),
+    Matrix (..),
+    QN (Neg, Qua),
+    QNMFormula (..),
+    Quantifier (Exists, ForAll),
+  )
 
 mget :: (Ord a) => a -> M.Map a b -> b
 mget a m = fromJust $ M.lookup a m
 
 automatizem :: M.Map Addend Int -> Matrix -> DFA [Int] Int
 automatizem dir (MEq as bs) =
-  eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
-automatizem dir (MLe  a b) = le (mget a dir) (mget b dir)
-automatizem dir (MLt  a b) = lt (mget a dir) (mget b dir)
+  eq (length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
+automatizem dir (MLe a b) = le (mget a dir) (mget b dir)
+automatizem dir (MLt a b) = lt (mget a dir) (mget b dir)
 automatizem dir (MAnd x y) = conj (automatizem dir x) (automatizem dir y)
-automatizem dir (MOr  x y) = disj (automatizem dir x) (automatizem dir y)
-automatizem dir (MNot x  ) = compl (automatizem dir x)
+automatizem dir (MOr x y) = disj (automatizem dir x) (automatizem dir y)
+automatizem dir (MNot x) = compl (automatizem dir x)
 
 automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int
 automatize dir (QNMFormula [] m) =
-  let dfa@( DFA s  _ _ _) = automatizem dir m
-      mdfa@(DFA s' _ _ _) = rmdist dfa (fromIntegral (length dir))
-      !t                  = (traceShowId $ (length s, length s'))
-  in  minimize (fromIntegral $ length dir) $ nondeterminize $ mdfa
+  let dfa = automatizem dir m
+      mdfa = minDistinguishability dfa (length dir)
+   in minReachability (length dir) $ nondeterminize mdfa
 automatize dir (QNMFormula (Neg : quas) m) =
   let nfa = automatize dir (QNMFormula quas m)
-  in  minimize (fromIntegral (length dir)) (ncompl nfa)
- where
-  rmmin d = rmdist d (fromIntegral (length dir))
-  ncompl = nondeterminize . compl . rmmin . determinize
+   in minReachability (length dir) (ncompl nfa)
+  where
+    md dfa = minDistinguishability dfa (length dir)
+    ncompl = nondeterminize . compl . md . determinize
 automatize dir (QNMFormula (Qua (Exists, v) : quas) m) =
   let nfa = automatize dir (QNMFormula quas m)
-  in  case M.lookup (Var v) dir of
-        Nothing  -> nfa
-        (Just i) -> minimize (fromIntegral $ length dir) $ existentialize i nfa
+   in case M.lookup (Var v) dir of
+        Nothing -> nfa
+        (Just i) -> minReachability (length dir) $ existentialize i nfa
+automatize _ (QNMFormula (Qua (ForAll, _) : _) _) =
+  error "should be universal-free"
 
 assign :: S.Set Addend -> M.Map Addend Int
 assign xs = M.fromList (zip (S.toList xs) [0 ..])
 
 collect :: Matrix -> S.Set Addend
-collect (MEq  as bs) = S.fromList (as ++ bs)
-collect (MLe  a  b ) = S.fromList [a, b]
-collect (MLt  a  b ) = S.fromList [a, b]
-collect (MAnd x  y ) = S.union (collect x) (collect y)
-collect (MOr  x  y ) = S.union (collect x) (collect y)
-collect (MNot x    ) = collect x
+collect (MEq as bs) = S.fromList (as ++ bs)
+collect (MLe a b) = S.fromList [a, b]
+collect (MLt a b) = S.fromList [a, b]
+collect (MAnd x y) = S.union (collect x) (collect y)
+collect (MOr x y) = S.union (collect x) (collect y)
+collect (MNot x) = collect x
 
 literals :: M.Map Addend Int -> [[Int]]
 literals m =
-  let
-    addends          = L.sortOn snd (M.toList m)
-    reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends
-    max              = L.maximum (map length reversedLiterals)
-    paddedReversed =
-      map (\x -> x ++ replicate (max - length x) 0) reversedLiterals
-    padded = map reverse paddedReversed
-  in
-    L.transpose padded
+  let addends = L.sortOn snd (M.toList m)
+      reversedLiterals = map (\(a, _) -> addendReverseBinary a) addends
+      padTo = L.maximum (map length reversedLiterals)
+      paddedReversed =
+        map (\x -> x ++ replicate (padTo - length x) 0) reversedLiterals
+      padded = map reverse paddedReversed
+   in L.transpose padded
 
 addendReverseBinary :: Addend -> [Int]
-addendReverseBinary (Var x) = []
+addendReverseBinary (Var _) = []
 addendReverseBinary (Con n) = reverseBinary n
 
-reverseBinary :: Integer -> [Int]
+reverseBinary :: Int -> [Int]
 reverseBinary 0 = []
-reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2)
+reverseBinary n = mod n 2 : reverseBinary (div n 2)
 
 eval :: QNMFormula -> Bool
-eval f@(QNMFormula q m) =
-  let dir   = (assign $ collect m)
-      nfa   = automatize dir f
+eval f@(QNMFormula _ m) =
+  let dir = (assign $ collect m)
+      nfa = automatize dir f
       input = literals (assign $ collect m)
-  in  runNFA nfa input
+   in runNFA nfa input
 
 data State a = S a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show)
 
@@ -93,137 +90,76 @@ data NFA c a = NFA [State a] [State a] [State a] (State a -> c -> [State a])
 runDFA :: (Ord a) => DFA c a -> [c] -> Bool
 runDFA (DFA _ start accepts f) cs = foldl f start cs `elem` accepts
 
-minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a
-minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f
- where
-  states'  = closure nfa (chars n) starts
-  starts'  = starts `L.intersect` states'
-  accepts' = accepts `L.intersect` states'
-
-
-rmdist :: (Ord a, Show a) => DFA [Int] a -> Integer -> DFA [Int] a
-rmdist dfa@(DFA states start accepts f) n =
-  let
-    statecandidates = minimize2 dfa n
-    states'         = map head statecandidates
-    start' = head $ head $ filter (\c -> L.elem start c) statecandidates
-    accepts'        = L.intersect accepts states'
-    f' s c =
-      let s' = f s c
-      in  head $ head $ filter (\c -> L.elem s' c) statecandidates
-  in
-    DFA states' start' accepts' f'
-
-
-minimize2 :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]]
-minimize2 dfa@(DFA states start accepts f) n =
-  let p0 = [states L.\\ accepts, accepts] in minrec dfa n p0
-
-minrec
-  :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]] -> [[State a]]
-minrec dfa n pklast =
-  let next = concatMap (\part -> minimize3 dfa n pklast [] part) pklast
-  in  if normpartition next == normpartition pklast
-        then next
-        else minrec dfa n next
-
-normpartition :: Ord a => [[a]] -> S.Set (S.Set a)
-normpartition xs = S.fromList (map S.fromList xs)
-
-
-minimize3
-  :: (Ord a, Show a)
-  => DFA [Int] a
-  -> Integer
-  -> [[State a]]
-  -> [[State a]]
-  -> [State a]
-  -> [[State a]]
-minimize3 dfa@(DFA states starts accepts f) n pklast pk [] = pk
-minimize3 dfa@(DFA states starts accepts f) n pklast [] (x : xs) =
-  minimize3 dfa n pklast [[x]] xs
-minimize3 dfa@(DFA states starts accepts f) n pklast pk (x : xs) =
-  let ys = filter (\s -> equivall dfa pklast (chars n) (head s) x) pk
-  in  if ys == []
-        then minimize3 dfa n pklast ([x] : pk) xs
-        else
-          let coll  = (head ys)
-              trunc = L.delete coll pk
-              new   = x : coll
-              pk'   = new : trunc
-          in  minimize3 dfa n pklast pk' xs
-
-equivall
-  :: (Eq a)
-  => DFA [Int] a
-  -> [[State a]]
-  -> [[Int]]
-  -> (State a)
-  -> (State a)
-  -> Bool
-equivall dfa partition cs x y = all (\c -> not $ dist dfa partition c x y) cs
-
-states = S <$> [0, 1, 2, 3, 4]
-start = S 0
-accepts = [S 4]
-f (S 0) [0] = S 1
-f (S 0) [1] = S 2
-f (S 1) [0] = S 1
-f (S 1) [1] = S 3
-f (S 2) [0] = S 1
-f (S 2) [1] = S 2
-f (S 3) [0] = S 1
-f (S 3) [1] = S 4
-f (S 4) [0] = S 1
-f (S 4) [1] = S 2
-dfa = DFA states start accepts f
-p0 = [states L.\\ accepts, accepts]
-p1 = concatMap (minimize3 dfa 1 p0 []) p0
-p2 = concatMap (minimize3 dfa 1 p1 []) p1
-minp = minimize2 dfa 1
-
-
-dist
-  :: (Eq a)
-  => DFA [Int] a
-  -> [[State a]]
-  -> [Int]
-  -> (State a)
-  -> (State a)
-  -> Bool
-dist (DFA states starts accepts f) partition c x y =
-  (findset partition (f x c)) /= (findset partition (f y c))
-
-findset :: (Eq a) => [[State a]] -> State a -> [State a]
-findset xs x = head (filter (\s -> L.elem x s) xs)
+minReachability :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a
+minReachability n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f
+  where
+    states' = closure nfa (chars n) starts
+    starts' = starts `L.intersect` states'
+    accepts' = accepts `L.intersect` states'
+
+minDistinguishability :: (Ord a, Show a) => DFA [Int] a -> Int -> DFA [Int] a
+minDistinguishability dfa@(DFA _ start accepts f) n =
+  let partition = hopcroftPartitionRefinement dfa n
+      states' = map head partition
+      start' = head $ head $ filter (L.elem start) partition
+      accepts' = L.intersect accepts states'
+      f' s c = let s' = f s c in head $ head $ filter (L.elem s') partition
+   in DFA states' start' accepts' f'
+
+hopcroftPartitionRefinement ::
+  (Ord a, Show a) => DFA [Int] a -> Int -> [[State a]]
+hopcroftPartitionRefinement (DFA states _ accepts f) n =
+  let p0 = [states L.\\ accepts, accepts] in recurse p0
+  where
+    sigma = chars n
+    normalizePartition partition = S.fromList (map S.fromList partition)
+    findInPartition xs x = fromJust $ L.find (L.elem x) xs
+    equalUnder partition x y =
+      findInPartition partition x == findInPartition partition y
+    indistinguishable partition x y =
+      all (\c -> equalUnder partition (f x c) (f y c)) sigma
+    partialRefine _ pk [] = pk
+    partialRefine pkPrev [] (x : xs) = partialRefine pkPrev [[x]] xs
+    partialRefine pkPrev pk (x : xs) =
+      case filter (\s -> indistinguishable pkPrev (head s) x) pk of
+        [] -> partialRefine pkPrev ([x] : pk) xs
+        [match] -> partialRefine pkPrev ((x : match) : L.delete match pk) xs
+        _ -> error "should be unreachable"
+    recurse pkPrev =
+      let pk = concatMap (partialRefine pkPrev []) pkPrev
+       in if normalizePartition pk == normalizePartition pkPrev
+            then pk
+            else recurse pk
 
 runNFA :: (Ord a) => NFA c a -> [c] -> Bool
 runNFA (NFA _ starts accepts f) cs =
   foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs
     `L.intersect` accepts
-    /=            []
+    /= []
 
 reversal :: (Ord a) => NFA c a -> NFA c a
 reversal (NFA states starts accepts f) = NFA states accepts starts f'
-  where f' s c = filter (\state -> s `elem` f state c) states
-
-eq :: Integer -> [Int] -> [Int] -> DFA [Int] Int
-eq n is js = determinize $ minimize n $ reversal $ nondeterminize dfa
- where
-  states   = S <$> [-(length js - 1) .. length is - 1 + 1]
-  start    = S 0
-  accepts  = [S 0]
-  rejector = last states
-  f :: State Int -> [Int] -> State Int
-  f carrystate@(S carry) c = if carrystate == rejector
-    then rejector
-    else
-      let si       = sum (map ((c) !!) (is))
-          sj       = sum (map (c !!) (js))
-          parityok = mod (carry + si) 2 == mod sj 2
-          newcarry = div (carry + si - sj) 2
-      in  if parityok then S newcarry else rejector
-  dfa = DFA states start accepts f
+  where
+    f' s c = filter (\state -> s `elem` f state c) states
+
+eq :: Int -> [Int] -> [Int] -> DFA [Int] Int
+eq n is js = determinize $ minReachability n $ reversal $ nondeterminize dfa
+  where
+    states = S <$> [- (length js - 1) .. length is - 1 + 1]
+    start = S 0
+    accepts = [S 0]
+    rejector = last states
+    f :: State Int -> [Int] -> State Int
+    f carrystate@(S carry) c =
+      if carrystate == rejector
+        then rejector
+        else
+          let si = sum (map (c !!) is)
+              sj = sum (map (c !!) js)
+              parityok = mod (carry + si) 2 == mod sj 2
+              newcarry = div (carry + si - sj) 2
+           in if parityok then S newcarry else rejector
+    dfa = DFA states start accepts f
 
 le :: Int -> Int -> DFA [Int] Int
 le = less LessEqual
@@ -234,37 +170,38 @@ lt = less LessThan
 data LessType = LessEqual | LessThan deriving (Eq, Ord, Show)
 
 less :: LessType -> Int -> Int -> DFA [Int] Int
-less lt i j = DFA [S 0, S 1, S 2] (S 0) accepts f
- where
-  accepts = if lt == LessEqual then [S 0, S 2] else [S 2]
-  f s c = case (s, (c !! i, c !! j)) of
-    (S 0, (1, 1)) -> S 0
-    (S 0, (0, 0)) -> S 0
-    (S 0, (1, 0)) -> S 1
-    (S 0, _     ) -> S 2
-    (S 1, _     ) -> S 1
-    (_  , _     ) -> S 2
+less op i j = DFA [S 0, S 1, S 2] (S 0) accepts f
+  where
+    accepts = if op == LessEqual then [S 0, S 2] else [S 2]
+    f s c = case (s, (c !! i, c !! j)) of
+      (S 0, (1, 1)) -> S 0
+      (S 0, (0, 0)) -> S 0
+      (S 0, (1, 0)) -> S 1
+      (S 0, _) -> S 2
+      (S 1, _) -> S 1
+      (_, _) -> S 2
 
 prod :: [a] -> [b] -> [(a, b)]
-prod xs       [] = []
-prod []       ys = []
-prod (x : xs) ys = fmap (x, ) ys ++ prod xs ys
+prod _ [] = []
+prod [] _ = []
+prod (x : xs) ys = fmap (x,) ys ++ prod xs ys
 
 data JunctionType = Conj | Disj deriving (Eq, Ord, Show)
 
 junction :: (Ord a) => JunctionType -> DFA c a -> DFA c a -> DFA c a
 junction jt (DFA states1 start1 accepts1 f1) (DFA states2 start2 accepts2 f2) =
   DFA states' start' accepts' f'
- where
-  newStates = prod states1 states2
-  states'   = Double <$> newStates
-  start'    = Double (start1, start2)
-  accepts'  = if jt == Conj
-    then Double <$> prod accepts1 accepts2
-    else
-      Double
-        <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
-  f' (Double (s, t)) c = Double (f1 s c, f2 t c)
+  where
+    newStates = prod states1 states2
+    states' = Double <$> newStates
+    start' = Double (start1, start2)
+    accepts' =
+      if jt == Conj
+        then Double <$> prod accepts1 accepts2
+        else
+          Double
+            <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
+    f' (Double (s, t)) c = Double (f1 s c, f2 t c)
 
 conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
 conj = junction Conj
@@ -277,44 +214,46 @@ compl (DFA states start accepts f) = DFA states start (states L.\\ accepts) f
 
 nondeterminize :: (Ord a) => DFA c a -> NFA c a
 nondeterminize (DFA states start accepts f) = NFA states [start] accepts f'
-  where f' s c = [f s c]
+  where
+    f' s c = [f s c]
 
 change :: [a] -> Int -> a -> [a]
 change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs
 
 closure :: (Ord a) => NFA c a -> [c] -> [State a] -> [State a]
-closure nfa@(NFA states starts accepts f) cs initstates =
+closure nfa@(NFA _ _ _ f) cs initstates =
   let new = concatMap (\state -> concatMap (f state) cs) initstates
-  in  if L.nub new L.\\ L.nub initstates /= []
+   in if L.nub new L.\\ L.nub initstates /= []
         then closure nfa cs (L.nub $ new ++ initstates)
         else L.nub initstates
 
 existentialize :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a
-existentialize idx nfa@(NFA states starts accepts f) = NFA states
-                                                           starts'
-                                                           accepts
-                                                           f'
- where
-  zeroer  = replicate 50 0
-  oneer   = change zeroer idx 1
-  starts' = closure nfa [zeroer, oneer] starts
-  f' s c = f s (change c idx 0) ++ f s (change c idx 1)
+existentialize idx nfa@(NFA states starts accepts f) =
+  NFA
+    states
+    starts'
+    accepts
+    f'
+  where
+    zeroer = replicate 50 0
+    oneer = change zeroer idx 1
+    starts' = closure nfa [zeroer, oneer] starts
+    f' s c = f s (change c idx 0) ++ f s (change c idx 1)
 
 powerset :: [a] -> [[a]]
-powerset []       = [[]]
+powerset [] = [[]]
 powerset (x : xs) = let rest = powerset xs in map (x :) rest ++ rest
 
 determinize :: (Ord a) => NFA c a -> DFA c a
 determinize (NFA states start accepts f) = DFA states' start' accepts' f'
- where
-  newStates = map L.sort $ powerset states
-  states'   = Multi <$> newStates
-  start'    = Multi $ L.sort start
-  accepts' =
-    Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
-  f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s
-
-
-chars :: Integer -> [[Int]]
+  where
+    newStates = map L.sort $ powerset states
+    states' = Multi <$> newStates
+    start' = Multi $ L.sort start
+    accepts' =
+      Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
+    f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s
+
+chars :: Int -> [[Int]]
 chars 0 = [[]]
 chars n = let r = chars (n - 1) in map (1 :) r ++ map (0 :) r
diff --git a/src/Parser.hs b/src/Parser.hs
index 2d0798f..77cde09 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -3,29 +3,24 @@
 
 module Parser where
 
-import Control.Applicative
-import qualified Data.Bifunctor
-import qualified Data.Either.Combinators as E
-import Data.Functor.Identity
-import qualified Data.List as L
-import qualified Data.Set as S
-import Text.Parsec ((<?>))
-import qualified Text.Parsec as Parsec
-import Text.Parsec.Language (haskellDef)
-import qualified Text.Parsec.Token as P
-
-pparse ::
-  Parsec.Stream s Data.Functor.Identity.Identity t =>
-  Parsec.Parsec s () a ->
-  s ->
-  Either Parsec.ParseError a
+import           Control.Applicative
+import qualified Data.Either.Combinators       as E
+import           Data.Functor.Identity
+import qualified Data.Set                      as S
+import qualified Text.Parsec                   as Parsec
+
+pparse
+  :: Parsec.Stream s Data.Functor.Identity.Identity t
+  => Parsec.Parsec s () a
+  -> s
+  -> Either Parsec.ParseError a
 pparse rule = Parsec.parse rule ""
 
 type Parser a = Parsec.Parsec String () a
 
 type Symbol = String
 
-type Natural = Integer
+type Natural = Int
 
 data Addend = Var Symbol | Con Natural deriving (Show, Eq, Ord)
 
@@ -49,7 +44,7 @@ data Formula
 pSymbol :: Parser Symbol
 pSymbol = Parsec.many1 (Parsec.oneOf $ ['a' .. 'z'] ++ ['\''])
 
-pNatural :: Parser Integer
+pNatural :: Parser Int
 pNatural = read <$> Parsec.many1 Parsec.digit
 
 pAddend :: Parser Addend
@@ -67,32 +62,35 @@ singleton a = [a]
 pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a
 pSums s op = do
   as <- f
-  Parsec.string s
+  _  <- Parsec.string s
   bs <- f
   return $ op (concat as) (concat bs)
-  where
-    f = Parsec.sepBy1 (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural)) (Parsec.char '+')
+ where
+  f = Parsec.sepBy1
+    (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural))
+    (Parsec.char '+')
 
 pBinOp :: String -> (Addend -> Addend -> a) -> Parser a
 pBinOp s op = do
   a <- pAddend
-  Parsec.string s
+  _ <- Parsec.string s
   b <- pAddend
   return $ op a b
 
 pMultiMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
 pMultiMatOp s op = do
-  term <- pFormulaInner
-  Parsec.space *> Parsec.string s *> Parsec.space
-  terms <- Parsec.sepBy1 pFormulaInner (Parsec.space *> Parsec.string s *> Parsec.space)
+  term  <- pFormulaInner
+  _     <- Parsec.space *> Parsec.string s *> Parsec.space
+  terms <- Parsec.sepBy1 pFormulaInner
+                         (Parsec.space *> Parsec.string s *> Parsec.space)
   return $ foldl1 op (term : terms)
 
 pBinMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
 pBinMatOp s op = do
   x <- pFormulaInner
-  Parsec.space
-  Parsec.string s
-  Parsec.space
+  _ <- Parsec.space
+  _ <- Parsec.string s
+  _ <- Parsec.space
   y <- pFormulaInner
   return $ op x y
 
@@ -117,13 +115,13 @@ pFormulaInner =
     <|> Parsec.try (pBinOp ">" Gt)
     <|> Parsec.try pNot
     <|> Parsec.between
-      (Parsec.char '(')
-      (Parsec.char ')')
-      ( Parsec.try (pMultiMatOp "&" And)
+          (Parsec.char '(')
+          (Parsec.char ')')
+          (   Parsec.try (pMultiMatOp "&" And)
           <|> Parsec.try (pMultiMatOp "|" Or)
           <|> Parsec.try (pBinMatOp "<->" Iff)
           <|> Parsec.try (pBinMatOp "->" Imp)
-      )
+          )
     <|> Parsec.try pQuantifier
 
 pFormula :: Parser Formula
@@ -141,60 +139,59 @@ data Matrix
   | MOr Matrix Matrix
   deriving (Eq, Show)
 
-data MFormula = MFormula [(Quantifier, Symbol)] Matrix deriving (Eq, Show)
+data MFormula = MFormula [(Quantifier, Symbol)] Matrix
+  deriving (Eq, Show)
 
 -- assumes simplified, pnf
 split :: Formula -> MFormula
-split (Q q v x) =
-  let (MFormula p m) = split x
-   in MFormula ((q, v) : p) m
+split (Q q v x ) = let (MFormula p m) = split x in MFormula ((q, v) : p) m
 split (Eq as bs) = MFormula [] (MEq as bs)
-split (Le a b) = MFormula [] (MLe a b)
-split (Lt a b) = MFormula [] (MLt a b)
-split (Not x) =
-  let MFormula [] x' = split x
-   in MFormula [] (MNot x')
+split (Le a  b ) = MFormula [] (MLe a b)
+split (Lt a  b ) = MFormula [] (MLt a b)
+split (Not x   ) = let MFormula [] x' = split x in MFormula [] (MNot x')
 split (And x y) =
   let MFormula [] x' = split x
       MFormula [] y' = split y
-   in MFormula [] (MAnd x' y')
+  in  MFormula [] (MAnd x' y')
 split (Or x y) =
   let MFormula [] x' = split x
       MFormula [] y' = split y
-   in MFormula [] (MOr x' y')
+  in  MFormula [] (MOr x' y')
 
 renameAddend :: (Symbol -> Symbol) -> Addend -> Addend
 renameAddend f (Var x) = Var (f x)
-renameAddend f x = x
+renameAddend f x       = x
 
 -- TODO restrict type?
 simplify :: Formula -> Formula
 simplify x@(Eq as bs) = x
-simplify (Ne as bs) = Not (Eq as bs)
-simplify x@(Le a b) = x
-simplify x@(Lt a b) = x
-simplify (Ge a b) = Le b a
-simplify (Gt a b) = Lt b a
-simplify (Not x) = Not (simplify x)
-simplify (And x y) = And (simplify x) (simplify y)
-simplify (Or x y) = Or (simplify x) (simplify y)
-simplify (Imp x y) = simplify (Or (Not x) y)
-simplify (Iff x y) = simplify (And (Imp x y) (Imp y x))
-simplify (Q q v f) = Q q v (simplify f)
+simplify (  Ne as bs) = Not (Eq as bs)
+simplify x@(Le a  b ) = x
+simplify x@(Lt a  b ) = x
+simplify (  Ge a  b ) = Le b a
+simplify (  Gt a  b ) = Lt b a
+simplify (  Not x   ) = Not (simplify x)
+simplify (  And x y ) = And (simplify x) (simplify y)
+simplify (  Or  x y ) = Or (simplify x) (simplify y)
+simplify (  Imp x y ) = simplify (Or (Not x) y)
+simplify (  Iff x y ) = simplify (And (Imp x y) (Imp y x))
+simplify (  Q q v f ) = Q q v (simplify f)
 
 prenex :: Formula -> Formula
-prenex (Not x) = pull $ Not (prenex x)
+prenex (Not x  ) = pull $ Not (prenex x)
 prenex (And x y) = pull (And (prenex x) (prenex y))
-prenex (Or x y) = pull (Or (prenex x) (prenex y))
+prenex (Or  x y) = pull (Or (prenex x) (prenex y))
 prenex (Q q v x) = Q q v (prenex x)
-prenex f = f
+prenex f         = f
 
 pull :: Formula -> Formula
 pull (Not (Q ForAll x f)) = Q Exists x (pull (Not f))
 pull (Not (Q Exists x f)) = Q ForAll x (pull (Not f))
-pull (Not f) = Not f
-pull (And (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (And x' y))
-pull (And y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (And y x'))
+pull (Not f             ) = Not f
+pull (And (Q q v x) y) =
+  let (v', x') = fixup v x y in Q q v' (pull (And x' y))
+pull (And y (Q q v x)) =
+  let (v', x') = fixup v x y in Q q v' (pull (And y x'))
 pull (And x y) = And x y
 pull (Or (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (Or x' y))
 pull (Or y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (Or y x'))
@@ -206,12 +203,12 @@ newname x seen = if x `elem` seen then newname (x <> "'") seen else x
 
 rename :: (Symbol -> Symbol) -> Formula -> Formula
 rename f (Eq as bs) = Eq (renameAddend f <$> as) (renameAddend f <$> bs)
-rename f (Le a b) = Le (renameAddend f a) (renameAddend f b)
-rename f (Lt a b) = Lt (renameAddend f a) (renameAddend f b)
-rename f (Not x) = Not (rename f x)
-rename f (And x y) = And (rename f x) (rename f y)
-rename f (Or x y) = Or (rename f x) (rename f y)
-rename f (Q q v x) = Q q (f v) (rename f x)
+rename f (Le a  b ) = Le (renameAddend f a) (renameAddend f b)
+rename f (Lt a  b ) = Lt (renameAddend f a) (renameAddend f b)
+rename f (Not x   ) = Not (rename f x)
+rename f (And x y ) = And (rename f x) (rename f y)
+rename f (Or  x y ) = Or (rename f x) (rename f y)
+rename f (Q q v x ) = Q q (f v) (rename f x)
 
 -- v is bound in x, other formula is y
 -- if v is either bound or free in y, then rename v in x (avoiding collisions in x or y)
@@ -220,67 +217,63 @@ fixup :: Symbol -> Formula -> Formula -> (Symbol, Formula)
 fixup v x y =
   let xvars = vars x
       yvars = vars y
-      v' =
-        if v `elem` yvars
-          then newname v (xvars ++ yvars)
-          else v
-      x' = rename (\z -> if z == v then v' else z) x
-   in (v', x')
+      v'    = if v `elem` yvars then newname v (xvars ++ yvars) else v
+      x'    = rename (\z -> if z == v then v' else z) x
+  in  (v', x')
 
 vars :: Formula -> [Symbol]
 vars (Eq as bs) = filtervars as ++ filtervars bs
-vars (Le a b) = filtervars [a, b]
-vars (Lt a b) = filtervars [a, b]
-vars (Not x) = vars x
-vars (And x y) = vars x ++ vars y
-vars (Or x y) = vars x ++ vars y
-vars (Q _ x f) = x : vars f
+vars (Le a  b ) = filtervars [a, b]
+vars (Lt a  b ) = filtervars [a, b]
+vars (Not x   ) = vars x
+vars (And x y ) = vars x ++ vars y
+vars (Or  x y ) = vars x ++ vars y
+vars (Q _ x f ) = x : vars f
 
 boundvars :: Formula -> [Symbol]
-boundvars (Not x) = boundvars x
+boundvars (Not x  ) = boundvars x
 boundvars (And x y) = boundvars x ++ boundvars y
-boundvars (Or x y) = boundvars x ++ boundvars y
+boundvars (Or  x y) = boundvars x ++ boundvars y
 boundvars (Q _ v f) = v : boundvars f
-boundvars x = []
+boundvars _         = []
 
 filtervars :: [Addend] -> [Symbol]
-filtervars as =
-  concatMap
-    ( \case
-        (Var x) -> [x]
-        (Con x) -> []
-    )
-    as
+filtervars = concatMap
+  (\case
+    (Var x) -> [x]
+    (Con _) -> []
+  )
 
 data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show)
 
-data QNMFormula = QNMFormula [QN] Matrix deriving (Eq, Show)
+data QNMFormula = QNMFormula [QN] Matrix
+  deriving (Eq, Show)
 
 eliminateUniversals :: [(Quantifier, Symbol)] -> [QN]
 eliminateUniversals [] = []
 eliminateUniversals ((q, v) : quas) =
   let ret = eliminateUniversals quas
       qua = Qua (Exists, v)
-   in if q == ForAll
-        then [Neg, qua, Neg] ++ ret
-        else qua : ret
+  in  if q == ForAll then [Neg, qua, Neg] ++ ret else qua : ret
 
 simplifyNegsQua :: [QN] -> [QN]
-simplifyNegsQua [] = []
+simplifyNegsQua []                 = []
 simplifyNegsQua (Neg : Neg : quas) = quas
-simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
+simplifyNegsQua (qua       : quas) = qua : simplifyNegsQua quas
 
 simplifyNegs :: MFormula -> QNMFormula
 simplifyNegs (MFormula quas m) =
   let quas' = (simplifyNegsQua . eliminateUniversals) quas
-   in QNMFormula quas' m
+  in  QNMFormula quas' m
 
 anyUnboundVars :: Formula -> Bool
-anyUnboundVars f = not $ S.null (S.fromList (vars f) S.\\ S.fromList (boundvars f))
+anyUnboundVars f =
+  not $ S.null (S.fromList (vars f) S.\\ S.fromList (boundvars f))
 
 parseMFormula :: String -> Either String QNMFormula
 parseMFormula s = do
-  formula <- E.mapLeft (flip (<>) "." . show) (prenex . simplify <$> pparse pFormula s)
+  formula <- E.mapLeft (flip (<>) "." . show)
+                       (prenex . simplify <$> pparse pFormula s)
   if anyUnboundVars formula
     then Left "All variables must be bound."
     else Right $ simplifyNegs $ split formula