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
                 }
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 87 88 89 90
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ 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)

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

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

recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
recordPP2PopulationProtocol r = 
Stefan Jaax's avatar
Stefan Jaax committed
176
  makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p  arcs where
Stefan Jaax's avatar
Stefan Jaax committed
177
        falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
Stefan Jaax's avatar
Stefan Jaax committed
178 179
        arcs = [(q, name t, 1) |  t <- transitions r, q <- pre t] ++ 
               [(name t, q, 1) | t <- transitions r, q <- post t]
Stefan Jaax's avatar
Stefan Jaax committed
180 181
        p = case predicate r of Nothing -> ExQuantFormula [] FTrue 
                                (Just p') -> p'
Philipp Meyer's avatar
Philipp Meyer committed
182 183

parseContent :: Parser PopulationProtocol
Stefan Jaax's avatar
Stefan Jaax committed
184 185 186 187 188 189 190 191
parseContent  = do 
  str <- manyTill anyChar eof
  let r = eitherDecode (BS.pack str)
  case r of
    (Left e) ->  fail e
    (Right pp) -> return (recordPP2PopulationProtocol pp)