1
|
/*
|
2
|
ANTLR Grammar for OO-Action Systems
|
3
|
(C) Willibald Krenn, 2009 - 2015
|
4
|
|
5
|
|
6
|
Notes
|
7
|
~~~~~
|
8
|
(*) No recursion
|
9
|
(*) float acutally is fixed-point!
|
10
|
(*) Named actions can only be "called" within the do-od block
|
11
|
(*) Methods can be called from within an action and a method.
|
12
|
Attention: Mutual Recursion not supported!
|
13
|
|
14
|
FixMe
|
15
|
~~~~~
|
16
|
(*) List-Enum: Length Restriction! (Defaults to 500 for now)
|
17
|
(*) subseteq missing
|
18
|
|
19
|
|
20
|
|
21
|
History
|
22
|
~~~~~~~
|
23
|
Changes 1.09 to 1.10
|
24
|
- allow actions to be declared with empty parameter lists and "()"
|
25
|
|
26
|
Changes 1.08 to 1.09
|
27
|
~ fix actionBody rule to allow multiple prioritized compositions (replace "?" by "*")
|
28
|
|
29
|
Changes 1.07 to 1.08
|
30
|
~ remove support for Qualitative Action Systems
|
31
|
|
32
|
Changes 1.06 to 1.07
|
33
|
~ move to org.momut naming
|
34
|
|
35
|
Changes 1.05 to 1.06
|
36
|
~ make action blocks more capable, add the projection feature already available in the do-od block.
|
37
|
- disable support for continuous actions
|
38
|
|
39
|
Changes 1.04 to 1.05
|
40
|
~ Fix bug with set constuctor: set with only one element produced wrong AST (inner element wasn't added correctly).
|
41
|
|
42
|
Changes 1.03 to 1.04
|
43
|
~ Move to JAVA
|
44
|
|
45
|
Changes 1.02 to 1.03
|
46
|
+ option to name objects when they are constructed: new (<class>,"<name>")
|
47
|
|
48
|
Changes 1.00 to 1.02
|
49
|
+ cast operator for objects ( ... as <typename> )
|
50
|
|
51
|
Changes 1.00 to 1.01
|
52
|
+ enum-type with fixed integer values
|
53
|
|
54
|
Changes 0.99b to 1.00
|
55
|
+ constant section added (consts a=4; b=4)
|
56
|
+ limits of simple types and lists can be const
|
57
|
+ local vars allowed in methods (... = var... begin...end)
|
58
|
+ prioritized composition on statement level
|
59
|
+ skip in do-od block
|
60
|
+ filter expression in do-od block sequential var statement
|
61
|
+ fold operator
|
62
|
|
63
|
Changes 0.99 to 0.99b
|
64
|
- disabled sequential composition of action systems (remains in grammar, though out-commented)
|
65
|
|
66
|
Changes 0.98 to 0.99
|
67
|
~ changed QR syntax.
|
68
|
|
69
|
Changes 0.97 to 0.98
|
70
|
~ changed syntax for list and set comprehension
|
71
|
list comprehension:
|
72
|
'[' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? ']'
|
73
|
set comprehension
|
74
|
'{' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? '}'
|
75
|
|
76
|
Usage: defined variables will sweep over value-range. If the latter expression
|
77
|
(after '&') evaluates to true (hence this expression must return a bool) with
|
78
|
the current valuation of the defined vars, the values are used to evaluate the
|
79
|
first expression, which has to return a value of the correct type.
|
80
|
|
81
|
Example:
|
82
|
type
|
83
|
myint = int [0..300000];
|
84
|
mytuple = (myint, myint)
|
85
|
var
|
86
|
l_tuple : list of mytuple = [nil];
|
87
|
l_int : list of myint = [nil];
|
88
|
...
|
89
|
l_int := [l_tuple[x][0] | var x: myint & x < len l_tuple ]
|
90
|
|
91
|
|
92
|
+ list element access by '[int]' allowed!
|
93
|
|
94
|
|
95
|
Changes 0.96 to 0.97
|
96
|
+ tuple-type initialization now properly supported
|
97
|
+ binary operator precedence handling
|
98
|
+ local variables in named actions
|
99
|
+ support for (<expression>).<reference> and
|
100
|
(<expression>).<accessExpression>
|
101
|
~ conditional expression: End required.
|
102
|
- remove support for power-operator
|
103
|
(may be we need to do calculation backwards)
|
104
|
|
105
|
Changes 0.95 to 0.96
|
106
|
~ string literals now ".."
|
107
|
~ priming of identifier access only supported at the end of the
|
108
|
expression
|
109
|
|
110
|
Changes 0.9 to 0.95
|
111
|
+ composition of action systems in 'system' block
|
112
|
~ Produce C# code
|
113
|
~ Operator Precedence
|
114
|
~ vars in action composition
|
115
|
~ forall/extists now with colon instead of in
|
116
|
|
117
|
|
118
|
Earlier changes removed.
|
119
|
|
120
|
*/
|
121
|
|
122
|
|
123
|
grammar ooa;
|
124
|
|
125
|
options {
|
126
|
k = 2;
|
127
|
superClass = ooaCustomParser;
|
128
|
}
|
129
|
|
130
|
|
131
|
@lexer::header
|
132
|
{
|
133
|
/*
|
134
|
Ulysses OO-Action System Parser
|
135
|
|
136
|
Copyright Graz University of Technology 2009
|
137
|
Copyright AIT Austrian Institute of Technology 2013
|
138
|
*/
|
139
|
package org.momut.ooas.parser;
|
140
|
}
|
141
|
|
142
|
|
143
|
@parser::header
|
144
|
{
|
145
|
/*
|
146
|
Ulysses OO-Action System Parser
|
147
|
|
148
|
Copyright Graz University of Technology 2009
|
149
|
Copyright AIT Austrian Institute of Technology 2013, 2016
|
150
|
Version 1.09
|
151
|
*/
|
152
|
package org.momut.ooas.parser;
|
153
|
|
154
|
import org.momut.ooas.ast.expressions.*;
|
155
|
import org.momut.ooas.ast.statements.*;
|
156
|
import org.momut.ooas.ast.identifiers.*;
|
157
|
import org.momut.ooas.ast.types.*;
|
158
|
import org.momut.ooas.ast.types.FunctionType.FunctionTypeEnum;
|
159
|
}
|
160
|
|
161
|
ooActionSystems
|
162
|
: {initializeTopLevelParserState();}
|
163
|
|
164
|
(T_CONSTS namedConstList)?
|
165
|
|
166
|
T_TYPES
|
167
|
namedTypeList
|
168
|
T_SYSTEM
|
169
|
comp=asTypeComposition[null]
|
170
|
{fixUpRun(comp);}
|
171
|
;
|
172
|
|
173
|
|
174
|
|
175
|
//
|
176
|
// ------------ named consts ------------
|
177
|
//
|
178
|
|
179
|
namedConstList
|
180
|
: namedConst (T_SEMICOLON namedConst)*
|
181
|
;
|
182
|
|
183
|
namedConst
|
184
|
: aName=T_IDENTIFIER
|
185
|
T_EQUAL
|
186
|
anExpr=expression
|
187
|
{addNamedConst(aName,anExpr);}
|
188
|
;
|
189
|
|
190
|
|
191
|
//
|
192
|
// ------------ named types ------------
|
193
|
//
|
194
|
namedTypeList
|
195
|
: namedType (T_SEMICOLON namedType)*
|
196
|
;
|
197
|
|
198
|
namedType
|
199
|
: aName=T_IDENTIFIER
|
200
|
T_EQUAL
|
201
|
(
|
202
|
aType=complexType {createNamedType(aName,aType);}
|
203
|
| anOoaType=ooActionSystem {createNamedType(aName,anOoaType);}
|
204
|
)
|
205
|
|
206
|
;
|
207
|
|
208
|
|
209
|
asTypeComposition [IdentifierList top]
|
210
|
returns [IdentifierList prioList]
|
211
|
: {prioList = new PrioIdentifierList(top);}
|
212
|
asTypeCompositionParallel[prioList] (T_PRIO asTypeCompositionParallel[prioList] )*
|
213
|
;
|
214
|
|
215
|
asTypeCompositionParallel [IdentifierList top]
|
216
|
: {IdentifierList parList = new NondetIdentifierList(top);}
|
217
|
asTypeCompositionSequential[parList] (T_NONDET asTypeCompositionSequential[parList])*
|
218
|
;
|
219
|
|
220
|
asTypeCompositionSequential [IdentifierList top]
|
221
|
: {IdentifierList seqList = new SeqIdentifierList(top);}
|
222
|
asTypeCompositionBlockParen[seqList] //(T_SEMICOLON asTypeCompositionBlockParen[seqList])*
|
223
|
;
|
224
|
|
225
|
asTypeCompositionBlockParen [IdentifierList top]
|
226
|
: T_LPAREN asTypeComposition[top] T_RPAREN
|
227
|
| aName=T_IDENTIFIER {addToIdentifierList(top,aName);}
|
228
|
;
|
229
|
|
230
|
|
231
|
//
|
232
|
// ------------ basic types ------------
|
233
|
//
|
234
|
|
235
|
complexType
|
236
|
returns [Type aTypeSymbol]
|
237
|
@init{
|
238
|
aTypeSymbol = null;
|
239
|
}
|
240
|
: T_LIST T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN T_OF innertype=complexType
|
241
|
{aTypeSymbol = createListType(numOfElements,innertype);}
|
242
|
|
243
|
// list type with predefined elements (dupes of each element as many as needed) FIXME: Length Restriction!
|
244
|
| T_LSQPAREN alistelem=T_IDENTIFIER {aTypeSymbol = createListEnumType(alistelem);}
|
245
|
(T_COMMA otherlistelem=T_IDENTIFIER {addToListEnumType(aTypeSymbol,otherlistelem);})* T_RSQPAREN // set of identifiers..
|
246
|
|
247
|
// maps do not really need a length restriction, as simpleType already is restricted..
|
248
|
| T_MAP (T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN)? mapfromtype=simpleType T_TO maptotype=complexType
|
249
|
{aTypeSymbol = createMapType(numOfElements,mapfromtype,maptotype);}
|
250
|
// tuple
|
251
|
| T_LPAREN aType=complexType {aTypeSymbol = createTupleType(aType);}
|
252
|
(T_COMMA anotherType=complexType {addToTupleType(aTypeSymbol,anotherType);})* T_RPAREN
|
253
|
|
254
|
// some simple type (note that this includes identifiers, which may be complex object types..)
|
255
|
| r=simpleType {aTypeSymbol = r;}
|
256
|
;
|
257
|
finally
|
258
|
{fixupComplexType(aTypeSymbol);}
|
259
|
|
260
|
|
261
|
simpleType
|
262
|
returns [Type aTypeSymbol]
|
263
|
@init{
|
264
|
aTypeSymbol = null;
|
265
|
}
|
266
|
: T_BOOL {aTypeSymbol = createBoolType();}
|
267
|
|
268
|
// ints plus subtypes
|
269
|
| T_INT T_LSQPAREN rangeLow=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN
|
270
|
{aTypeSymbol = createIntType(rangeLow,rangeHigh);}
|
271
|
|
272
|
// floats plus subtypes
|
273
|
| T_FLOAT T_LSQPAREN rangeLow=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN
|
274
|
{aTypeSymbol = createFloatType(rangeLow,rangeHigh);}
|
275
|
|
276
|
// char
|
277
|
| T_CHAR {aTypeSymbol = createCharType();}
|
278
|
|
279
|
// simple type, domain restricted to the values within the given set. (operators supported: equal, not equal) - may be casted to integer if
|
280
|
// explicit int values are given
|
281
|
| T_CBRL aRangeValue=T_IDENTIFIER (T_EQUAL optVal=T_INTNUMBER)? {aTypeSymbol = createEnumType(aRangeValue, optVal);}
|
282
|
(T_COMMA otherRangeValue=T_IDENTIFIER (T_EQUAL otherOptVal=T_INTNUMBER)? {addToEnumType(aTypeSymbol,otherRangeValue,otherOptVal); otherOptVal=null;})* T_CBRR
|
283
|
|
284
|
| aType=T_IDENTIFIER {aTypeSymbol = getNamedType(aType);} // alias could be simple type - otherwise, it's a complex type!!
|
285
|
;
|
286
|
finally
|
287
|
{fixupSimpleType(aTypeSymbol);}
|
288
|
|
289
|
|
290
|
|
291
|
|
292
|
|
293
|
|
294
|
ooActionSystem
|
295
|
returns [OoActionSystemType aTypeSymbol]
|
296
|
@init{
|
297
|
boolean autoCons = false;
|
298
|
aTypeSymbol = null;
|
299
|
refinesSystemName = null;
|
300
|
}
|
301
|
: (T_AUTOCONS {autoCons = true;})?
|
302
|
T_SYSTEM (T_LPAREN refinesSystemName=T_IDENTIFIER T_RPAREN)?
|
303
|
{aTypeSymbol = createOoaType(refinesSystemName,autoCons);}
|
304
|
'|['
|
305
|
(T_VAR attrList)?
|
306
|
(T_METHODS methodList)?
|
307
|
(T_ACTIONS namedActionList)?
|
308
|
(T_DO (bl=actionBlock[null] {addActionBlock(aTypeSymbol,bl);})? T_OD)?
|
309
|
']|'
|
310
|
;
|
311
|
finally
|
312
|
{fixupOoaType(aTypeSymbol);}
|
313
|
|
314
|
|
315
|
|
316
|
|
317
|
//
|
318
|
// ------------ variables (objects and simple types) ------------
|
319
|
//
|
320
|
attrList
|
321
|
: {BeginParsingAttributes();}
|
322
|
attr (T_SEMICOLON attr)*
|
323
|
;
|
324
|
finally {
|
325
|
EndParsingAttributes();
|
326
|
}
|
327
|
|
328
|
attr
|
329
|
@init{
|
330
|
boolean isStatic = false;
|
331
|
boolean isCtr = false;
|
332
|
boolean isObs = false;
|
333
|
|
334
|
}
|
335
|
: (T_STATIC {isStatic = true;})? (T_OBS {isObs = true;} | T_CTRL {isCtr = true;})?
|
336
|
varname=T_IDENTIFIER T_COLON aType=complexType (T_EQUAL anExpr=expression)?
|
337
|
{createAttribute(varname, isStatic, isObs, isCtr, aType, anExpr);}
|
338
|
;
|
339
|
|
340
|
//
|
341
|
// ------------ methods ------------
|
342
|
//
|
343
|
methodList
|
344
|
: method (T_SEMICOLON method)*
|
345
|
;
|
346
|
|
347
|
method
|
348
|
@init {
|
349
|
FunctionIdentifier newMethod = null;
|
350
|
}
|
351
|
: mname=T_IDENTIFIER {newMethod = createMethodSymbol(mname);}
|
352
|
(T_LPAREN methodParameterList[newMethod] T_RPAREN)?
|
353
|
(T_COLON rt=complexType {setMethodReturnType(newMethod,rt);})? // actions can not have a return type!!
|
354
|
T_EQUAL
|
355
|
( T_VAR localActionVars[newMethod] 'begin')? // var here always means vars of the method. This disables the var of the actionBody!
|
356
|
// If that is wanted, the user needs to use parens... Alternatively we could force the "begin" which feels cumbersome.
|
357
|
// Using a semantic predicate here triggers a bug in the codegen it seems..
|
358
|
statements=actionBody[null] {addMethodBody(newMethod,statements);}
|
359
|
T_END
|
360
|
;
|
361
|
finally
|
362
|
{popResolveStack(newMethod);}
|
363
|
|
364
|
methodParameterList[FunctionIdentifier newMethod]
|
365
|
: paramName=T_IDENTIFIER T_COLON atype=complexType {addMethodParameter(newMethod,paramName,atype);}
|
366
|
(T_COMMA otherparam=T_IDENTIFIER T_COLON othertype=complexType
|
367
|
{addMethodParameter(newMethod,otherparam,othertype);} )*
|
368
|
;
|
369
|
|
370
|
|
371
|
//
|
372
|
// ------------ named, anonymous actions ------------
|
373
|
//
|
374
|
|
375
|
namedActionList
|
376
|
: namedAction (T_SEMICOLON namedAction)*
|
377
|
;
|
378
|
|
379
|
namedAction
|
380
|
@init {
|
381
|
FunctionTypeEnum actionType;
|
382
|
FunctionIdentifier newAction = null;
|
383
|
}
|
384
|
: {actionType = FunctionTypeEnum.Internal;}
|
385
|
(T_CTRL {actionType = FunctionTypeEnum.Controllable;}| T_OBS {actionType = FunctionTypeEnum.Observable;}| )
|
386
|
actionname=T_IDENTIFIER {newAction = createNamedAction(actionname,actionType);}
|
387
|
(T_LPAREN methodParameterList[newAction]? T_RPAREN)?
|
388
|
T_EQUAL
|
389
|
(T_VAR localActionVars[newAction] )?
|
390
|
body=discreteActionBody
|
391
|
{addActionBody(newAction,body);}
|
392
|
;
|
393
|
finally
|
394
|
{popResolveStack(newAction);}
|
395
|
|
396
|
|
397
|
localActionVars[FunctionIdentifier newMethod]
|
398
|
: // a named, discrete action may have local variables.
|
399
|
id1=T_IDENTIFIER T_COLON t1=complexType {addLocalVariableToNamedAction(newMethod,id1,t1);}
|
400
|
(T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType
|
401
|
{addLocalVariableToNamedAction(newMethod,id2,t2);} )*
|
402
|
;
|
403
|
|
404
|
|
405
|
|
406
|
anonymousAction
|
407
|
returns [GuardedCommand result]
|
408
|
:
|
409
|
b=discreteActionBody {result = b;}
|
410
|
;
|
411
|
|
412
|
discreteActionBody
|
413
|
returns [GuardedCommand result]
|
414
|
@init{
|
415
|
result = null;
|
416
|
}
|
417
|
:
|
418
|
{result = createGuardedCommandStatement(); pushBlockToResolveStack(result);}
|
419
|
T_REQUIRES expr=expression T_COLON
|
420
|
bdy=actionBody[null]
|
421
|
T_END
|
422
|
{addExprAndBlockToGuardedCommand(result,expr,bdy);}
|
423
|
;
|
424
|
finally
|
425
|
{popBlockFromResolveStack(result);}
|
426
|
|
427
|
|
428
|
//
|
429
|
// ------------ do-od block ------------
|
430
|
//
|
431
|
|
432
|
actionBlock [Block top]
|
433
|
returns [Block prioList]
|
434
|
: {prioList = createPrioBlock(top); pushBlockToResolveStack(prioList);}
|
435
|
actionBlockParallel[prioList] (T_PRIO actionBlockParallel[prioList])*
|
436
|
;
|
437
|
finally
|
438
|
{popBlockFromResolveStack(prioList);}
|
439
|
|
440
|
actionBlockParallel [Block top]
|
441
|
@init { Block parList = createNondetBlock(top);
|
442
|
pushBlockToResolveStack(parList);
|
443
|
}
|
444
|
: actionBlockSequential[parList] (T_NONDET actionBlockSequential[parList])*
|
445
|
;
|
446
|
finally
|
447
|
{popBlockFromResolveStack(parList);}
|
448
|
// atomic sequential composition of actions
|
449
|
actionBlockSequential [Block top]
|
450
|
@init {
|
451
|
Block seqList = createSeqBlock(top);
|
452
|
pushBlockToResolveStack(seqList);
|
453
|
}
|
454
|
: (T_VAR syms=blockvarlist[seqList] ('&' sexpr=expression {addSeqBlockExpression(seqList,sexpr);} )? T_COLON )?
|
455
|
actionBlockParen[seqList] (T_SEMICOLON actionBlockParen[seqList])*
|
456
|
;
|
457
|
finally
|
458
|
{popBlockFromResolveStack(seqList);}
|
459
|
|
460
|
actionBlockParen [Block top]
|
461
|
: T_LPAREN actionBlock[top] T_RPAREN
|
462
|
| anonymousOrNamedAction[top]
|
463
|
;
|
464
|
|
465
|
anonymousOrNamedAction [Block top]
|
466
|
: gcmd=anonymousAction {addToBlockList(top,gcmd);}
|
467
|
| aname=T_IDENTIFIER
|
468
|
(T_LPAREN m_params=methodCallParams T_RPAREN)?
|
469
|
(amap=(T_FOLDLR|T_FOLDRL) '(' amapexpr=expression ')')?
|
470
|
{addNamedActionCallToBlockList(top,aname,m_params,amap,amapexpr);}
|
471
|
| T_SKIP {addSkipStatementToBlockList(top);}
|
472
|
;
|
473
|
|
474
|
|
475
|
blockvarlist [Block seqList]
|
476
|
: blockvar[seqList] (T_SEMICOLON blockvar[seqList] )*
|
477
|
;
|
478
|
|
479
|
blockvar [Block seqList]
|
480
|
: varname=T_IDENTIFIER T_COLON aType=complexType
|
481
|
{addBlockVariable(seqList,varname,aType);}
|
482
|
;
|
483
|
|
484
|
|
485
|
|
486
|
//
|
487
|
// ------------ action body of non-continuous actions ------------
|
488
|
//
|
489
|
|
490
|
actionBody[Block top]
|
491
|
returns [Block result]
|
492
|
: {result = createPrioBlock(top); pushBlockToResolveStack(result);}
|
493
|
actionBodyParallel[result] (T_PRIO actionBodyParallel[result])*
|
494
|
;
|
495
|
finally
|
496
|
{popBlockFromResolveStack(result);}
|
497
|
|
498
|
actionBodyParallel[Block top]
|
499
|
returns [Block result]
|
500
|
: {result = createNondetBlock(top); pushBlockToResolveStack(result);}
|
501
|
actionBodySequential[result]
|
502
|
(T_NONDET olst=actionBodySequential[result])*
|
503
|
;
|
504
|
finally
|
505
|
{popBlockFromResolveStack(result);}
|
506
|
|
507
|
|
508
|
// seq binds stronger than nondet, i.e. a;b;cd;e is read as (a;b;c)[](d;e)
|
509
|
actionBodySequential[Block top]
|
510
|
returns [SeqBlock result]
|
511
|
: {result = createSeqBlock(top); pushBlockToResolveStack(result);}
|
512
|
(T_VAR syms=blockvarlist[result] ('&' sexpr=expression {addSeqBlockExpression(result,sexpr);} )? T_COLON )?
|
513
|
actionBodyParen[result] (T_SEMICOLON actionBodyParen[result])*
|
514
|
;
|
515
|
finally
|
516
|
{popBlockFromResolveStack(result);}
|
517
|
|
518
|
|
519
|
actionBodyParen [SeqBlock top]
|
520
|
: T_LPAREN actionBody[top] T_RPAREN
|
521
|
| stmt=statement
|
522
|
{addToStatementList(top,stmt);}
|
523
|
;
|
524
|
|
525
|
|
526
|
statement
|
527
|
returns [Statement result]
|
528
|
@init {
|
529
|
boolean popFromResolveStack = false;
|
530
|
result = null;
|
531
|
}
|
532
|
: T_ABORT {result = createAbortStatement();}
|
533
|
| T_SKIP {result = createSkipStatement();}
|
534
|
| T_BREAK {result = createBreakStatement();}
|
535
|
| T_KILL T_LPAREN aname=(T_IDENTIFIER | T_SELF) T_RPAREN {result = createKillStatement(aname);}
|
536
|
| gc=discreteActionBody {result = gc;}
|
537
|
| aqname=reference
|
538
|
( // single assignment
|
539
|
T_ASSIGNMENT aexp=expression {result = createSingleAssignmentStatement(aqname,aexp);}
|
540
|
(T_WITH ndexp=expression {addConstraintToAssignment(result,ndexp);})? // nondet assignment
|
541
|
|
542
|
// multi assignment
|
543
|
| {result = createMultipleAssignmentStatementLHS(aqname);}
|
544
|
(T_COMMA malhs=reference {addMultipleAssignmentStatementLHS(result,malhs);})+
|
545
|
T_ASSIGNMENT
|
546
|
{pushAssignmentOnResolveStack(result); popFromResolveStack = true;}
|
547
|
mexp=expression
|
548
|
{addMutlipleAssignmentStatementRHS(result,mexp);}
|
549
|
(T_COMMA mexp2=expression {addMutlipleAssignmentStatementRHS(result,mexp2);})+
|
550
|
(T_WITH ndex2=expression {addConstraintToAssignment(result,ndex2);})? // nondet assignment
|
551
|
|
552
|
// just a call of a method.
|
553
|
| {result = createCallStatement(aqname);}
|
554
|
)
|
555
|
;
|
556
|
finally {
|
557
|
if (popFromResolveStack == true)
|
558
|
popAssignmentOffResolveStack(result);
|
559
|
}
|
560
|
|
561
|
//
|
562
|
// ------------ expression ------------
|
563
|
//
|
564
|
expression
|
565
|
returns [Expression expr]
|
566
|
@init{
|
567
|
ArrayList<BinaryOperator> operators = new ArrayList<BinaryOperator>();
|
568
|
ArrayList<Expression> expressions = new ArrayList<Expression>();
|
569
|
}
|
570
|
: left=atomExpression
|
571
|
{expressions.add(left);}
|
572
|
( op=binoperator
|
573
|
right=atomExpression
|
574
|
{
|
575
|
if (op != null) {
|
576
|
operators.add(op);
|
577
|
expressions.add(right);
|
578
|
}
|
579
|
}
|
580
|
)*
|
581
|
{expr = createPrecedenceTree(expressions,operators);}
|
582
|
;
|
583
|
|
584
|
|
585
|
binoperator
|
586
|
returns [BinaryOperator binop]
|
587
|
: T_BIIMPLIES
|
588
|
{binop = createBinaryOperator(ExpressionKind.biimplies);}
|
589
|
| T_GREATER
|
590
|
{binop = createBinaryOperator(ExpressionKind.greater);}
|
591
|
| T_GREATEREQUAL
|
592
|
{binop = createBinaryOperator(ExpressionKind.greaterequal);}
|
593
|
| T_LESS
|
594
|
{binop = createBinaryOperator(ExpressionKind.less);}
|
595
|
| T_LESSEQUAL
|
596
|
{binop = createBinaryOperator(ExpressionKind.lessequal);}
|
597
|
| T_EQUAL // bool, numeric, char, lists, maps
|
598
|
{binop = createBinaryOperator(ExpressionKind.equal);}
|
599
|
| T_NOTEQUAL // bool, numeric, char, lists, maps
|
600
|
{binop = createBinaryOperator(ExpressionKind.notequal);}
|
601
|
| T_IMPLIES
|
602
|
{binop = createBinaryOperator(ExpressionKind.implies);}
|
603
|
| T_MINUS
|
604
|
{binop = createBinaryOperator(ExpressionKind.minus);}
|
605
|
| T_SUM
|
606
|
{binop = createBinaryOperator(ExpressionKind.sum);}
|
607
|
| T_IN T_SET? // A * list of A -> bool
|
608
|
{binop = createBinaryOperator(ExpressionKind.elemin);}
|
609
|
| T_NOT T_IN T_SET? // A * list of A -> bool
|
610
|
{binop = createBinaryOperator(ExpressionKind.notelemin);}
|
611
|
| T_SUBSET // list of A * list of A -> bool (does not respect dupes)
|
612
|
{binop = createBinaryOperator(ExpressionKind.subset);}
|
613
|
| T_OR
|
614
|
{binop = createBinaryOperator(ExpressionKind.or);}
|
615
|
| T_DIV
|
616
|
{binop = createBinaryOperator(ExpressionKind.div);}
|
617
|
| T_PROD
|
618
|
{binop = createBinaryOperator(ExpressionKind.prod);}
|
619
|
| T_IDIV
|
620
|
{binop = createBinaryOperator(ExpressionKind.idiv);}
|
621
|
| T_MOD
|
622
|
{binop = createBinaryOperator(ExpressionKind.mod);}
|
623
|
| T_UNION // list of A * list of A -> list of A (does not respect dupes)
|
624
|
{binop = createBinaryOperator(ExpressionKind.union);}
|
625
|
| T_DIFF // list of A * list of A -> list of A (does not respect dupes)
|
626
|
{binop = createBinaryOperator(ExpressionKind.diff);}
|
627
|
| T_INTER // list of A * list of A -> list of A (does not respect dupes)
|
628
|
{binop = createBinaryOperator(ExpressionKind.inter);}
|
629
|
| T_AND
|
630
|
{binop = createBinaryOperator(ExpressionKind.and);}
|
631
|
| T_POW
|
632
|
{binop = createBinaryOperator(ExpressionKind.pow);}
|
633
|
| T_CONC // list of A * list of A -> list of A
|
634
|
{binop = createBinaryOperator(ExpressionKind.conc);}
|
635
|
| T_DOMRESBY // list of A * map A to B -> map A to B
|
636
|
{binop = createBinaryOperator(ExpressionKind.domresby);}
|
637
|
| T_DOMRESTO // list of A * map A to B -> map A to B
|
638
|
{binop = createBinaryOperator(ExpressionKind.domresto);}
|
639
|
| T_RNGRESBY // map A to B * list of B -> map A to B
|
640
|
{binop = createBinaryOperator(ExpressionKind.rngresby);}
|
641
|
| T_RNGRESTO // map A to B * list of B -> map A to B
|
642
|
{binop = createBinaryOperator(ExpressionKind.rngresto);}
|
643
|
| T_MUNION // map A to B * map A to B -> map A to B
|
644
|
{binop = createBinaryOperator(ExpressionKind.munion);}
|
645
|
| T_SEQMOD_MAPOVERRIDE // list of A * map int to A -> list of A or
|
646
|
// map A to B * map A to B -> map A to B
|
647
|
{binop = createBinaryOperator(ExpressionKind.seqmod_mapoverride);}
|
648
|
;
|
649
|
|
650
|
|
651
|
atomExpression
|
652
|
returns [Expression expr]
|
653
|
@init {
|
654
|
expr = null;
|
655
|
}
|
656
|
: (unexpr=op_un? (
|
657
|
e=identifierExpression
|
658
|
| e=constant
|
659
|
| e=initializedComplexType
|
660
|
| e=quantifierExpression
|
661
|
| T_LPAREN e=expression T_RPAREN
|
662
|
(
|
663
|
(T_POINT
|
664
|
idn=T_IDENTIFIER
|
665
|
{e = addIdentifierAccessExpression(e,idn);})+
|
666
|
(res=accessExpression[e] {e=res;})?
|
667
|
|
|
668
|
e=accessExpression[e]
|
669
|
)?
|
670
|
) ('as' cid=T_IDENTIFIER {e=addCastExpression(e,cid);})?
|
671
|
{expr = addUnaryExpression(unexpr,e);}
|
672
|
)
|
673
|
| ie=T_IF ce=expression T_THEN te=expression T_ELSE ee=expression T_END
|
674
|
{expr = createConditionalExpression(ce,te,ee,ie);}
|
675
|
;
|
676
|
|
677
|
|
678
|
quantifierExpression
|
679
|
returns [Quantifier result]
|
680
|
@init {
|
681
|
result = null;
|
682
|
}
|
683
|
: t=(T_FORALL | T_EXISTS)
|
684
|
{result = createQuantifierExpression(t);}
|
685
|
(id=T_IDENTIFIER (T_COLON id_type=simpleType {addBoundVarToQuantifierExpression(result,id,id_type);})
|
686
|
(T_COMMA id2=T_IDENTIFIER (T_COLON id_type2=simpleType){addBoundVarToQuantifierExpression(result,id2,id_type2);})*)
|
687
|
T_COLON T_LPAREN e=expression T_RPAREN
|
688
|
{addExpressionToQuantifier(result,e);}
|
689
|
;
|
690
|
finally
|
691
|
{removeBoundVarsFromResolveStack(result);}
|
692
|
|
693
|
constant
|
694
|
returns [LeafExpression result]
|
695
|
@init {
|
696
|
result = null;
|
697
|
}
|
698
|
: T_TRUE {result = createBoolConstant(true);}
|
699
|
| T_FALSE {result = createBoolConstant(false);}
|
700
|
| T_NIL {result = createNullPointerConstant();}
|
701
|
| T_SELF {result = createSelfPointer();}
|
702
|
| t_fl=T_FLOATNUMBER {result = createFloatConstant(t_fl);}
|
703
|
| t_in=T_INTNUMBER {result = createIntConstant(t_in);}
|
704
|
| t_l=T_STRINGLITERAL {result = createStringConstant(t_l);}
|
705
|
;
|
706
|
|
707
|
initializedComplexType
|
708
|
returns [Expression result]
|
709
|
@init {
|
710
|
result = null;
|
711
|
}
|
712
|
: res=initializedListType {result = res;}
|
713
|
| res=initializedSetType {result = res;}
|
714
|
| T_NEW T_LPAREN anid=T_IDENTIFIER
|
715
|
(
|
716
|
T_COMMA aname=T_STRINGLITERAL T_RPAREN {result = createNamedObject(anid, aname);}
|
717
|
| T_RPAREN {result = createObject(anid);} // constructor call..
|
718
|
)
|
719
|
;
|
720
|
|
721
|
initializedListType
|
722
|
returns [ListConstructor result]
|
723
|
@init {
|
724
|
result = createInitializedList();
|
725
|
pushListVarsOnResolveStack(result); // need this here for list comprehension
|
726
|
}
|
727
|
: T_LSQPAREN e=expression {addListElement(result,e);} (
|
728
|
(T_COMMA e2=expression {addListElement(result,e2);})+
|
729
|
| listComprehension[result]
|
730
|
)? T_RSQPAREN
|
731
|
;
|
732
|
finally
|
733
|
{popListVarsFromResolveStack(result);}
|
734
|
|
735
|
listComprehension [ListConstructor result]
|
736
|
@init{
|
737
|
result.SetHasComprehension(true);
|
738
|
}
|
739
|
:
|
740
|
T_BAR T_VAR
|
741
|
id=T_IDENTIFIER T_COLON t1=complexType {addListComprVar(result,id,t1);}
|
742
|
(T_SEMICOLON id2=T_IDENTIFIER t2=complexType {addListComprVar(result,id2,t2);})*
|
743
|
('&'
|
744
|
e=expression {addListComprExpr(result,e);})?
|
745
|
;
|
746
|
|
747
|
initializedSetType
|
748
|
returns[Expression result]
|
749
|
@init {
|
750
|
result = null;
|
751
|
}
|
752
|
: T_CBRL T_MAPS T_CBRR {result = createEmptyMap();} // empty map
|
753
|
| res=initializedSet {result = res;}
|
754
|
;
|
755
|
|
756
|
initializedSet
|
757
|
returns [Expression result]
|
758
|
@init {
|
759
|
SetConstructor theset = createSet();
|
760
|
pushSetVarsOnResolveStack(theset); // need this here for set comprehension
|
761
|
result = theset;
|
762
|
}
|
763
|
: T_CBRL e1=expression
|
764
|
( // set constructor; empty set: {nil}
|
765
|
{addToSet(result,e1);}
|
766
|
(T_COMMA e2=expression {addToSet(result,e2);})* // set constructor for sets > 1 elem
|
767
|
| m=map[result, e1] {result = m;} // we have a set in the resolution stack, but this should be fine (no syms)
|
768
|
| {addToSet(result,e1);} setComprehension[(SetConstructor)result] // set comprehension
|
769
|
) T_CBRR
|
770
|
;
|
771
|
finally
|
772
|
{popSetVarsFromResolveStack(theset);}
|
773
|
|
774
|
map[Expression _map, Expression e1]
|
775
|
returns [Expression result]
|
776
|
@init {
|
777
|
result = null;
|
778
|
}
|
779
|
: am=T_MAPS e2=expression {result = createMap(e1,e2,am);} (T_COMMA e3=expression T_MAPS e4=expression {addToMap(result,e3,e4);})*
|
780
|
;
|
781
|
|
782
|
setComprehension[SetConstructor _set]
|
783
|
@init {
|
784
|
_set.SetHasComprehension(true);
|
785
|
}
|
786
|
: T_BAR T_VAR id1=T_IDENTIFIER T_COLON t1=complexType
|
787
|
{ addSetComprVar(_set, id1, t1); }
|
788
|
(T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType
|
789
|
{ addSetComprVar(_set, id2, t2); })*
|
790
|
('&'
|
791
|
epx=expression
|
792
|
{ addSetComprExpr(_set,epx); })?
|
793
|
;
|
794
|
|
795
|
identifierExpression
|
796
|
returns [Expression result]
|
797
|
: // if next token is a tuple-type then create an initialized tuple!
|
798
|
{isTuple(input.LT(1).getText())}?
|
799
|
aName=T_IDENTIFIER T_LPAREN m_params=methodCallParams T_RPAREN
|
800
|
{result = createInitializedTuple(aName,m_params);}
|
801
|
| // is some sort of reference
|
802
|
res=reference
|
803
|
{result = res;}
|
804
|
;
|
805
|
|
806
|
|
807
|
reference
|
808
|
returns [Expression result]
|
809
|
@init {
|
810
|
result = null;
|
811
|
init = null;
|
812
|
}
|
813
|
: {!isTuple(input.LT(1).getText())}? // check that the next token is not a reference to a tuple-type
|
814
|
aName=qualifiedIdentifier {result = aName;}
|
815
|
( output=accessExpression[result] {result = output;}
|
816
|
// call expression
|
817
|
| // variable access or method call that takes no params? (do we allow for that? - answer: no!)
|
818
|
)
|
819
|
( pr=T_PRIMED {result = setIdentifierExpressionPrimed(result,pr);}
|
820
|
|
|
821
|
('::' T_LPAREN init=expression T_RPAREN)? afold=(T_FOLDLR|T_FOLDRL) T_LPAREN anexpr=expression T_RPAREN
|
822
|
{result = createFoldExpression(result,afold,init,anexpr);}
|
823
|
)?
|
824
|
;
|
825
|
|
826
|
accessExpression[Expression subexpr]
|
827
|
returns [Expression result]
|
828
|
@init{
|
829
|
UnaryOperator newExpr = null;
|
830
|
result = subexpr;
|
831
|
}
|
832
|
:
|
833
|
( tcall=T_LSQPAREN ac=expression T_RSQPAREN // access tuples, maps
|
834
|
{ result = createTupleMapAccessExpression(result,ac,tcall); }
|
835
|
| bcall=T_LPAREN m_params=methodCallParams T_RPAREN // access method
|
836
|
{ result = createMethodAccessExpression(result,m_params,bcall); }
|
837
|
)+
|
838
|
( // a[1].c.e()...
|
839
|
(T_POINT
|
840
|
idn=T_IDENTIFIER
|
841
|
{result = addIdentifierAccessExpression(result,idn);})+
|
842
|
(res=accessExpression[result] {result=res;})?
|
843
|
)?
|
844
|
;
|
845
|
|
846
|
qualifiedIdentifier
|
847
|
returns [Expression top]
|
848
|
@init {
|
849
|
IdentifierExpression selfexpr = null;
|
850
|
top = null;
|
851
|
}
|
852
|
:
|
853
|
(self=T_SELF T_POINT {selfexpr = createSelfIdentifierExpression(self);})?
|
854
|
idb=T_IDENTIFIER {top = createIdentifierAccessExpression(selfexpr,idb);}
|
855
|
(T_POINT idd=T_IDENTIFIER {top = addIdentifierAccessExpression(top,idd);})*
|
856
|
;
|
857
|
|
858
|
|
859
|
methodCallParams
|
860
|
returns [ArrayList<Expression> result]
|
861
|
@init {
|
862
|
result = new ArrayList<Expression>();
|
863
|
}
|
864
|
: (expa=expression {result.add(expa);} (T_COMMA expb=expression {result.add(expb);})*)?
|
865
|
;
|
866
|
|
867
|
|
868
|
|
869
|
//
|
870
|
// ------------ unary Operators ------------
|
871
|
//
|
872
|
|
873
|
|
874
|
op_un
|
875
|
returns [UnaryOperator expr]
|
876
|
@init {
|
877
|
expr = null;
|
878
|
}
|
879
|
: r=op_un_set_list {expr = r;}
|
880
|
| r2=op_un_map {expr = r2;}
|
881
|
| T_MINUS {expr = createUnaryOperator(ExpressionKind.unminus);}
|
882
|
| T_NOT {expr = createUnaryOperator(ExpressionKind.not);}
|
883
|
| T_ABS {expr = createUnaryOperator(ExpressionKind.abs);}
|
884
|
;
|
885
|
|
886
|
|
887
|
op_un_set_list
|
888
|
returns [UnaryOperator expr]
|
889
|
@init {
|
890
|
expr = null;
|
891
|
}
|
892
|
: T_CARD // list of A -> int (does not respect dupes, i.e. dupes do not count)
|
893
|
{expr = createUnaryOperator(ExpressionKind.card);}
|
894
|
| T_DCONC // list of list of A -> list of A
|
895
|
{expr = createUnaryOperator(ExpressionKind.dconc);}
|
896
|
| T_DINTER // list of list of A -> list of A (intersection, does not respect dupes)
|
897
|
{expr = createUnaryOperator(ExpressionKind.dinter);}
|
898
|
| T_DUNION // list of list of A -> list of A (union, does not respect dupes)
|
899
|
{expr = createUnaryOperator(ExpressionKind.dunion);}
|
900
|
| T_ELEMS // list of A -> list of A (does not respect dupes)
|
901
|
{expr = createUnaryOperator(ExpressionKind.elems);}
|
902
|
| T_HEAD // list of A -> A
|
903
|
{expr = createUnaryOperator(ExpressionKind.head);}
|
904
|
| T_INDS // list of A -> list of int
|
905
|
{expr = createUnaryOperator(ExpressionKind.inds);}
|
906
|
| T_LEN // list of A -> int (dupes count)
|
907
|
{expr = createUnaryOperator(ExpressionKind.len);}
|
908
|
| T_TAIL // list of A -> list of A
|
909
|
{expr = createUnaryOperator(ExpressionKind.tail);}
|
910
|
;
|
911
|
|
912
|
|
913
|
op_un_map
|
914
|
returns [UnaryOperator expr]
|
915
|
@init {
|
916
|
expr = null;
|
917
|
}
|
918
|
: T_DOM // map A to B -> list of A
|
919
|
{expr = createUnaryOperator(ExpressionKind.dom);}
|
920
|
| T_RNG // map A to B -> list of B
|
921
|
{expr = createUnaryOperator(ExpressionKind.range);}
|
922
|
| T_MERGE // list of map A to B -> map A to B
|
923
|
{expr = createUnaryOperator(ExpressionKind.merge);}
|
924
|
;
|
925
|
|
926
|
|
927
|
|
928
|
|
929
|
|
930
|
|
931
|
//
|
932
|
// ============== LEXER =================
|
933
|
//
|
934
|
T_WS : (' '|'\r'|'\t'|'\u000C'|'\n') {$channel=HIDDEN;}
|
935
|
;
|
936
|
|
937
|
T_COMMENT
|
938
|
: '/*' .* '*/' {$channel=HIDDEN;}
|
939
|
;
|
940
|
|
941
|
LINE_COMMENT
|
942
|
: '#' ~('\n'|'\r')* '\r'? '\n' {$channel=HIDDEN;}
|
943
|
;
|
944
|
|
945
|
T_PRIMED
|
946
|
: '\'';
|
947
|
|
948
|
T_STRINGLITERAL
|
949
|
: '"'
|
950
|
(
|
951
|
( '"' '"' )=> '"'
|
952
|
| ~'"'
|
953
|
)*
|
954
|
'"'
|
955
|
;
|
956
|
|
957
|
|
958
|
T_ABORT : 'abort';
|
959
|
T_ACTIONS
|
960
|
: 'actions';
|
961
|
T_ASSIGNMENT
|
962
|
: ':=';
|
963
|
T_AUTOCONS: 'autocons';
|
964
|
T_BAR : '|';
|
965
|
T_BOOL : 'bool';
|
966
|
T_CBRL : '{';
|
967
|
T_CBRR : '}';
|
968
|
T_COLON : ':';
|
969
|
T_COMMA : ',';
|
970
|
//T_CONT : 'qual';
|
971
|
T_CHAR : 'char';
|
972
|
T_CTRL : 'ctr';
|
973
|
T_SYSTEM
|
974
|
: 'system';
|
975
|
T_DO : 'do';
|
976
|
T_ELSE : 'else';
|
977
|
T_END : 'end';
|
978
|
T_EQUAL : '=';
|
979
|
T_EXISTS : 'exists';
|
980
|
T_FLOAT : 'float';
|
981
|
T_FORALL : 'forall';
|
982
|
T_FALSE : 'false';
|
983
|
T_IF : 'if';
|
984
|
T_IN : 'in';
|
985
|
T_INT : 'int';
|
986
|
T_KILL : 'kill';
|
987
|
T_LIST : 'list';
|
988
|
T_LPAREN : '(';
|
989
|
T_LSQPAREN: '[';
|
990
|
T_MAP : 'map';
|
991
|
T_MAPS : '->';
|
992
|
T_METHODS
|
993
|
: 'methods';
|
994
|
T_NEW : 'new';
|
995
|
T_NIL : 'nil';
|
996
|
T_NONDET : '[]';
|
997
|
T_OBS : 'obs';
|
998
|
T_OD : 'od';
|
999
|
T_OF : 'of';
|
1000
|
T_PRIO : '//';
|
1001
|
T_REQUIRES
|
1002
|
: 'requires';
|
1003
|
T_RPAREN : ')';
|
1004
|
T_RSQPAREN: ']';
|
1005
|
T_SELF : 'self';
|
1006
|
T_SET : 'set';
|
1007
|
T_SEMICOLON
|
1008
|
: ';';
|
1009
|
T_STATIC : 'static';
|
1010
|
T_SKIP : 'skip';
|
1011
|
T_BREAK : 'break';
|
1012
|
T_THEN : 'then';
|
1013
|
T_TRUE : 'true';
|
1014
|
T_TO : 'to';
|
1015
|
T_TYPES : 'types';
|
1016
|
T_VAR : 'var';
|
1017
|
T_WITH : 'with'; // for nondet assignment
|
1018
|
|
1019
|
|
1020
|
//T_ACTION: 'action';
|
1021
|
|
1022
|
//BOOL
|
1023
|
T_AND : 'and';
|
1024
|
T_BIIMPLIES
|
1025
|
: '<=>';
|
1026
|
T_IMPLIES
|
1027
|
: '=>'; //VDM-Style
|
1028
|
T_NOT : 'not'; //VDM-Style
|
1029
|
T_NOTEQUAL: '<>'; //VDM-Style
|
1030
|
T_OR : 'or';
|
1031
|
|
1032
|
//Numeric (equal, not equal same as in BOOL)
|
1033
|
T_ABS : 'abs';
|
1034
|
T_DIV : '/';
|
1035
|
T_GREATER
|
1036
|
: '>';
|
1037
|
T_GREATEREQUAL
|
1038
|
: '>=';
|
1039
|
T_IDIV : 'div';
|
1040
|
T_LESS : '<';
|
1041
|
T_LESSEQUAL
|
1042
|
: '<='; //VDM-Style
|
1043
|
T_MOD : 'mod'; //VDM-Style
|
1044
|
T_POW : '**';
|
1045
|
T_PROD : '*';
|
1046
|
T_DERIV : 'dt';
|
1047
|
|
1048
|
// set/list
|
1049
|
T_CARD : 'card';
|
1050
|
T_CONC : '^';
|
1051
|
T_DCONC : 'conc';
|
1052
|
T_DIFF : '\\';
|
1053
|
T_DINTER : 'dinter';
|
1054
|
T_DUNION : 'dunion';
|
1055
|
T_ELEMS : 'elems';
|
1056
|
T_HEAD : 'hd';
|
1057
|
T_INDS : 'inds';
|
1058
|
T_INTER : 'inter';
|
1059
|
T_LEN : 'len'; // differs from T_CARD, as card does not count dupes..
|
1060
|
T_SEQMOD_MAPOVERRIDE
|
1061
|
: '++';
|
1062
|
T_SUBSET : 'subset';
|
1063
|
T_TAIL : 'tl';
|
1064
|
T_UNION : 'union';
|
1065
|
T_FOLDLR
|
1066
|
: ':>:';
|
1067
|
T_FOLDRL
|
1068
|
: ':<:';
|
1069
|
|
1070
|
|
1071
|
// maps
|
1072
|
T_DOM : 'dom';
|
1073
|
T_DOMRESBY
|
1074
|
: '<-:';
|
1075
|
T_DOMRESTO
|
1076
|
: '<:';
|
1077
|
T_RNG : 'rng';
|
1078
|
T_RNGRESBY
|
1079
|
: ':->';
|
1080
|
T_RNGRESTO
|
1081
|
: ':>';
|
1082
|
T_MERGE : 'merge';
|
1083
|
T_MUNION : 'munion';
|
1084
|
|
1085
|
T_CONSTS : 'consts';
|
1086
|
|
1087
|
// numbers
|
1088
|
|
1089
|
T_INFTY : (T_MINUS|T_SUM)? 'inf'
|
1090
|
;
|
1091
|
|
1092
|
|
1093
|
// INTNUMBER, FLOATNUMBER, RANGETO, T_MINUS, T_PLUS are set within
|
1094
|
// FLOAT_OR_INT_OR_RANGE
|
1095
|
fragment T_INTNUMBER
|
1096
|
: ;
|
1097
|
fragment T_FLOATNUMBER
|
1098
|
: ;
|
1099
|
fragment T_RANGETO
|
1100
|
: ;
|
1101
|
|
1102
|
FLOAT_OR_INT_OR_RANGE
|
1103
|
: (T_MINUS|T_SUM)? T_DIGIT+
|
1104
|
( // at this stage, we could face an int, int..int (=range), int.exp (=float), int.exp..int.exp (=float range) etc..
|
1105
|
(T_POINT T_POINT) => {$type=T_INTNUMBER;}
|
1106
|
| (T_POINT T_DIGIT) => T_POINT T_DIGIT+ (('e'|'E') (T_MINUS|T_SUM)? T_DIGIT+)? {$type=T_FLOATNUMBER;}
|
1107
|
| {$type=T_INTNUMBER;}
|
1108
|
)
|
1109
|
| T_POINT
|
1110
|
( // could be point or range..
|
1111
|
T_POINT {$type=T_RANGETO;}
|
1112
|
| {$type=T_POINT;}
|
1113
|
)
|
1114
|
| T_MINUS {$type=T_MINUS;}
|
1115
|
| T_SUM {$type=T_SUM;}
|
1116
|
;
|
1117
|
|
1118
|
|
1119
|
|
1120
|
fragment T_MINUS: '-';
|
1121
|
fragment T_SUM : '+';
|
1122
|
fragment T_POINT: '.';
|
1123
|
|
1124
|
|
1125
|
|
1126
|
// identifiers
|
1127
|
T_IDENTIFIER
|
1128
|
: T_LETTER (T_LETTER|T_DIGIT)*
|
1129
|
;
|
1130
|
|
1131
|
//T_PRIMEDIDENTIFIER
|
1132
|
// : T_IDENTIFIER '\'';
|
1133
|
|
1134
|
fragment
|
1135
|
T_LETTER
|
1136
|
: '$'
|
1137
|
| 'A'..'Z'
|
1138
|
| 'a'..'z'
|
1139
|
| '_'
|
1140
|
;
|
1141
|
|
1142
|
fragment
|
1143
|
T_DIGIT: '0'..'9';
|
1144
|
|