PP.hs 6.38 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
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
145 146 147 148 149 150 151 152 153 154 155 156
data RecordTransition = RecordTransition { 
        name :: String,
        pre :: [String],
        post :: [String]
} deriving (Show)

data RecordPP = RecordPP { 
        title :: String,
        states :: [String],
        transitions :: [RecordTransition],
        initialStates :: [String],
        trueStates :: [String],
157
        precondition :: Maybe (Formula String),
158
        predicate :: Maybe (Formula String),
Stefan Jaax's avatar
Stefan Jaax committed
159
        description :: Maybe String
Stefan Jaax's avatar
Stefan Jaax committed
160 161 162 163 164 165
} deriving (Show)

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

recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
166
recordPP2PopulationProtocol r =
167
  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
168
        falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
169
        arcs = [(q, name t, 1) |  t <- transitions r, q <- pre t] ++
Stefan Jaax's avatar
Stefan Jaax committed
170
               [(name t, q, 1) | t <- transitions r, q <- post t]
171
        p = case predicate r of Nothing -> FTrue
Stefan Jaax's avatar
Stefan Jaax committed
172
                                (Just p') -> p'
173 174
        precond = case precondition r of Nothing -> FTrue
                                         (Just p') -> p'
Philipp Meyer's avatar
Philipp Meyer committed
175 176

parseContent :: Parser PopulationProtocol
177
parseContent  = do
Stefan Jaax's avatar
Stefan Jaax committed
178 179 180 181 182
  str <- manyTill anyChar eof
  let r = eitherDecode (BS.pack str)
  case r of
    (Left e) ->  fail e
    (Right pp) -> return (recordPP2PopulationProtocol pp)
183

Stefan Jaax's avatar
Stefan Jaax committed
184