path: root/src/Parser.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}

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
pparse rule = Parsec.parse rule ""

type Parser a = Parsec.Parsec String () a

type Symbol = String

type Natural = Int

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 Int
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')

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 _         = []

filtervars :: [Addend] -> [Symbol]
filtervars = concatMap
  (\case
    (Var x) -> [x]
    (Con _) -> []
  )

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