1 files changed, 288 insertions, 0 deletions
diff --git a/src/Parser.hs b/src/Parser.hs
new file mode 100644
index 0000000..c61cd79
--- /dev/null
+++ b/src/Parser.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+
+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
+pparse rule = Parsec.parse rule ""
+
+type Parser a = Parsec.Parsec String () a
+
+type Symbol = String
+
+type Natural = Integer
+
+data Addend = Var Symbol | Con Natural deriving (Show, Eq, Ord)
+
+data Quantifier = ForAll | Exists deriving (Show, Eq, Ord)
+
+data Formula
+  = Eq [Addend] [Addend]
+  | Ne [Addend] [Addend]
+  | Le Addend Addend
+  | Lt Addend Addend
+  | Ge Addend Addend
+  | Gt Addend Addend
+  | Not Formula
+  | And Formula Formula
+  | Or Formula Formula
+  | Imp Formula Formula
+  | Iff Formula Formula
+  | Q Quantifier Symbol Formula
+  deriving (Show)
+
+pSymbol :: Parser Symbol
+pSymbol = Parsec.many1 (Parsec.oneOf $ ['a' .. 'z'] ++ ['\''])
+
+pNatural :: Parser Integer
+pNatural = read <$> Parsec.many1 Parsec.digit
+
+pAddend :: Parser Addend
+pAddend = Var <$> pSymbol <|> Con <$> pNatural
+
+pTerm :: Parser [Addend]
+pTerm = do
+  c <- Parsec.option 1 pNatural
+  a <- pSymbol
+  return $ replicate (fromIntegral c) (Var a)
+
+singleton :: a -> [a]
+singleton a = [a]
+
+pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a
+pSums s op = do
+  as <- f
+  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
+
+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)
+  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
+  y <- pFormulaInner
+  return $ op x y
+
+pNot :: Parser Formula
+pNot = Not <$> (Parsec.char '~' *> pFormulaInner)
+
+pQuantifier :: Parser Formula
+pQuantifier = do
+  q <- Parsec.oneOf ['A', 'E']
+  c <- pSymbol
+  Parsec.char '.'
+  f <- pFormulaInner
+  return $ Q (if q == 'A' then ForAll else Exists) c f
+
+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 pNot
+    <|> Parsec.between
+      (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
+pFormula = do
+  p <- pFormulaInner
+  Parsec.eof
+  return p
+
+data Matrix
+  = MEq [Addend] [Addend]
+  | MLe Addend Addend
+  | MLt Addend Addend
+  | MNot Matrix
+  | MAnd Matrix Matrix
+  | MOr Matrix 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 (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 (And x y) =
+  let MFormula [] x' = split x
+      MFormula [] y' = split y
+   in MFormula [] (MAnd x' y')
+split (Or x y) =
+  let MFormula [] x' = split x
+      MFormula [] y' = split y
+   in MFormula [] (MOr x' y')
+
+(&) = And
+
+renameAddend :: (Symbol -> Symbol) -> Addend -> Addend
+renameAddend f (Var x) = Var (f 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)
+
+prenex :: Formula -> Formula
+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 (Q q v x) = Q q v (prenex x)
+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 (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'))
+pull (Or x y) = Or x y
+pull x = x
+
+newname :: Symbol -> [Symbol] -> Symbol
+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)
+
+-- 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)
+-- otherwise, leave as is
+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')
+
+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
+
+boundvars :: Formula -> [Symbol]
+boundvars (Not x) = boundvars x
+boundvars (And x y) = boundvars x ++ boundvars y
+boundvars (Or x y) = boundvars x ++ boundvars y
+boundvars (Q _ v f) = v : boundvars f
+boundvars x = []
+
+filtervars :: [Addend] -> [Symbol]
+filtervars as =
+  concatMap
+    ( \case
+        (Var x) -> [x]
+        (Con x) -> []
+    )
+    as
+
+data QN = Qua (Quantifier, Symbol) | Neg 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
+
+simplifyNegsQua :: [QN] -> [QN]
+simplifyNegsQua [] = []
+simplifyNegsQua (Neg : Neg : quas) = quas
+simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
+
+simplifyNegs :: MFormula -> QNMFormula
+simplifyNegs (MFormula quas m) =
+  let quas' = (simplifyNegsQua . eliminateUniversals) quas
+   in QNMFormula quas' m
+
+anyUnboundVars :: Formula -> Bool
+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)
+  if anyUnboundVars formula
+    then Left "All variables must be bound."
+    else Right $ simplifyNegs $ split formula