24.09., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

PP.hs 7.36 KB
Newer Older
1
module Parser.PP
2 3 4
    (parseContent)
where

5 6
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
7
import Text.Parsec
8
import Text.Parsec.Expr
9 10 11 12
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import Parser
13
import PopulationProtocol (PopulationProtocol,makePopulationProtocolFromStrings,State(..),Transition(..))
14 15 16 17 18 19 20 21 22 23
import Property

languageDef :: LanguageDef ()
languageDef =
        emptyDef {
                 Token.commentStart    = "/*",
                 Token.commentEnd      = "*/",
                 Token.commentLine     = "//",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> char '_',
24
                 Token.reservedNames   = ["true", "false", "EXISTS", "FORALL"],
25
                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
26
                                          "+", "-", "*", "&&", "||", "!", ":"]
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
                 }

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

71 72
states :: Parser [String]
states = reserved "states" *> identList
73 74 75 76

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

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

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

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

86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
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

105 106 107
data Statement = States [String]
               | Transitions [String]
               | Initial [String]
108 109
               | TrueStatement [String]
               | FalseStatement [String]
110
               | PredicateStatement (QuantFormula String)
111
               | Arcs [(String,String,Integer)]
112 113

statement :: Parser Statement
114
statement = States <$> states <|>
115 116
            Transitions <$> transitions <|>
            Arcs <$> arcs <|>
117
            Initial <$> initial <|>
118
            TrueStatement <$> trueStates <|>
119 120
            FalseStatement <$> falseStates <|>
            PredicateStatement <$> predicate
121

122 123 124 125
populationProtocol :: Parser PopulationProtocol
populationProtocol = do
            reserved "population"
            reserved "protocol"
126 127
            name <- option "" ident
            statements <- braces (many statement)
128
            let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],Nothing,[]) statements
129
            let predicate = case ps of
130 131
                                Nothing -> ExQuantFormula [] FTrue
                                Just p -> p
132
            return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as
133
        where
134 135 136 137 138 139
            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)
140
                  PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,Just p,as)
141
                  Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as)
142

143 144 145 146
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 )
147

148
termOperatorTable :: [[Operator String () Identity (Term String)]]
149 150 151 152 153 154
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

155
termAtom :: Parser (Term String)
156
termAtom =  (Var <$> ident)
157
        <|> (Const <$> integer)
158 159
        <|> parens term
        <?> "basic term"
160

161
term :: Parser (Term String)
162
term = buildExpressionParser termOperatorTable termAtom <?> "term"
163 164 165 166 167

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

172
linIneq :: Parser (Formula String)
173
linIneq = do
174 175 176
        lhs <- term
        op <- parseOp
        rhs <- term
177
        return (LinearInequation lhs op rhs)
178

179
formOperatorTable :: [[Operator String () Identity (Formula String)]]
180 181 182 183 184
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]
185

186
formAtom :: Parser (Formula String)
187
formAtom =  try linIneq
188 189
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
190 191
        <|> parens formula
        <?> "basic formula"
192

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

196 197 198 199 200 201 202 203 204 205 206 207 208
quantFormula :: Parser (QuantFormula String)
quantFormula =
        (do
            reserved "EXISTS"
            xs <- optionalCommaSep ident
            reservedOp ":"
            p <- formula
            return (ExQuantFormula xs p)
        )
          <|>
        (ExQuantFormula [] <$> formula)

predicate :: Parser (QuantFormula String)
Philipp Meyer's avatar
Philipp Meyer committed
209 210
predicate = do
        reserved "predicate"
211
        form <- braces quantFormula
212
        return form
Philipp Meyer's avatar
Philipp Meyer committed
213 214

parseContent :: Parser PopulationProtocol
215 216
parseContent = do
        whiteSpace
217
        pp <- populationProtocol
218
        properties <- many predicate
219
        eof
Philipp Meyer's avatar
Philipp Meyer committed
220
        return pp