-
Notifications
You must be signed in to change notification settings - Fork 1
/
parsing.maude
405 lines (318 loc) · 14.1 KB
/
parsing.maude
1
2
3
4
5
6
7
8
9
10
11
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
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
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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
***(
PARSING.MAUDE
This module defines a meta level functional module that represents the Core-Erlang syntax
definition. The metaParse function (included from META-LEVEL) uses the grammar defined here
to parse Core-Erlang source-code that is input as a list of quoted identifiers.
Due to limitations in the current implementation, we have to insert whitespaces into the
Core-Erlang code as generated by the erlang compiler before and after those characters
(when they are used as brackets or to separate atoms, etc.)
"/", ":", "<", ">"
These characters are not recognized as separators by the Maude parser. Therefore Core-Erlang
function names, written without whitespace, such as "funname/2" would be treated as one quoted
identifier instead of the "_/_" operator of arity two in mix-fix notation. Such an interpretation
leads to syntax errors, of course.
***)
----------------------------------------------------------------------------------------------------
---
--- PRINT-SYNTAX-ERROR
---
--- Some functions to print out the position at which a syntax error is reported by
--- the metaParse function. This code is taken from the Full-Mode implementation.
---
----------------------------------------------------------------------------------------------------
fmod PRINT-SYNTAX-ERROR is
protecting META-LEVEL .
protecting INT .
var QIL : QidList .
var Q : Qid .
var N : Nat .
vars RP RP' : ResultPair .
var RP? : [ResultPair?] .
op printN : Nat QidList -> QidList . *** first N qid's in a qidList
eq printN(N, nil) = nil .
eq printN(0, QIL) = nil .
eq printN(s N, Q QIL) = Q printN(N, QIL) .
op removeFront : Nat QidList -> QidList . *** removes first N qid's
eq removeFront(N, nil) = nil .
eq removeFront(0, QIL) = QIL .
eq removeFront(s N, Q QIL) = removeFront(N, QIL) .
op printSyntaxError : [ResultPair?] QidList -> QidList .
eq printSyntaxError(noParse(N), QIL)
= '\r 'Parse 'error 'in '\o '\s printN(N + 1, QIL) '\r '<---*HERE* '\o .
eq printSyntaxError(ambiguity(RP, RP'), QIL)
= '\r 'Ambiguous 'parsing 'for '\o '\s QIL '\o .
eq printSyntaxError(RP?, QIL) = QIL [owise] .
endfm
----------------------------------------------------------------------------------------------------
---
--- SYNTAX-HELPER
---
----------------------------------------------------------------------------------------------------
fmod SYNTAX-HELPER is
protecting RAT .
protecting FLOAT .
protecting INT .
protecting STRING .
protecting CONVERSION .
protecting QID .
protecting META-LEVEL .
*** core-erlang atoms
op syntaxCheckAtom : Term -> Bool .
op getAtom : Term -> String .
*** core-erlang variable names
op syntaxCheckVar : Term -> Bool .
op getVar : Term -> String .
*** core-erlang characters
op syntaxCheckChar : Term -> Bool .
op getChar : Term -> Char .
*** core-erlang strings
op syntaxCheckString : Term -> Bool .
op getString : Term -> String .
*** core-erlang integers
op syntaxCheckInt : Term -> Bool .
op getInt : Term -> Int .
*** core-erlang floats
op syntaxCheckFloat : Term -> Bool .
op getFloat : Term -> Float .
sort CharSet .
subsort Char < CharSet .
op _,_ : CharSet CharSet -> CharSet [ctor comm assoc] .
op intCharSet : -> CharSet .
op signCharSet : -> CharSet .
op stringCharSet : -> CharSet .
op characterSet : String CharSet -> Bool .
op downQid : Qid -> Qid .
var Str : String .
var T : Term .
var QID : Qid .
var EndPos : Int .
var Chr Chr1 Chr2 : Char .
var Set : CharSet .
eq intCharSet = "0","1","2","3","4","5","6","7","8","9" .
eq signCharSet = "-", "+" .
eq characterSet("", Set) = true .
eq characterSet(Chr, Chr1) = if (Chr == Chr1) then true else false fi .
eq characterSet(Chr, (Chr1, Set)) = if (Chr == Chr1) then true else characterSet(Chr, Set) fi .
eq characterSet(Str, Set) =
if characterSet(substr(Str, 0, 1), Set) then characterSet(substr(Str, 1, length(Str) + (-1)), Set) else false fi .
ceq downQid( QID ) = qid(substr(Str, 1, length(Str)))
if Str := string(QID) /\ substr(Str, 0, 1) == "'" .
*** core-erlang atoms
ceq syntaxCheckAtom('token[T]) = (substr(Str, 0, 1) == "'") and (substr(Str, EndPos, 1) == "'")
if Str := string(downQid(getName(T))) /\ EndPos := length(Str) + (-1) .
ceq getAtom('token[T]) = substr(Str, 1, EndPos)
if Str := string(downQid(getName(T))) /\ EndPos := length(Str) + (-2) /\ syntaxCheckAtom('token[T]) .
*** core-erlang variable names
ceq syntaxCheckVar('token[T]) = ((ascii(Chr) >= 65) and (ascii(Chr) <= 90)) or (ascii(Chr) == 95)
if Chr := substr(string(downQid(getName(T))), 0, 1) .
ceq getVar('token[T]) = string(downQid(getName(T)))
if syntaxCheckVar('token[T]) .
*** core-erlang characters
ceq syntaxCheckChar('token[T]) = (substr(Str, 0, 1) == "'") and (substr(Str, 2, 1) == "'")
if Str := string(downQid(getName(T))) /\ (length(Str) == 2) .
ceq getChar('token[T]) = substr(Str, 1, 1)
if Str := string(downQid(getName(T))) /\ syntaxCheckAtom('token[T]) .
*** core-erlang strings
ceq syntaxCheckString('token[T]) = (substr(Str, 0, 1) == "\"") and (substr(Str, EndPos, 1) == "\"")
if Str := string(downQid(getName(T))) /\ EndPos := length(Str) + (-1) .
ceq getString('token[T]) = string(downQid(getName(T)))
if syntaxCheckString('token[T]) .
*** core-erlang integers
ceq syntaxCheckInt('token[T]) = (characterSet(substr(Str, 0, 1), signCharSet) and characterSet(substr(Str, 1, length(Str) + (-1)), intCharSet))
or (characterSet(substr(Str,0,length(Str)), intCharSet))
if Str := string(downQid(getName(T))) .
ceq getInt('token[T]) = rat(string(downQid(getName(T))),10)
if syntaxCheckInt('token[T]) .
*** core-erlang floats
*** - not implemented -
*** core-erlang token lists
*** - not implemented -
endfm
----------------------------------------------------------------------------------------------------
---
--- COMMON-SYNTAX-DOWN
---
--- This functional module converts the Core-Erlang program from the meta-level (level 1)
--- back to the object level (level 0).
---
----------------------------------------------------------------------------------------------------
fmod COMMON-SYNTAX-DOWN is
protecting SYNTAX .
protecting QID .
protecting META-TERM .
protecting META-LEVEL .
protecting STRING .
protecting INT .
protecting CONVERSION .
protecting SYNTAX-HELPER .
op GRAMMAR : -> FModule .
op #downModule : Term -> ErlModule [memo] .
op #downAtom : Term -> Atom [memo] .
op #downVar : Term -> Atom [memo] .
op #downErlInt : Term -> ErlInt [memo] .
op #downModuleBody : Term -> ModuleBody [memo] .
op #downNeFunDefList : Term -> NeFunDefList [memo] .
op #downFunDef : Term -> FunDef [memo] .
op #downFun : Term -> Fun [memo] .
op #downFunName : Term -> FunName [memo] .
op #downTimeoutClause : Term -> TimeoutClause [memo] .
op #downNeVarList : Term -> NeVarList [memo] .
op #downExpr : Term -> Expr [memo] .
op #downClause : Term -> Clause [memo] .
op #downPatterns : Term -> Patterns [memo] .
op #downNeClauseList : Term -> NeClauseList [memo] .
op #downVariables : Term -> Variables [memo] .
op #downVarSeq : Term -> VarSeq [memo] .
op #downOSeq : Term -> OSeq [memo] .
op #downNeSingleExprList : Term -> NeSingleExprList [memo] .
op #downSingleExpr : Term -> SingleExpr [memo] .
op #downNeExprList : Term -> NeExprList [memo] .
op #downList : Term -> ErlList [memo] .
op #downTuple : Term -> ErlTuple [memo] .
vars T1 T2 T3 T4 : Term .
var SUB : Substitution .
eq #downModule('module_`[_`]__end[T1,T2,T3,T4]) = module #downAtom(T1) [] attributes [] #downModuleBody(T4) end .
eq #downModuleBody(T1) = #downNeFunDefList(T1) .
eq #downNeFunDefList('_/_=_[T1,T2,T3]) = #downFunDef('_/_=_[T1,T2,T3]) .
ceq #downNeFunDefList(T1) = #downFunDef(T2) #downNeFunDefList(T3)
if SUB := metaMatch(GRAMMAR, '__['F:FunDef, 'FL:NeFunDefList], T1, nil, 0)
/\ 'F:FunDef <- T2 ; 'FL:NeFunDefList <- T3 := SUB .
eq #downFunDef('_/_=_[T1,T2,T3]) = #downAtom(T1) / #downErlInt(T2) = #downFun(T3) .
eq #downFun('fun`(_`)->_[T1,T2]) = fun(#downNeVarList(T1)) -> #downExpr(T2) .
eq #downFun('fun`(`)->_[T1]) = fun() -> #downExpr(T1) .
eq #downFunName('_/_[T1,T2]) = #downExpr(T1) / #downExpr(T2) .
eq #downTimeoutClause('after_->_[T1,T2]) = after #downExpr(T1) -> #downExpr(T2) .
ceq #downNeVarList(T1) = #downVar(T2) , #downNeVarList(T3)
if SUB := metaMatch(GRAMMAR, '_`,_['V:Var, 'VL:NeVarList], T1, nil, 0)
/\ 'V:Var <- T2 ; 'VL:NeVarList <- T3 := SUB .
eq #downNeVarList(T1) = #downVar(T1) [owise] .
eq #downExpr('<>.EmptySeq) = <> .
eq #downExpr('<_>[T1]) = #downOSeq('<_>[T1]) .
eq #downExpr(T1) = #downSingleExpr(T1) .
eq #downVariables(T1) = #downVarSeq(T1) .
eq #downVarSeq('<>.EmptySeq) = <> .
eq #downVarSeq('<_>[T1]) = #downNeVarList(T1) .
eq #downVarSeq(T1) = #downVar(T1) .
eq #downOSeq('<>.EmptySeq) = <> .
eq #downOSeq('<_>[T1]) = < #downNeSingleExprList(T1) > .
ceq #downNeSingleExprList(T1) = #downSingleExpr(T2), #downNeSingleExprList(T3)
if SUB := metaMatch(GRAMMAR, '_`,_['E:SingleExpr, 'EL:NeSingleExprList], T1, nil, 0)
/\ 'E:SingleExpr <- T2 ; 'EL:NeSingleExprList <- T3 := SUB .
eq #downNeSingleExprList(T1) = #downSingleExpr(T1) [owise] .
ceq #downNeExprList(T1) = #downExpr(T2), #downNeExprList(T3)
if SUB := metaMatch(GRAMMAR, '_`,_['E:Expr, 'EL:NeExprList], T1, nil, 0)
/\ 'E:Expr <- T2 ; 'EL:NeExprList <- T3 := SUB .
eq #downNeExprList(T1) = #downExpr(T1) [owise] .
ceq #downNeClauseList(T1) = #downClause(T2) #downNeClauseList(T3)
if SUB := metaMatch(GRAMMAR, '__['C:Clause, 'CL:NeClauseList], T1, nil, 0)
/\ 'C:Clause <- T2 ; 'CL:NeClauseList <- T3 := SUB .
eq #downNeClauseList(T1) = #downClause(T1) [owise] .
eq #downClause('_when_->_[T1,T2,T3]) = #downPatterns(T1) when #downExpr(T2) -> #downExpr(T3) .
eq #downPatterns('<>.EmptySeq) = <> .
eq #downPatterns('<_>[T1]) = < #downNeExprList(T1) > .
eq #downPatterns(T1) = #downExpr(T1) [owise] .
eq #downSingleExpr('case_of_end[T1,T2]) = case #downExpr(T1) of #downNeClauseList(T2) end .
eq #downSingleExpr('let_=_in_[T1,T2,T3]) = let #downVariables(T1) = #downExpr(T2) in #downExpr(T3) .
eq #downSingleExpr('letrec_in_[T1,T2]) = letrec #downNeFunDefList(T1) in #downExpr(T2) .
eq #downSingleExpr('call_:_`(`)[T1,T2]) = call #downAtom(T1) : #downAtom(T2) () .
eq #downSingleExpr('call_:_`(_`)[T1,T2,T3]) = call #downAtom(T1) : #downAtom(T2) (#downNeExprList(T3)) .
eq #downSingleExpr('apply_`(`)[T1]) = apply #downSingleExpr(T1) () .
eq #downSingleExpr('apply_`(_`)[T1,T2]) = apply #downSingleExpr(T1) (#downNeExprList(T2)) .
eq #downSingleExpr('do__[T1,T2]) = do #downExpr(T1) #downExpr(T2) .
eq #downSingleExpr('receive__[T1,T2]) = receive #downNeClauseList(T1) #downTimeoutClause(T2) .
eq #downSingleExpr('fun`(`)->_[T1]) = #downFun('fun`(`)->_[T1]) .
eq #downSingleExpr('fun`(_`)->_[T1,T2]) = #downFun('fun`(_`)->_[T1,T2]) .
eq #downSingleExpr('_/_[T1,T2]) = #downFunName('_/_[T1,T2]) .
eq #downSingleExpr('`[`].Nil) = [] .
eq #downSingleExpr('`{_`}[T1]) = #downTuple('`{_`}[T1]) .
eq #downSingleExpr('`{`}.TupleConstl) = {} .
eq #downSingleExpr('`[_`][T1]) = #downList('`[_`][T1]) .
eq #downSingleExpr('`[_|_`][T1,T2]) = #downList('`[_|_`][T1,T2]) .
eq #downSingleExpr('<>.EmptySeq) = <> .
eq #downSingleExpr('primop_`(_`)[T1,T2]) = primop #downAtom(T1) (#downNeExprList(T2)) .
eq #downSingleExpr('primop_`(`)[T1]) = primop #downAtom(T1) () .
eq #downSingleExpr('catch_[T1]) = catch #downExpr(T1) .
eq #downTuple('`{_`}[T1]) = {#downNeExprList(T1)} .
eq #downTuple('`{`}.TupleConst) = {} .
eq #downList('`[_`][T1]) = [#downNeExprList(T1)] .
eq #downList('`[_|_`][T1,T2]) = [#downExpr(T1) | #downExpr(T2)] .
endfm
fmod PARSING-SYNTAX-DOWN is
including COMMON-SYNTAX-DOWN .
op #downErlString : Term -> ListConst [memo] .
op #downErlChar : Term -> ErlInt [memo] .
eq GRAMMAR =
(mod 'GRAMMAR is
including 'QID-LIST .
including 'COMMAND-GRAMMAR .
including 'PARSING-SYNTAX .
including 'PREDICATES .
including 'LTL-FORMULAE .
sorts none .
none
op 'token : 'Qid -> 'Token
[ctor special(
(id-hook('Bubble, '1 '1)
op-hook('qidSymbol, '<Qids>, nil, 'Qid)
id-hook('Exclude, 'module 'end '-| '-> 'attributes 'catch 'do
'receive 'after 'try 'of 'case 'let 'letrec
'fun 'primop 'apply 'when '`[ '`] '`, '`. '= '/
'/ '< '> '`( '`) '`} '`{ '`{`} '`(`) '`[`] '<>)))
format ('b 'o)] .
none
none
none
endm) .
var T : Term .
var INT : Int .
var STR : String .
eq #downAtom('token[T]) = atom(substr(string(getName(T)), 2, length(string(getName(T))) + (-3))) .
eq #downVar('token[T]) = var(substr(string(getName(T)), 1, length(string(getName(T))))) .
eq #downErlInt('token[T]) = int(rat(substr(string(getName(T)), 1, length(string(getName(T)))), 10)) .
eq #downErlString('token[T])
= #builtStringList(substr(string(getName(T)), 2, length(string(getName(T))) + (-3))) .
op #builtStringList : String -> ListConst .
eq #builtStringList("") = [] .
eq #builtStringList(STR)
= [ int(ascii(substr(STR, 0, 1))) | #builtStringList(substr(STR, 1, length(STR) + -1))] [owise] .
ceq #downSingleExpr('token[T]) = #downAtom('token[T])
if syntaxCheckAtom('token[T]) .
ceq #downSingleExpr('token[T]) = #downVar('token[T])
if syntaxCheckVar('token[T]) .
ceq #downSingleExpr('token[T]) = #downErlInt('token[T])
if syntaxCheckInt('token[T]) .
ceq #downSingleExpr('token[T]) = #downErlString('token[T])
if syntaxCheckString('token[T]) .
endfm
fmod MAUDE-SYNTAX-DOWN is
protecting META-UP-DOWN .
including COMMON-SYNTAX-DOWN .
eq GRAMMAR =
(mod 'GRAMMAR is
including 'QID-LIST .
including 'SYNTAX .
including 'SEM_PROCESSES .
including 'SEM_MODENV .
including 'SEM_PID_SEQUENCE .
including 'SEM_MAILBOX .
including 'PREDICATES .
including 'LTL-FORMULAE .
sorts none .
none
none
none
none
none
endm) .
var T : Term .
eq #downAtom('atom[T]) = atom(#downString(T)) .
eq #downVar('var[T]) = var(#downString(T)) .
eq #downErlInt('int[T]) = int(#downInt(T)) .
eq #downSingleExpr('atom[T]) = atom(#downString(T)) .
eq #downSingleExpr('var[T]) = var(#downString(T)) .
eq #downSingleExpr('int[T]) = int(#downInt(T)) .
endfm
fmod MAUDE-SYNTAX-UPDOWN is
protecting MAUDE-SYNTAX-UP .
protecting MAUDE-SYNTAX-DOWN .
endfm