This repository has been archived by the owner. It is now read-only.
Permalink
Switch branches/tags
stable-20161113-115302 stable-20151214-102407 stable-20150506-095613 stable-20150401-084749 stable-20150126-161805 stable-20150120-095010 stable-20150120-091856 stable-20141219-150702 stable-20141029-170046 stable-20140715-165046 stable-20140530-090013 stable-20140521-143929 stable-20140509-113028 stable-20140509-110423 stable-20140415-165131 stable-20140414-164252 stable-20140414-144950 stable-20140414-131645 stable-20140408-135559 stable-20140408-132007 stable-20140408-115925 stable-20140408-093224 stable-20140401-201237 stable-20140121-151530 stable-20131109-100904 stable-20131029-195331 stable-20131029-122855 stable-20131029-112113 jenkins-Sireum-Update-Site-Stable-8 jenkins-Sireum-Update-Site-Stable-4 jenkins-Sireum-Update-Site-Stable-3 jenkins-Sireum-Update-Site-Dev-28 jenkins-Sireum-Update-Site-Dev-27 jenkins-Sireum-Update-Site-Dev-26 jenkins-Sireum-Update-Site-Dev-25 jenkins-Sireum-Update-Site-Dev-22 jenkins-Sireum-Update-Site-Dev-21 jenkins-Sireum-Update-Site-Dev-20 jenkins-Sireum-Update-Site-Dev-19 dev-20170105-002220 dev-20170104-002209 dev-20170103-002224 dev-20170102-002232 dev-20170101-002323 dev-20161231-002215 dev-20161230-002128 dev-20161229-002120 dev-20161228-002120 dev-20161227-002152 dev-20161226-002112 dev-20161225-002134 dev-20161224-002237 dev-20161223-002038 dev-20161222-002119 dev-20161221-002125 dev-20161220-002005 dev-20161219-002121 dev-20161218-002028 dev-20161217-002158 dev-20161216-002152 dev-20161215-002033 dev-20161214-002031 dev-20161213-002114 dev-20161212-002124 dev-20161211-002116 dev-20161210-002135 dev-20161209-002127 dev-20161208-002025 dev-20161207-002125 dev-20161206-002121 dev-20161205-002034 dev-20161204-002129 dev-20161203-002133 dev-20161202-002125 dev-20161201-002130 dev-20161130-002025 dev-20161129-002146 dev-20161128-002131 dev-20161127-002125 dev-20161126-002138 dev-20161125-002131 dev-20161124-002132 dev-20161123-002124 dev-20161122-002137 dev-20161121-002131 dev-20161120-002142 dev-20161119-002133 dev-20161118-002130 dev-20161117-002106 dev-20161116-002145 dev-20161115-002144 dev-20161114-002135 dev-20161113-110002 dev-20161113-002022 dev-20161112-002021 dev-20161111-002022 dev-20161110-002011 dev-20161109-130334 dev-20161108-002018 dev-20161107-002021
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
641 lines (514 sloc) 13.5 KB
grammar Antlr4Pilar;
modelFile : model EOF;
annotationFile : annotation EOF;
bodyFile : implementedBody EOF;
locationFile : location EOF;
transformationFile : transformation EOF;
actionFile : action EOF;
jumpFile : jump EOF;
expFile : exp EOF;
typeFile : type EOF;
model
: annotation* modelElement*
;
annotation
: '@' ID annotationParams?
;
annotationParams
: '(' annotationParam ( ',' annotationParam )* ')' #AnnotationParamsA
| exp+ #AnnotationParamsE
;
annotationParam
: ID '=' annotation #AnnotationParamIA
| ID '=' exp #AnnotationParamIE
| annotation #AnnotationParamA
| exp #AnnotationParamE
;
modelElement
: constDeclaration
| enumDeclaration
| recordDeclaration
| globalVarsDeclaration
| procedureDeclaration
| funDeclaration
| extDeclaration
| typealiasDeclaration
;
constDeclaration
: 'const' ID annotation* '{' constElement* '}'
;
constElement
: ID '=' constant annotation* ';'
;
enumDeclaration
: 'enum' ID annotation* '{' ( enumElement ( ',' enumElement )* )? '}'
;
enumElement
: ID annotation*
;
typealiasDeclaration
: 'typealias' ID typeVarTuple? annotation* '=' type ';'
;
typeVarTuple
: '<' typeVar ( ',' typeVar )* '>'
;
typeVar
: ID annotation*
;
recordDeclaration
: 'record' ID typeVarTuple? annotation* extendClauses? '{' field* '}'
;
extendClauses
: 'extends' extendClause ( ',' extendClause )*
;
extendClause
: ID typeTuple? annotation*
;
typeTuple
: '<' type ( ',' type )* '>'
;
field
: fieldFragment ( ',' fieldFragment )* ':' type ';'
| type? fieldFragment ( ',' fieldFragment )* ';'
;
fieldFragment
: ID annotation*
;
globalVarsDeclaration
: 'global' globalVarDeclaration+
;
globalVarDeclaration
: globalVarFragment ( ',' globalVarFragment )* ':' type ';'
| type? globalVarFragment ( ',' globalVarFragment )* ';'
;
globalVarFragment
: GID annotation*
;
procedureDeclaration
: 'procedure' typeVarTuple?
( ID ( '(' ( paramVar ( ',' paramVar )* )? ')' )? ':' type
annotation* body
| type? ID ( '(' ( paramVar ( ',' paramVar )* )? ')' )?
annotation* body
)
;
paramVar
: ID annotation* ':' type
| type? ID annotation*
;
funDeclaration
: 'fun' typeVarTuple?
( ID ( '(' ( paramVar ( ',' paramVar )* )? ')' )?
annotation* ':' type '=' exp ';'
| type? ID ( '(' ( paramVar ( ',' paramVar )* )? ')' )?
annotation* '=' exp ';'
)
;
extDeclaration
: 'extension' typeVarTuple? ID annotation* '{' extElement* '}'
;
extElement
: 'typedef' typeVarTuple? ID annotation* extendClauses? ';' #TypeExtension
| 'actiondef' typeVarTuple? ID ( '(' extParams? ')' )? annotation* ';' #ActionExtension
| 'expdef' typeVarTuple? ID ( '(' extParams? ')' )? annotation* ':' type ';' #ExpExtension
| 'expdef' typeVarTuple? type? ID ( '(' extParams? ')' )? annotation* ';' #ExpExtension
| 'procdef' typeVarTuple? ID ( '(' extParams? ')' )? annotation* ':' type ';' #ProcedureExtension
| 'procdef' typeVarTuple? type? ID ( '(' extParams? ')' )? annotation* ';' #ProcedureExtension
;
extParams
: extParam ( ',' extParam )* ( ',' extParamVariable )?
| extParamVariable
;
extParam
: ID annotation* ':' type
| type ID? annotation*
;
extParamVariable
: ID '...' annotation* ':' type
| type '...' ID? annotation*
;
body
: implementedBody
| emptyBody
;
implementedBody
: '{'
localVarsDeclaration?
location*
catchClause*
'}'
;
emptyBody
: ';'
;
localVarsDeclaration
: localVarDeclaration+
;
localVarDeclaration
: localVarFragment ( ',' localVarFragment )* ':' type ';'
| type? localVarFragment ( ',' localVarFragment )* ';'
;
localVarFragment
: ID annotation*
;
location
: LID annotation*
( transformation ( '|' transformation )* )?
;
transformation
: guard? 'call'
( clhs+=ID ( ',' clhs+=ID )* AssignOP )? p=ID
tupleExp
( cans+=annotation )*
( gotoj | ';' ) ( tanns+=annotation )* #CallTransformation
| guard? action* jump?
( tanns+=annotation )* #BlockTransformation
;
guard
: exp annotation* '+>' # ExpGuard
| 'else' annotation* # ElseGuard
;
action
: 'assert' exp ( ',' exp )? annotation* ';' #Assert
| 'assume' exp ( ',' exp )? annotation* ';' #Assume
| 'throw' exp annotation* ';' #Throw
| 'start' typeTuple? ID ( '[' n=exp ']' )?
tupleExp annotation* ';' #Start
| ID typeTuple? tupleExp
annotation* ';' #ActionExtCall
| lhss AssignOP rhs ( ',' rhs )* annotation* ';' #Assign
;
lhss
: lhs ( ',' lhs )*
;
lhs
: exp annotation*
;
rhs
: annotation* exp
;
jump
: gotoj #GotoJump
| 'return' ( exp ( ',' exp )* )? annotation* ';' #ReturnJump
| ifThenJump ( 'else' ifThenJump )* ifElseJump? annotation* ';' #IfJump
| 'switch' exp switchCaseJump* switchDefaultJump? annotation* ';' #SwitchJump
;
gotoj
: 'goto' ID annotation* ';'
;
ifThenJump
: 'if' exp 'then' annotation* 'goto' ID
;
ifElseJump
: 'else' annotation* 'goto' ID
;
switchCaseJump
: '|' constant '=>' annotation* 'goto' ID
;
switchDefaultJump
: '|' 'else' '=>' annotation* 'goto' ID
;
catchClause
: 'catch' annotation*
( var=ID? ':' type | type? var=ID? )
'@' '[' from=ID '..' to=ID ']' gotoj
;
exp
: primary primarySuffix* #PrimaryExp
| '(' type ')' exp #CastExp
| op=( UnaryOP | AddOP | MulOP ) exp #UnaryExp
| exp op=ID exp #BinaryExp
| exp op=MulOP exp #BinaryExp
| exp op=AddOP exp #BinaryExp
| exp op=ShiftOP exp #BinaryExp
| exp op=( RelOP | '<' | '>' ) exp #BinaryExp
| exp op=EqOP exp #BinaryExp
| exp op=AndOP exp #BinaryExp
| exp op=XorOP exp #BinaryExp
| exp op=OrOP exp #BinaryExp
| exp op=CondAndOP exp #BinaryExp
| exp op=CondOrOP exp #BinaryExp
| exp op=( '==>' | '<==' ) exp #BinaryExp
| ifThenExp ( 'else' ifThenExp )* ifElseExp #IfExp
;
ifThenExp
: 'if' exp 'then' annotation* exp
;
ifElseExp
: 'else' annotation* exp
;
primarySuffix
: '[' exp ( ',' exp )* ']' #IndexingSuffix
| '.' ID #AccessSuffix
| typeTuple? tupleExp #CallSuffix
;
primary
: ID #NameExp
| GID #GlobalNameExp
| constant #ConstantLit
| tupleExp #PTupleExp
| 'let' binding ( ',' binding )* 'in' exp #LetExp
| newK '[' exp '..' exp ']' #RangedListExp
| newK '[' ( exp ( ',' exp )* )? ']' #ListExp
| newK '{' ( exp ( ',' exp )* )? '}' #SetExp
| newK '{' ( '->' | mapping ( ',' mapping )* ) '}' #MapExp
| newK '['
( newMultiSeqFragment
( ',' newMultiSeqFragment )* )? ']' #MultiSeqExp
| newK ID typeTuple?
'{' ( fieldInit ( ',' fieldInit )* )? '}' #RecordExp
| newK baseType newMultiSeqTypeFragment* typeFragment* #ArrayExp
| '^' type #TypeExp
| '{' matching ( '|' matching )* '}' #ClosureExp
;
tupleExp
: '(' ( annExp ( ',' annExp )* )? ')'
;
annExp
: exp annotation*
;
newK
: '^' | 'new'
;
binding
: ID ( ',' ID )? '=' exp
;
mapping
: exp '->' exp
;
newMultiSeqFragment
: '[' ( newMultiSeqFragmentE
( ',' newMultiSeqFragmentE )* )? ']'
;
newMultiSeqFragmentE
: newMultiSeqFragment #NewMultiSeqFragmentENew
| exp #NewMultiSeqFragmentEExp
;
matching
: ( paramVar ( ',' paramVar )* )? '=>' exp
;
fieldInit
: ID '=' exp
;
newMultiSeqTypeFragment
: '[' exp ( ',' exp )* ']'
;
type
: baseType typeFragment*
;
typeFragment
: '[' ']' #SeqFragment
| '[' constant ']' #StaticSeqFragment
| '[' ( rank+=',' )+ ']' #MultiSeqFragment
| '[' constant ( ',' constant )+ ']' #StaticMultiSeqFragment
| '{' '}' #SetFragment
;
constant
: 'true' #TrueConstant
| 'false' #FalseConstant
| 'null' #NullConstant
| ID #IdConstant
| CHAR #CharConstant
| HEX #HexConstant
| OCT #OctConstant
| DEC #DecConstant
| BIN #BinConstant
| FLOAT #FloatConstant
| STRING #StringConstant
| MSTRING #MultilineStringConstant
;
baseType
: ID typeTuple? #NamedType
| '(' ( typeParam ( ',' typeParam )* )? '->' annotatedType? ')' #ClosureType
| '(' ( typeParam ( ',' typeParam )* )? '-!>' annotatedType? ')' #ProcedureType
| '(' typeParam ( ',' typeParam)* ')' #TupleType
| '{' typeParam ( ',' typeParam )* '->' annotatedType '}' #MapType
| '{' typeParam ( ',' typeParam )+ '}' #RelationType
;
typeParam
: ID annotation* ':' type
| type ID? annotation*
;
annotatedType
: type annotation*
;
GID
: '@@' IDFragment
| '`@@' ( ~( '\n' | '\r' | '\t' | '\u000C' | '`' ) )* '`'
;
ID
: IDFragment '\''*
| '`' ( ~( '\n' | '\r' | '\t' | '\u000C' | '`' ) )* '`'
;
LID
: '#' ( ID '.'? )?
;
MSTRING
: '"""' .*? '"""'
;
WS
: [ \r\t\u000C\n]+ -> channel(HIDDEN)
;
COMMENT
: '/*' .*? '*/' -> channel(2)
;
LINE_COMMENT
: '//' ~[\r\n]* -> channel(2)
;
AssignOP
: ':' OPChar* '='
;
CondAndOP
: '&' OPSuffix
;
CondOrOP
: '||' OPSuffix
;
AndOP : '^&' OPSuffix
;
XorOP : '^~' OPSuffix
;
OrOP : '^|' OPSuffix
;
EqOP: ( '==' | '!=' ) OPSuffix
;
RelOP
: '<' OPCharMLT OPSuffix
| '>' OPCharMGT OPSuffix
;
ShiftOP
: '^<' | '^>>' OPSuffix
| '^>' ( OPCharMGT OPSuffix )?
;
AddOP
: ( '+' | '-' ) OPSuffix
;
MulOP
: ( '/' | '%' | '*' ) OPSuffix
;
UnaryOP
: ( '!' | '~' ) OPSuffix
;
fragment
OPSuffix
: OPChar* ( '_' IDFragment )?
;
fragment
OPChar
: ( '+' | '-' | '/' | '\\' | '*' | '%' | '&' | '|' | '?' | '>' | '<' | '=' | '~' | ':' )
;
fragment
OPCharMGT
: ( '+' | '-' | '/' | '\\' | '*' | '%' | '&' | '|' | '?' | '<' | '=' | '~' | ':' )
;
fragment
OPCharMLT
: ( '+' | '-' | '/' | '\\' | '*' | '%' | '&' | '|' | '?' | '>' | '=' | '~' | ':' )
;
fragment
IDFragment
: LETTER ( LETTER | DIGIT )*
;
HEX
: '0' ('x'|'X')
HexDigits
IntegerTypeSuffix?
;
DEC
: '-'? ( '0' | '1'..'9' ('_'* Digit)* ) IntegerTypeSuffix?
;
OCT
: '0' ('_'* '0'..'7')+ IntegerTypeSuffix?
;
BIN
: '0' ('b'|'B')
BinaryDigit ('_'* BinaryDigit)*
IntegerTypeSuffix?
;
fragment
BinaryDigit : ('0'|'1') ;
fragment
HexDigits : HexDigit ('_'* HexDigit)* ;
fragment
HexDigit : (Digit|'a'..'f'|'A'..'F') ;
fragment
Digits : Digit ('_'* Digit)* ;
fragment
Digit : '0'..'9' ;
fragment
IntegerTypeSuffix : 'l' | 'L' | 'i'| 'I';
FLOAT
: '-'? Digits '.' Digits? Exponent? FloatTypeSuffix?
| '-'? '.' Digits Exponent? FloatTypeSuffix?
| '-'? Digits Exponent FloatTypeSuffix?
| '-'? Digits FloatTypeSuffix
// Hex float literal
| ('0x' | '0X')
HexDigits? ('.' HexDigits?)?
( 'p' | 'P' ) ( '+' | '-' )? Digits // note decimal exponent
FloatTypeSuffix?
;
fragment
Exponent : ('e'|'E') ('+'|'-')? Digits ;
fragment
FloatTypeSuffix : ('f'|'F'|'d'|'D') ;
CHAR
: '\'' ( EscapeSequence | ~('\''|'\\') ) '\''
;
STRING
: '"' ( EscapeSequence | ~('\\'|'"') )* '"'
;
fragment
EscapeSequence
: '\\' ('b'|'t'|'n'|'f'|'r'|'\"'|'\''|'\\')
| UnicodeEscape
| OctalEscape
;
fragment
OctalEscape
: '\\' ('0'..'3') ('0'..'7') ('0'..'7')
| '\\' ('0'..'7') ('0'..'7')
| '\\' ('0'..'7')
;
fragment
UnicodeEscape
: '\\' 'u' HexDigit HexDigit HexDigit HexDigit
;
// From JavaCC's grammar
fragment
LETTER
: '\u0024' // $
| '\u0041'..'\u005a' // A-Z
| '\u005f' // _
| '\u0061'..'\u007a' // a-z
| '\u00c0'..'\u00d6' // Latin Capital LETTER A with grave - Latin Capital letter O with diaeresis
| '\u00d8'..'\u00f6' // Latin Capital letter O with stroke - Latin Small LETTER O with diaeresis
| '\u00f8'..'\u00ff' // Latin Small LETTER O with stroke - Latin Small LETTER Y with diaeresis
| '\u0100'..'\u1fff' // Latin Capital LETTER A with macron - Latin Small LETTER O with stroke and acute
| '\u3040'..'\u318f' // Hiragana
| '\u3300'..'\u337f' // CJK compatibility
| '\u3400'..'\u3d2d' // CJK compatibility
| '\u4e00'..'\u9fff' // CJK compatibility
| '\uf900'..'\ufaff' // CJK compatibility
;
fragment
DIGIT
: '\u0030'..'\u0039' // 0-9
| '\u0660'..'\u0669' // Arabic-Indic Digit 0-9
| '\u06f0'..'\u06f9' // Extended Arabic-Indic Digit 0-9
| '\u0966'..'\u096f' // Devanagari 0-9
| '\u09e6'..'\u09ef' // Bengali 0-9
| '\u0a66'..'\u0a6f' // Gurmukhi 0-9
| '\u0ae6'..'\u0aef' // Gujarati 0-9
| '\u0b66'..'\u0b6f' // Oriya 0-9
| '\u0be7'..'\u0bef' // Tami 0-9
| '\u0c66'..'\u0c6f' // Telugu 0-9
| '\u0ce6'..'\u0cef' // Kannada 0-9
| '\u0d66'..'\u0d6f' // Malayala 0-9
| '\u0e50'..'\u0e59' // Thai 0-9
| '\u0ed0'..'\u0ed9' // Lao 0-9
| '\u1040'..'\u1049' // Myanmar 0-9?
;
ErrorChar
: .
;