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.07 KB
Newer Older
Stefan Jaax's avatar
Stefan Jaax committed
1 2 3 4
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

5
module Parser.PP
6 7 8
    (parseContent)
where

Stefan Jaax's avatar
Stefan Jaax committed
9 10
import Data.Aeson
import Data.Aeson.TH (deriveJSON, defaultOptions)
11 12
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
13
import Text.Parsec
Stefan Jaax's avatar
Stefan Jaax committed
14 15 16
import qualified Data.Set as S
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Text as T
17
import Text.Parsec.Expr
18 19 20
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
21
import PopulationProtocol (PopulationProtocol,makePopulationProtocolFromStrings,State(..),Transition(..))
22 23 24 25 26 27 28 29 30 31
import Property

languageDef :: LanguageDef ()
languageDef =
        emptyDef {
                 Token.commentStart    = "/*",
                 Token.commentEnd      = "*/",
                 Token.commentLine     = "//",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> char '_',
32
                 Token.reservedNames   = ["true", "false", "EXISTS", "FORALL"],
33
                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "=%", "!=%",
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 71 72 73 74 75 76 77 78
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

79 80 81 82
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 )
83

84
termOperatorTable :: [[Operator String () Identity (Term String)]]
85 86
termOperatorTable =
        [ [ prefix "-" Minus ]
87
        , [ binary "*" (:*:) AssocLeft, binary "/" (:/:) AssocLeft, binary "%" (:%:) AssocLeft ]
88 89 90
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

91
termAtom :: Parser (Term String)
92
termAtom =  (Var <$> ident)
93
        <|> (Const <$> integer)
94 95
        <|> parens term
        <?> "basic term"
96

97
term :: Parser (Term String)
98
term = buildExpressionParser termOperatorTable termAtom <?> "term"
99 100 101 102 103

parseOp :: Parser Op
parseOp = (reservedOp "<" *> return Lt) <|>
          (reservedOp "<=" *> return Le) <|>
          (reservedOp "=" *> return Eq) <|>
104
          (reservedOp "!=" *> return Ne) <|>
105
          (reservedOp ">" *> return Gt) <|>
106 107
          (reservedOp "=%" *> (ModEq <$> integer)) <|>
          (reservedOp "!=%" *> (ModNe <$> integer))
108

109
linIneq :: Parser (Formula String)
110
linIneq = do
111 112 113
        lhs <- term
        op <- parseOp
        rhs <- term
114
        return (LinearInequation lhs op rhs)
115

116
formOperatorTable :: [[Operator String () Identity (Formula String)]]
117 118 119 120 121
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]
122

123
formAtom :: Parser (Formula String)
124
formAtom =  try linIneq
125 126
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
127 128
        <|> parens formula
        <?> "basic formula"
129

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

133 134 135 136 137 138 139 140 141 142 143 144
quantFormula :: Parser (QuantFormula String)
quantFormula =
        (do
            reserved "EXISTS"
            xs <- optionalCommaSep ident
            reservedOp ":"
            p <- formula
            return (ExQuantFormula xs p)
        )
          <|>
        (ExQuantFormula [] <$> formula)

145 146 147 148 149 150 151 152 153 154 155
instance FromJSON (Formula String) where
          parseJSON (String v) = do
                  let f = parse formula "" (T.unpack v)
                  case f of
                    Left e -> fail "Predicate formula not well-formed."
                    Right r -> return r
          parseJSON _ = fail "Expect string for predicate."

instance ToJSON (Formula String) where
        toJSON x = String ""

Stefan Jaax's avatar
Stefan Jaax committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
instance FromJSON (QuantFormula String) where
          parseJSON (String v) = do
                  let formula = parse quantFormula "" (T.unpack v)
                  case formula of
                    Left e -> fail "Predicate formula not well-formed."
                    Right r -> return r
          parseJSON _ = fail "Expect string for predicate."

instance ToJSON (QuantFormula String) where
        toJSON x = String ""

data RecordTransition = RecordTransition { 
        name :: String,
        pre :: [String],
        post :: [String]
} deriving (Show)

data RecordPP = RecordPP { 
        title :: String,
        states :: [String],
        transitions :: [RecordTransition],
        initialStates :: [String],
        trueStates :: [String],
179
        precondition :: Maybe (Formula String),
180
        predicate :: Maybe (QuantFormula String),
Stefan Jaax's avatar
Stefan Jaax committed
181
        description :: Maybe String
Stefan Jaax's avatar
Stefan Jaax committed
182 183 184 185 186 187
} deriving (Show)

$(deriveJSON defaultOptions ''RecordTransition)
$(deriveJSON defaultOptions ''RecordPP)

recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
188
recordPP2PopulationProtocol r =
189
  makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p precond arcs where
Stefan Jaax's avatar
Stefan Jaax committed
190
        falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
191
        arcs = [(q, name t, 1) |  t <- transitions r, q <- pre t] ++
Stefan Jaax's avatar
Stefan Jaax committed
192
               [(name t, q, 1) | t <- transitions r, q <- post t]
193
        p = case predicate r of Nothing -> ExQuantFormula [] FTrue
Stefan Jaax's avatar
Stefan Jaax committed
194
                                (Just p') -> p'
195 196
        precond = case precondition r of Nothing -> FTrue
                                         (Just p') -> p'
Philipp Meyer's avatar
Philipp Meyer committed
197 198

parseContent :: Parser PopulationProtocol
199
parseContent  = do
Stefan Jaax's avatar
Stefan Jaax committed
200 201 202 203 204
  str <- manyTill anyChar eof
  let r = eitherDecode (BS.pack str)
  case r of
    (Left e) ->  fail e
    (Right pp) -> return (recordPP2PopulationProtocol pp)
205

Stefan Jaax's avatar
Stefan Jaax committed
206