Generalize Le/Lt to support multiple addends

1 files changed, 90 insertions, 88 deletions

diff --git a/src/Parser.hs b/src/Parser.hs
index 77cde09..e328b6e 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -3,17 +3,17 @@
 
 module Parser where
 
-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
+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
@@ -29,10 +29,10 @@ data Quantifier = ForAll | Exists deriving (Show, Eq, Ord)
 data Formula
   = Eq [Addend] [Addend]
   | Ne [Addend] [Addend]
+  | GenLe [Addend] [Addend]
+  | GenLt [Addend] [Addend]
   | Le Addend Addend
   | Lt Addend Addend
-  | Ge Addend Addend
-  | Gt Addend Addend
   | Not Formula
   | And Formula Formula
   | Or Formula Formula
@@ -62,27 +62,23 @@ 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 '+')
-
-pBinOp :: String -> (Addend -> Addend -> a) -> Parser a
-pBinOp s op = do
-  a <- pAddend
-  _ <- Parsec.string s
-  b <- pAddend
-  return $ op a b
+  where
+    f =
+      Parsec.sepBy1
+        (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural))
+        (Parsec.char '+')
 
 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
@@ -109,19 +105,19 @@ pFormulaInner :: Parser Formula
 pFormulaInner =
   Parsec.try (pSums "=" Eq)
     <|> Parsec.try (pSums "!=" Ne)
-    <|> Parsec.try (pBinOp "<=" Le)
-    <|> Parsec.try (pBinOp "<" Lt)
-    <|> Parsec.try (pBinOp ">=" Ge)
-    <|> Parsec.try (pBinOp ">" Gt)
+    <|> Parsec.try (pSums "<=" GenLe)
+    <|> Parsec.try (pSums "<" GenLt)
+    <|> Parsec.try (pSums ">=" (flip GenLe))
+    <|> Parsec.try (pSums ">" (flip GenLt))
     <|> 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
@@ -144,50 +140,53 @@ data MFormula = MFormula [(Quantifier, Symbol)] Matrix
 
 -- 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
+-- note: "V" will not appear in user input, as Symbol is over a-z
+simplify (GenLe [a] [b]) = Le a b
+simplify (GenLe as bs) = Q Exists "V" (Eq (Var "V" : as) bs)
+simplify (GenLt [a] [b]) = Lt a b
+simplify (GenLt as bs) = Q Exists "V" (Eq (Var "V" : Con 1 : as) bs)
+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 (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)) =
@@ -203,12 +202,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)
@@ -217,32 +216,33 @@ 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 _         = []
+boundvars _ = []
 
 filtervars :: [Addend] -> [Symbol]
-filtervars = concatMap
-  (\case
-    (Var x) -> [x]
-    (Con _) -> []
-  )
+filtervars =
+  concatMap
+    ( \case
+        (Var x) -> [x]
+        (Con _) -> []
+    )
 
 data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show)
 
@@ -254,17 +254,17 @@ 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 =
@@ -272,8 +272,10 @@ anyUnboundVars 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