PP.hs 7.11 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) <|>
Philipp Meyer's avatar
Philipp Meyer committed
106
          (reservedOp ">=" *> return Ge) <|>
107 108
          (reservedOp "=%" *> (ModEq <$> integer)) <|>
          (reservedOp "!=%" *> (ModNe <$> integer))
109

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

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

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

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

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

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

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

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

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

Stefan Jaax's avatar
Stefan Jaax committed
207