Parser.hs 6.31 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
4
module Parser
    (parseString, parseFile)
where

Philipp Meyer's avatar
Philipp Meyer committed
5
import Control.Applicative ((<*),(*>),(<*>),(<$>))
Philipp Meyer's avatar
Philipp Meyer committed
6
7
8
9
10
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import PetriNet (PetriNet,makePetriNet)
Philipp Meyer's avatar
Philipp Meyer committed
11
import Property
Philipp Meyer's avatar
Philipp Meyer committed
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

type Parser u a = Parsec String u a

languageDef :: LanguageDef u
languageDef =
        emptyDef {
                 Token.commentStart    = "/*",
                 Token.commentEnd      = "*/",
                 Token.commentLine     = "//",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> char '_',
                 Token.reservedNames   = [],
                 Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">",
                                          "+", "-", "*", "&", "|", "!"]
                 }

lexer :: Token.TokenParser u
lexer = Token.makeTokenParser languageDef

identifier :: Parser u String
identifier = Token.identifier lexer -- parses an identifier
stringLiteral :: Parser u String
stringLiteral = Token.stringLiteral lexer -- parses a string literal
reserved :: String -> Parser u ()
reserved   = Token.reserved   lexer -- parses a reserved name
reservedOp :: String -> Parser u ()
reservedOp = Token.reservedOp lexer -- parses an operator
brackets :: Parser u a -> Parser u a
brackets   = Token.brackets   lexer -- parses p surrounded by brackets
braces :: Parser u a -> Parser u a
braces     = Token.braces     lexer -- parses p surrounded by braces
Philipp Meyer's avatar
Philipp Meyer committed
43
44
parens :: Parser u a -> Parser u a
parens     = Token.parens     lexer -- parses p surrounded by parenthesis
Philipp Meyer's avatar
Philipp Meyer committed
45
46
natural :: Parser u Integer
natural    = Token.natural    lexer -- parses a natural number
Philipp Meyer's avatar
Philipp Meyer committed
47
48
integer :: Parser u Integer
integer    = Token.integer    lexer -- parses an integer
Philipp Meyer's avatar
Philipp Meyer committed
49
comma :: Parser u String
Philipp Meyer's avatar
Philipp Meyer committed
50
comma      = Token.comma       lexer -- parses a comma
Philipp Meyer's avatar
Philipp Meyer committed
51
52
53
54
55
56
57
whiteSpace :: Parser u ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace

optionalCommaSep :: Parser u a -> Parser u [a]
optionalCommaSep p = many (p <* optional comma)

singleOrList :: Parser u a -> Parser u [a]
Philipp Meyer's avatar
Philipp Meyer committed
58
singleOrList p = braces (optionalCommaSep p) <|> (:[]) <$> p
Philipp Meyer's avatar
Philipp Meyer committed
59
60
61
62
63
64
65
66
67
68
69

numberOption :: Parser u Integer
numberOption = option 1 (brackets natural)

ident :: Parser u String
ident = (identifier <|> stringLiteral) <?> "identifier"

identList :: Parser u [String]
identList = singleOrList ident

places :: Parser u [String]
Philipp Meyer's avatar
Philipp Meyer committed
70
places = reserved "places" *> identList
Philipp Meyer's avatar
Philipp Meyer committed
71
72

transitions :: Parser u [String]
Philipp Meyer's avatar
Philipp Meyer committed
73
transitions = reserved "transitions" *> identList
Philipp Meyer's avatar
Philipp Meyer committed
74
75

initial :: Parser u [(String,Integer)]
Philipp Meyer's avatar
Philipp Meyer committed
76
initial = reserved "initial" *> singleOrList (do
Philipp Meyer's avatar
Philipp Meyer committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
            n <- ident
            i <- numberOption
            return (n,i)
          )

arc :: Parser u [(String,String,Integer)]
arc = do
        lhs <- identList
        rhsList <- many1 (do
                reservedOp "->"
                w <- numberOption
                ids <- identList
                return (ids,w)
            )
        return $ fst $ foldl makeArc ([],lhs) rhsList
      where
        makeArc (as,lhs) (rhs,w) = ([(l,r,w) | l <- lhs, r <- rhs] ++ as, rhs)

arcs :: Parser u [(String,String,Integer)]
arcs = do
        reserved "arcs"
        as <- singleOrList arc
        return $ concat as

data Statement = Places [String] | Transitions [String] |
                 Arcs [(String,String,Integer)] | Initial [(String,Integer)]

statement :: Parser u Statement
Philipp Meyer's avatar
Philipp Meyer committed
105
106
107
108
statement = Places <$> places <|>
            Transitions <$> transitions <|>
            Arcs <$> arcs <|>
            Initial <$> initial
Philipp Meyer's avatar
Philipp Meyer committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

petriNet :: Parser u PetriNet
petriNet = do
            reserved "petri"
            reserved "net"
            name <- option "" ident
            statements <- braces (many statement)
            let (p,t,a,i) = foldl splitStatement ([],[],[],[]) statements
            return $ makePetriNet name p t a i
        where
            splitStatement (ps,ts,as,is) stmnt = case stmnt of
                  Places p -> (p ++ ps,ts,as,is)
                  Transitions t -> (ps,t ++ ts,as,is)
                  Arcs a -> (ps,ts,a ++ as,is)
                  Initial i -> (ps,ts,as,i ++ is)

Philipp Meyer's avatar
Philipp Meyer committed
125
126
127
128
129
preFactor :: Parser u Integer
preFactor = (reservedOp "-" *> return (-1)) <|>
            (reservedOp "+" *> return 1)

linAtom :: Integer -> Parser u LinAtom
130
131
132
linAtom fac = ( integer >>= \lhs ->
                option (Const (fac*lhs)) $ Var (fac*lhs) <$> (reservedOp "*" *> ident)
              ) <|> Var fac <$> ident
Philipp Meyer's avatar
Philipp Meyer committed
133
134
135

term :: Parser u Term
term = Term <$> ((:) <$> (option 1 preFactor >>= linAtom) <*>
136
                         many (preFactor >>= linAtom))
Philipp Meyer's avatar
Philipp Meyer committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183

parseOp :: Parser u Op
parseOp = (reservedOp "<" *> return Lt) <|>
          (reservedOp "<=" *> return Le) <|>
          (reservedOp "=" *> return Eq) <|>
          (reservedOp ">" *> return Gt) <|>
          (reservedOp ">=" *> return Ge)

atom :: Parser u Formula
atom = do
        lhs <- term
        op <- parseOp
        rhs <- term
        return (Atom (LinIneq lhs op rhs))

parensForm :: Parser u Formula
parensForm = atom <|> parens formula

negation :: Parser u Formula
negation = (Neg <$> (reservedOp "!" *> negation)) <|> parensForm

conjunction :: Parser u Formula
conjunction = do
        lhs <- negation
        option lhs ((lhs :&:) <$> (reservedOp "&" *> conjunction))

disjunction :: Parser u Formula
disjunction = do
        lhs <- conjunction
        option lhs ((lhs :|:) <$> (reservedOp "|" *> disjunction))

formula :: Parser u Formula
formula = disjunction

propertyType :: Parser u PropertyType
propertyType =
        (reserved "safety" *> return Safety) <|>
        (reserved "liveness" *> return Liveness)

property :: Parser u Property
property = do
        ptype <- propertyType
        reserved "property"
        name <- option "" ident
        pformulas <- braces formula
        return $ Property name ptype pformulas

184
185
186
187
188
189
190
parseContent :: Parser u (PetriNet,[Property])
parseContent = do
        whiteSpace
        net <- petriNet
        properties <- many property
        eof
        return (net, properties)
Philipp Meyer's avatar
Philipp Meyer committed
191

192
parseString :: String -> (PetriNet,[Property])
Philipp Meyer's avatar
Philipp Meyer committed
193
parseString str =
Philipp Meyer's avatar
Philipp Meyer committed
194
        case parse parseContent "" str of
Philipp Meyer's avatar
Philipp Meyer committed
195
196
197
            Left e -> error $ show e
            Right r -> r

198
parseFile :: String -> IO (PetriNet,[Property])
Philipp Meyer's avatar
Philipp Meyer committed
199
200
parseFile file =  do
        contents <- readFile file
Philipp Meyer's avatar
Philipp Meyer committed
201
        case parse parseContent file contents of
Philipp Meyer's avatar
Philipp Meyer committed
202
203
            Left e -> print e >> fail "parse error"
            Right r -> return r