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

PP.hs 6.74 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"],
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
               | Arcs [(String,String,Integer)]
111 112

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

120 121 122 123
populationProtocol :: Parser PopulationProtocol
populationProtocol = do
            reserved "population"
            reserved "protocol"
124 125
            name <- option "" ident
            statements <- braces (many statement)
126 127
            let (qs,ts,qinitial,qtrue,qfalse,as) = foldl splitStatement ([],[],[],[],[],[]) statements
            return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse as
128
        where
129 130 131 132 133 134 135
            splitStatement (qs,ts,qinitial,qtrue,qfalse,as) stmnt = case stmnt of
                  States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,as)
                  Transitions t -> (qs,t ++ ts,qinitial,qtrue,qfalse,as)
                  Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,as)
                  TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,as)
                  FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,as)
                  Arcs a -> (qs,ts,qinitial,qtrue,qfalse,a ++ as)
136

137 138 139 140
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 )
141

142
termOperatorTable :: [[Operator String () Identity (Term String)]]
143 144 145 146 147 148
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

149
termAtom :: Parser (Term String)
150
termAtom =  (Var <$> ident)
151
        <|> (Const <$> integer)
152 153
        <|> parens term
        <?> "basic term"
154

155
term :: Parser (Term String)
156
term = buildExpressionParser termOperatorTable termAtom <?> "term"
157 158 159 160 161

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

166
linIneq :: Parser (Formula String)
167
linIneq = do
168 169 170
        lhs <- term
        op <- parseOp
        rhs <- term
171
        return (LinearInequation lhs op rhs)
172

173
formOperatorTable :: [[Operator String () Identity (Formula String)]]
174 175 176 177 178
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]
179

180
formAtom :: Parser (Formula String)
181
formAtom =  try linIneq
182 183
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
184 185
        <|> parens formula
        <?> "basic formula"
186

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

Philipp Meyer's avatar
Philipp Meyer committed
190 191 192
predicate :: Parser (Formula PopulationProtocol.State)
predicate = do
        reserved "predicate"
193
        name <- option "" ident
Philipp Meyer's avatar
Philipp Meyer committed
194 195 196 197
        form <- braces formula
        return (fmap PopulationProtocol.State form)

parseContent :: Parser PopulationProtocol
198 199
parseContent = do
        whiteSpace
200
        pp <- populationProtocol
Philipp Meyer's avatar
Philipp Meyer committed
201
--        properties <- many predicate
202
        eof
Philipp Meyer's avatar
Philipp Meyer committed
203
        return pp