PP.hs 6.99 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
                 }
Stefan Jaax's avatar
Stefan Jaax committed
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 106 107
          (reservedOp ">" *> return Gt) <|>
          (reservedOp ">=" *> return Ge)

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

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

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

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

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

144 145 146 147 148 149 150 151 152 153 154
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
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
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],
178
        precondition :: Maybe (Formula String),
179
        predicate :: Maybe (QuantFormula String),
Stefan Jaax's avatar
Stefan Jaax committed
180
        description :: Maybe String
Stefan Jaax's avatar
Stefan Jaax committed
181 182 183 184 185 186
} deriving (Show)

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

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

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

Stefan Jaax's avatar
Stefan Jaax committed
205