PP.hs

module Parser.PP
    (parseContent)
where

import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import Parser
import PopulationProtocol (PopulationProtocol,makePopulationProtocolFromStrings,State(..),Transition(..))
import Property

languageDef :: LanguageDef ()
languageDef =
        emptyDef {
                 Token.commentStart    = "/*",
                 Token.commentEnd      = "*/",
                 Token.commentLine     = "//",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> char '_',
                 Token.reservedNames   = ["true", "false", "EXISTS", "FORALL"],
                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
                                          "+", "-", "*", "&&", "||", "!", ":"]
                 }

lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef

identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
stringLiteral :: Parser String
stringLiteral = Token.stringLiteral lexer -- parses a string literal
reserved :: String -> Parser ()
reserved   = Token.reserved   lexer -- parses a reserved name
reservedOp :: String -> Parser ()
reservedOp = Token.reservedOp lexer -- parses an operator
brackets :: Parser a -> Parser a
brackets   = Token.brackets   lexer -- parses p surrounded by brackets
braces :: Parser a -> Parser a
braces     = Token.braces     lexer -- parses p surrounded by braces
parens :: Parser a -> Parser a
parens     = Token.parens     lexer -- parses p surrounded by parenthesis
natural :: Parser Integer
natural    = Token.natural    lexer -- parses a natural number
integer :: Parser Integer
integer    = Token.integer    lexer -- parses an integer
comma :: Parser String
comma      = Token.comma       lexer -- parses a comma
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace


optionalCommaSep :: Parser a -> Parser [a]
optionalCommaSep p = many (p <* optional comma)

singleOrList :: Parser a -> Parser [a]
singleOrList p = braces (optionalCommaSep p) <|> (:[]) <$> p

numberOption :: Parser Integer
numberOption = option 1 (brackets natural)

ident :: Parser String
ident = (identifier <|> stringLiteral) <?> "identifier"

identList :: Parser [String]
identList = singleOrList ident

states :: Parser [String]
states = reserved "states" *> identList

transitions :: Parser [String]
transitions = reserved "transitions" *> identList

initial :: Parser [String]
initial = reserved "initial" *> identList

trueStates :: Parser [String]
trueStates = reserved "true" *> identList

falseStates :: Parser [String]
falseStates = reserved "false" *> identList

arc :: Parser [(String,String,Integer)]
arc = do
        lhs <- identList
        rhsList <- many1 (do
                reservedOp "->"
                w <- numberOption
                ids <- identList
                return (ids,w)
            )
        return $ fst $ foldl makeArc ([],lhs) rhsList
      where
        makeArc (as,lhs) (rhs,w) = ([(l,r,w) | l <- lhs, r <- rhs] ++ as, rhs)

arcs :: Parser [(String,String,Integer)]
arcs = do
        reserved "arcs"
        as <- singleOrList arc
        return $ concat as

data Statement = States [String]
               | Transitions [String]
               | Initial [String]
               | TrueStatement [String]
               | FalseStatement [String]
               | PredicateStatement (QuantFormula String)
               | Arcs [(String,String,Integer)]

statement :: Parser Statement
statement = States <$> states <|>
            Transitions <$> transitions <|>
            Arcs <$> arcs <|>
            Initial <$> initial <|>
            TrueStatement <$> trueStates <|>
            FalseStatement <$> falseStates <|>
            PredicateStatement <$> predicate

populationProtocol :: Parser PopulationProtocol
populationProtocol = do
            reserved "population"
            reserved "protocol"
            name <- option "" ident
            statements <- braces (many statement)
            let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],Nothing,[]) statements
            let predicate = case ps of
                                Nothing -> ExQuantFormula [] FTrue
                                Just p -> p
            return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as
        where
            splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of
                  States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,ps,as)
                  Transitions t -> (qs,t ++ ts,qinitial,qtrue,qfalse,ps,as)
                  Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,ps,as)
                  TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,ps,as)
                  FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as)
                  PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,Just p,as)
                  Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as)

binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix  ( reservedOp name *> return fun )
prefix :: String -> (a -> a) -> Operator String () Identity a
prefix name fun = Prefix ( reservedOp name *> return fun )

termOperatorTable :: [[Operator String () Identity (Term String)]]
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

termAtom :: Parser (Term String)
termAtom =  (Var <$> ident)
        <|> (Const <$> integer)
        <|> parens term
        <?> "basic term"

term :: Parser (Term String)
term = buildExpressionParser termOperatorTable termAtom <?> "term"

parseOp :: Parser Op
parseOp = (reservedOp "<" *> return Lt) <|>
          (reservedOp "<=" *> return Le) <|>
          (reservedOp "=" *> return Eq) <|>
          (reservedOp "!=" *> return Ne) <|>
          (reservedOp ">" *> return Gt) <|>
          (reservedOp ">=" *> return Ge)

linIneq :: Parser (Formula String)
linIneq = do
        lhs <- term
        op <- parseOp
        rhs <- term
        return (LinearInequation lhs op rhs)

formOperatorTable :: [[Operator String () Identity (Formula String)]]
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]

formAtom :: Parser (Formula String)
formAtom =  try linIneq
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
        <|> parens formula
        <?> "basic formula"

formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"

quantFormula :: Parser (QuantFormula String)
quantFormula =
        (do
            reserved "EXISTS"
            xs <- optionalCommaSep ident
            reservedOp ":"
            p <- formula
            return (ExQuantFormula xs p)
        )
          <|>
        (ExQuantFormula [] <$> formula)

predicate :: Parser (QuantFormula String)
predicate = do
        reserved "predicate"
        form <- braces quantFormula
        return form

parseContent :: Parser PopulationProtocol
parseContent = do
        whiteSpace
        pp <- populationProtocol
        properties <- many predicate
        eof
        return pp