/* ANTLR Grammar for OO-Action Systems (C) Willibald Krenn, 2009 - 2010 Notes ~~~~~ (*) No recursion (*) float acutally is fixed-point! (*) Named actions can only be "called" within the do-od block (*) Methods can be called from within an action and a method. Attention: Mutual Recursion not supported! FixMe ~~~~~ (*) List-Enum: Length Restriction! (Defaults to 500 for now) (*) subseteq missing History ~~~~~~~ Changes 1.03 to 1.04 ~ Fix bug with set constuctor: set with only one element produced wrong AST (inner element wasn't added correctly). Changes 1.02 to 1.03 + option to name objects when they are constructed: new (,"") Changes 1.00 to 1.02 + cast operator for objects ( ... as ) Changes 1.00 to 1.01 + enum-type with fixed integer values Changes 0.99b to 1.00 + constant section added (consts a=4; b=4) + limits of simple types and lists can be const + local vars allowed in methods (... = var... begin...end) + prioritized composition on statement level + skip in do-od block + filter expression in do-od block sequential var statement + fold operator Changes 0.99 to 0.99b - disabled sequential composition of action systems (remains in grammar, though out-commented) Changes 0.98 to 0.99 ~ changed QR syntax. Changes 0.97 to 0.98 ~ changed syntax for list and set comprehension list comprehension: '[' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? ']' set comprehension '{' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? '}' Usage: defined variables will sweep over value-range. If the latter expression (after '&') evaluates to true (hence this expression must return a bool) with the current valuation of the defined vars, the values are used to evaluate the first expression, which has to return a value of the correct type. Example: type myint = int [0..300000]; mytuple = (myint, myint) var l_tuple : list of mytuple = [nil]; l_int : list of myint = [nil]; ... l_int := [l_tuple[x][0] | var x: myint & x < len l_tuple ] + list element access by '[int]' allowed! Changes 0.96 to 0.97 + tuple-type initialization now properly supported + binary operator precedence handling + local variables in named actions + support for (). and (). ~ conditional expression: End required. - remove support for power-operator (may be we need to do calculation backwards) Changes 0.95 to 0.96 ~ string literals now ".." ~ priming of identifier access only supported at the end of the expression Changes 0.9 to 0.95 + composition of action systems in 'system' block ~ Produce C# code ~ Operator Precedence ~ vars in action composition ~ forall/extists now with colon instead of in Earlier changes removed. */ grammar ooa; options { language = CSharp2; k = 2; // output = AST; } @lexer::namespace { TUG.Mogentes } @lexer::header { /* Ulysses OO-Action System Parser Copyright Willibald Krenn 2009 */ } @parser::namespace { TUG.Mogentes } @parser::header { /* Ulysses OO-Action System Parser Copyright Willibald Krenn 2009 */ } ooActionSystems : {initializeTopLevelParserState();} (T_CONSTS namedConstList)? T_TYPES namedTypeList T_SYSTEM comp=asTypeComposition[null] {fixUpRun(comp);} ; // // ------------ named consts ------------ // namedConstList : namedConst (T_SEMICOLON namedConst)* ; namedConst : aName=T_IDENTIFIER T_EQUAL anExpr=expression {addNamedConst(aName,anExpr);} ; // // ------------ named types ------------ // namedTypeList : namedType (T_SEMICOLON namedType)* ; namedType : aName=T_IDENTIFIER T_EQUAL ( aType=complexType {createNamedType(aName,aType);} | anOoaType=ooActionSystem {createNamedType(aName,anOoaType);} ) ; asTypeComposition [IdentifierList top] returns [IdentifierList prioList] : {prioList = new PrioIdentifierList(top);} asTypeCompositionParallel[prioList] (T_PRIO asTypeCompositionParallel[prioList] )* ; asTypeCompositionParallel [IdentifierList top] : {IdentifierList parList = new NondetIdentifierList(top);} asTypeCompositionSequential[parList] (T_NONDET asTypeCompositionSequential[parList])* ; asTypeCompositionSequential [IdentifierList top] : {IdentifierList seqList = new SeqIdentifierList(top);} asTypeCompositionBlockParen[seqList] //(T_SEMICOLON asTypeCompositionBlockParen[seqList])* ; asTypeCompositionBlockParen [IdentifierList top] : T_LPAREN asTypeComposition[top] T_RPAREN | aName=T_IDENTIFIER {addToIdentifierList(top,aName);} ; // // ------------ basic types ------------ // complexType returns [UlyssesType aTypeSymbol] @init{ aTypeSymbol = null; alandmark = null; } : T_LIST T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN T_OF innertype=complexType {aTypeSymbol = createListType(numOfElements,innertype);} // list type with predefined elements (dupes of each element as many as needed) FIXME: Length Restriction! | T_LSQPAREN alistelem=T_IDENTIFIER {aTypeSymbol = createListEnumType(alistelem);} (T_COMMA otherlistelem=T_IDENTIFIER {addToListEnumType(aTypeSymbol,otherlistelem);})* T_RSQPAREN // set of identifiers.. // maps do not really need a length restriction, as simpleType already is restricted.. | T_MAP (T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN)? mapfromtype=simpleType T_TO maptotype=complexType {aTypeSymbol = createMapType(numOfElements,mapfromtype,maptotype);} // quantity space | T_QUANTITY T_OF T_LSQPAREN (alandmark=T_IDENTIFIER| alandmark=T_MINUS T_INFTY) {aTypeSymbol = createQrType(alandmark);} (T_COMMA (otherlandmark=T_IDENTIFIER|otherlandmark=T_INFTY) {addToQrType(aTypeSymbol,otherlandmark);})* T_RSQPAREN // tuple | T_LPAREN aType=complexType {aTypeSymbol = createTupleType(aType);} (T_COMMA anotherType=complexType {addToTupleType(aTypeSymbol,anotherType);})* T_RPAREN // some simple type (note that this includes identifiers, which may be complex object types..) | r=simpleType {aTypeSymbol = r;} ; finally {fixupComplexType(aTypeSymbol);} simpleType returns [UlyssesType aTypeSymbol] @init{ aTypeSymbol = null; } : T_BOOL {aTypeSymbol = createBoolType();} // ints plus subtypes | T_INT T_LSQPAREN rangeLow=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN {aTypeSymbol = createIntType(rangeLow,rangeHigh);} // floats plus subtypes | T_FLOAT T_LSQPAREN rangeLow=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN {aTypeSymbol = createFloatType(rangeLow,rangeHigh);} // char | T_CHAR {aTypeSymbol = createCharType();} // simple type, domain restricted to the values within the given set. (operators supported: equal, not equal) - may be casted to integer if // explicit int values are given | T_CBRL aRangeValue=T_IDENTIFIER (T_EQUAL optVal=T_INTNUMBER)? {aTypeSymbol = createEnumType(aRangeValue, optVal);} (T_COMMA otherRangeValue=T_IDENTIFIER (T_EQUAL otherOptVal=T_INTNUMBER)? {addToEnumType(aTypeSymbol,otherRangeValue,otherOptVal); otherOptVal=null;})* T_CBRR | aType=T_IDENTIFIER {aTypeSymbol = getNamedType(aType);} // alias could be simple type - otherwise, it's a complex type!! ; finally {fixupSimpleType(aTypeSymbol);} ooActionSystem returns [OoActionSystemType aTypeSymbol] @init{ bool autoCons = false; aTypeSymbol = null; refinesSystemName = null; } : (T_AUTOCONS {autoCons = true;})? T_SYSTEM (T_LPAREN refinesSystemName=T_IDENTIFIER T_RPAREN)? {aTypeSymbol = createOoaType(refinesSystemName,autoCons);} '|[' (T_VAR attrList)? (T_METHODS methodList)? (T_ACTIONS namedActionList)? (T_DO (bl=actionBlock[null] {addActionBlock(aTypeSymbol,bl);})? T_OD)? ']|' ; finally {fixupOoaType(aTypeSymbol);} // // ------------ variables (objects and simple types) ------------ // attrList : {BeginParsingAttributes();} attr (T_SEMICOLON attr)* ; finally { EndParsingAttributes(); } attr @init{ bool isStatic = false; bool isCtr = false; bool isObs = false; } : (T_STATIC {isStatic = true;})? (T_OBS {isObs = true;} | T_CTRL {isCtr = true;})? varname=T_IDENTIFIER T_COLON aType=complexType (T_EQUAL anExpr=expression)? {createAttribute(varname, isStatic, isObs, isCtr, aType, anExpr);} ; // // ------------ methods ------------ // methodList : method (T_SEMICOLON method)* ; method @init { FunctionIdentifier newMethod = null; } : mname=T_IDENTIFIER {newMethod = createMethodSymbol(mname);} (T_LPAREN methodParameterList[newMethod] T_RPAREN)? (T_COLON rt=complexType {setMethodReturnType(newMethod,rt);})? // actions can not have a return type!! T_EQUAL (T_VAR localActionVars[newMethod] 'begin')? statements=actionBody[null] {addMethodBody(newMethod,statements);} T_END ; finally {popResolveStack(newMethod);} methodParameterList[FunctionIdentifier newMethod] : paramName=T_IDENTIFIER T_COLON atype=complexType {addMethodParameter(newMethod,paramName,atype);} (T_COMMA otherparam=T_IDENTIFIER T_COLON othertype=complexType {addMethodParameter(newMethod,otherparam,othertype);} )* ; // // ------------ named, anonymous actions ------------ // namedActionList : namedAction (T_SEMICOLON namedAction)* ; namedAction @init { FunctionTypeEnum actionType; FunctionIdentifier newAction = null; } : T_CONT cactionname=T_IDENTIFIER {newAction = createNamedContinuousAction(cactionname, FunctionTypeEnum.Continuous);} (T_LPAREN methodParameterList[newAction] T_RPAREN)? T_EQUAL constraints=continuousActionBody {addContinuousActionBody(newAction,constraints);} | {actionType = FunctionTypeEnum.Internal;} (T_CTRL {actionType = FunctionTypeEnum.Controllable;}| T_OBS {actionType = FunctionTypeEnum.Observable;}| ) actionname=T_IDENTIFIER {newAction = createNamedAction(actionname,actionType);} (T_LPAREN methodParameterList[newAction] T_RPAREN)? T_EQUAL (T_VAR localActionVars[newAction] )? body=discreteActionBody {addActionBody(newAction,body);} ; finally {popResolveStack(newAction);} localActionVars[FunctionIdentifier newMethod] : // a named, discrete action may have local variables. id1=T_IDENTIFIER T_COLON t1=complexType {addLocalVariableToNamedAction(newMethod,id1,t1);} (T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType {addLocalVariableToNamedAction(newMethod,id2,t2);} )* ; anonymousAction returns [GuardedCommand result] : a=continuousActionBody {result = a;} | b=discreteActionBody {result = b;} ; continuousActionBody returns [GuardedCommand result] @init { result = null; } : T_CONT T_REQUIRES expr=expression T_COLON bdy=qualConstraintList T_END {result = createGuardedCommandStatement(expr,bdy,true);} ; qualConstraintList returns [Block result] @init{ result = createSeqBlock(null); pushBlockToResolveStack(result); } : stmt=qualConstraint {addToBlockList(result,stmt);} (T_COMMA ostmt=qualConstraint {addToBlockList(result,ostmt);})* ; finally {popBlockFromResolveStack(result);} qualConstraint returns [QualitativeConstraintStatement result] : id1=T_IDENTIFIER T_EQUAL ( T_DERIV derivid=T_IDENTIFIER {result = createQualDerivConstraintStatement(id1,derivid);} | id2=T_IDENTIFIER ( ( op=T_SUM | op=T_DIFF | op=T_PROD ) id3=T_IDENTIFIER {result = createQualArithConstraintStatement(id1,id2,id3,op);} | {result = createQualEqualConstraintStatement(id1,id2);} ) ) ; discreteActionBody returns [GuardedCommand result] @init{ result = null; } : T_REQUIRES expr=expression T_COLON bdy=actionBody[null] T_END {result = createGuardedCommandStatement(expr,bdy);} ; // // ------------ do-od block ------------ // actionBlock [Block top] returns [Block prioList] : {prioList = createPrioBlock(top);} actionBlockParallel[prioList] (T_PRIO actionBlockParallel[prioList])* ; actionBlockParallel [Block top] : {Block parList = createNondetBlock(top);} actionBlockSequential[parList] (T_NONDET actionBlockSequential[parList])* ; // atomic sequential composition of actions actionBlockSequential [Block top] @init { Block seqList = createSeqBlock(top); pushBlockToResolveStack(seqList); } : (T_VAR syms=blockvarlist[seqList] ('&' sexpr=expression {addSeqBlockExpression(seqList,sexpr);} )? T_COLON )? actionBlockParen[seqList] (T_SEMICOLON actionBlockParen[seqList])* ; finally {popBlockFromResolveStack(seqList);} actionBlockParen [Block top] : T_LPAREN actionBlock[top] T_RPAREN | anonymousOrNamedAction[top] ; anonymousOrNamedAction [Block top] : gcmd=anonymousAction {addToBlockList(top,gcmd);} | aname=T_IDENTIFIER (T_LPAREN m_params=methodCallParams T_RPAREN)? (amap=(T_FOLDLR|T_FOLDRL) '(' amapexpr=expression ')')? {addNamedActionCallToBlockList(top,aname,m_params,amap,amapexpr);} | T_SKIP {addSkipStatementToBlockList(top);} ; blockvarlist [Block seqList] : blockvar[seqList] (T_SEMICOLON blockvar[seqList] )* ; blockvar [Block seqList] : varname=T_IDENTIFIER T_COLON aType=complexType {addBlockVariable(seqList,varname,aType);} ; // // ------------ action body of non-continuous actions ------------ // actionBody[Block top] returns [Block result] : {result = createPrioBlock(top);} actionBodyParallel[result] (T_PRIO actionBodyParallel[result])? ; actionBodyParallel[Block top] returns [Block result] : {result = createNondetBlock(top);} actionBodySequential[result] (T_NONDET olst=actionBodySequential[result])* ; // seq binds stronger than nondet, i.e. a;b;cd;e is read as (a;b;c)[](d;e) actionBodySequential[Block top] returns [Block result] : {result = createSeqBlock(top);} actionBodyParen[result] (T_SEMICOLON actionBodyParen[result])* ; actionBodyParen [Block top] : T_LPAREN actionBody[top] T_RPAREN | stmt=statement {addToStatementList(top,stmt);} ; statement returns [Statement result] @init { bool popFromResolveStack = false; result = null; } : T_ABORT {result = createAbortStatement();} | T_SKIP {result = createSkipStatement();} | T_KILL T_LPAREN aname=(T_IDENTIFIER | T_SELF) T_RPAREN {result = createKillStatement(aname);} | gc=discreteActionBody {result = gc;} | aqname=reference ( // single assignment T_ASSIGNMENT aexp=expression {result = createSingleAssignmentStatement(aqname,aexp);} (T_WITH ndexp=expression {addConstraintToAssignment(result,ndexp);})? // nondet assignment // multi assignment | {result = createMultipleAssignmentStatementLHS(aqname);} (T_COMMA malhs=reference {addMultipleAssignmentStatementLHS(result,malhs);})+ T_ASSIGNMENT {pushAssignmentOnResolveStack(result); popFromResolveStack = true;} mexp=expression {addMutlipleAssignmentStatementRHS(result,mexp);} (T_COMMA mexp2=expression {addMutlipleAssignmentStatementRHS(result,mexp2);})+ (T_WITH ndex2=expression {addConstraintToAssignment(result,ndex2);})? // nondet assignment // just a call of a method. | {result = createCallStatement(aqname);} ) ; finally { if (popFromResolveStack == true) popAssignmentOffResolveStack(result); } // // ------------ expression ------------ // expression returns [Expression expr] @init{ System.Collections.Generic.List operators = new System.Collections.Generic.List(); System.Collections.Generic.List expressions = new System.Collections.Generic.List(); } : left=atomExpression {expressions.Add(left);} ( op=binoperator right=atomExpression { operators.Add(op); expressions.Add(right); } )* {expr = createPrecedenceTree(expressions,operators);} ; binoperator returns [BinaryOperator binop] : T_BIIMPLIES {binop = createBinaryOperator(ExpressionKind.biimplies);} | T_GREATER {binop = createBinaryOperator(ExpressionKind.greater);} | T_GREATEREQUAL {binop = createBinaryOperator(ExpressionKind.greaterequal);} | T_LESS {binop = createBinaryOperator(ExpressionKind.less);} | T_LESSEQUAL {binop = createBinaryOperator(ExpressionKind.lessequal);} | T_EQUAL // bool, numeric, char, lists, maps {binop = createBinaryOperator(ExpressionKind.equal);} | T_NOTEQUAL // bool, numeric, char, lists, maps {binop = createBinaryOperator(ExpressionKind.notequal);} | T_IMPLIES {binop = createBinaryOperator(ExpressionKind.implies);} | T_MINUS {binop = createBinaryOperator(ExpressionKind.minus);} | T_SUM {binop = createBinaryOperator(ExpressionKind.sum);} | T_IN T_SET? // A * list of A -> bool {binop = createBinaryOperator(ExpressionKind.elemin);} | T_NOT T_IN T_SET? // A * list of A -> bool {binop = createBinaryOperator(ExpressionKind.notelemin);} | T_SUBSET // list of A * list of A -> bool (does not respect dupes) {binop = createBinaryOperator(ExpressionKind.subset);} | T_OR {binop = createBinaryOperator(ExpressionKind.or);} | T_DIV {binop = createBinaryOperator(ExpressionKind.div);} | T_PROD {binop = createBinaryOperator(ExpressionKind.prod);} | T_IDIV {binop = createBinaryOperator(ExpressionKind.idiv);} | T_MOD {binop = createBinaryOperator(ExpressionKind.mod);} | T_UNION // list of A * list of A -> list of A (does not respect dupes) {binop = createBinaryOperator(ExpressionKind.union);} | T_DIFF // list of A * list of A -> list of A (does not respect dupes) {binop = createBinaryOperator(ExpressionKind.diff);} | T_INTER // list of A * list of A -> list of A (does not respect dupes) {binop = createBinaryOperator(ExpressionKind.inter);} | T_AND {binop = createBinaryOperator(ExpressionKind.and);} | T_POW {binop = createBinaryOperator(ExpressionKind.pow);} | T_CONC // list of A * list of A -> list of A {binop = createBinaryOperator(ExpressionKind.conc);} | T_DOMRESBY // list of A * map A to B -> map A to B {binop = createBinaryOperator(ExpressionKind.domresby);} | T_DOMRESTO // list of A * map A to B -> map A to B {binop = createBinaryOperator(ExpressionKind.domresto);} | T_RNGRESBY // map A to B * list of B -> map A to B {binop = createBinaryOperator(ExpressionKind.rngresby);} | T_RNGRESTO // map A to B * list of B -> map A to B {binop = createBinaryOperator(ExpressionKind.rngresto);} | T_MUNION // map A to B * map A to B -> map A to B {binop = createBinaryOperator(ExpressionKind.munion);} | T_SEQMOD_MAPOVERRIDE // list of A * map int to A -> list of A or // map A to B * map A to B -> map A to B {binop = createBinaryOperator(ExpressionKind.seqmod_mapoverride);} ; atomExpression returns [Expression expr] @init { expr = null; } : (unexpr=op_un? ( e=identifierExpression | e=qvalExpression | e=constant | e=initializedComplexType | e=quantifierExpression | T_LPAREN e=expression T_RPAREN ( (T_POINT idn=T_IDENTIFIER {e = addIdentifierAccessExpression(e,idn);})+ (res=accessExpression[e] {e=res;})? | e=accessExpression[e] )? ) ('as' cid=T_IDENTIFIER {e=addCastExpression(e,cid);})? {expr = addUnaryExpression(unexpr,e);} ) | ie=T_IF ce=expression T_THEN te=expression T_ELSE ee=expression T_END {expr = createConditionalExpression(ce,te,ee,ie);} ; quantifierExpression returns [Quantifier result] @init { result = null; } : t=(T_FORALL | T_EXISTS) {result = createQuantifierExpression(t);} (id=T_IDENTIFIER (T_COLON id_type=simpleType {addBoundVarToQuantifierExpression(result,id,id_type);}) (T_COMMA id2=T_IDENTIFIER (T_COLON id_type2=simpleType){addBoundVarToQuantifierExpression(result,id2,id_type2);})*) T_COLON T_LPAREN e=expression T_RPAREN {addExpressionToQuantifier(result,e);} ; finally {removeBoundVarsFromResolveStack(result);} constant returns [LeafExpression result] @init { result = null; } : T_TRUE {result = createBoolConstant(true);} | T_FALSE {result = createBoolConstant(false);} | T_NIL {result = createNullPointerConstant();} | T_SELF {result = createSelfPointer();} | t_fl=T_FLOATNUMBER {result = createFloatConstant(t_fl);} | t_in=T_INTNUMBER {result = createIntConstant(t_in);} | t_l=T_STRINGLITERAL {result = createStringConstant(t_l);} ; initializedComplexType returns [Expression result] @init { result = null; } : res=initializedListType {result = res;} | res=initializedSetType {result = res;} | T_NEW T_LPAREN anid=T_IDENTIFIER ( T_COMMA aname=T_STRINGLITERAL T_RPAREN {result = createNamedObject(anid, aname);} | T_RPAREN {result = createObject(anid);} // constructor call.. ) ; initializedListType returns [ListConstructor result] @init { result = createInitializedList(); pushListVarsOnResolveStack(result); // need this here for list comprehension } : T_LSQPAREN e=expression {addListElement(result,e);} ( (T_COMMA e2=expression {addListElement(result,e2);})+ | listComprehension[result] )? T_RSQPAREN ; finally {popListVarsFromResolveStack(result);} listComprehension [ListConstructor result] @init{ result.SetHasComprehension(true); } : T_BAR T_VAR id=T_IDENTIFIER T_COLON t1=complexType {addListComprVar(result,id,t1);} (T_SEMICOLON id2=T_IDENTIFIER t2=complexType {addListComprVar(result,id2,t2);})* ('&' e=expression {addListComprExpr(result,e);})? ; initializedSetType returns[Expression result] @init { result = null; } : T_CBRL T_MAPS T_CBRR {result = createEmptyMap();} // empty map | res=initializedSet {result = res;} ; initializedSet returns [Expression result] @init { SetConstructor theset = createSet(); pushSetVarsOnResolveStack(theset); // need this here for set comprehension result = theset; } : T_CBRL e1=expression ( // set constructor; empty set: {nil} {addToSet(result,e1);} (T_COMMA e2=expression {addToSet(result,e2);})* // set constructor for sets > 1 elem | m=map[result, e1] {result = m;} // we have a set in the resolution stack, but this should be fine (no syms) | {addToSet(result,e1);} setComprehension[(SetConstructor)result] // set comprehension ) T_CBRR ; finally {popSetVarsFromResolveStack(theset);} map[Expression _map, Expression e1] returns [Expression result] @init { result = null; } : am=T_MAPS e2=expression {result = createMap(e1,e2,am);} (T_COMMA e3=expression T_MAPS e4=expression {addToMap(result,e3,e4);})* ; setComprehension[SetConstructor _set] @init { _set.SetHasComprehension(true); } : T_BAR T_VAR (id1=T_IDENTIFIER T_COLON t1=complexType { addSetComprVar(_set, id1, t1); } T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType { addSetComprVar(_set, id2, t2); })* ('&' epx=expression { addSetComprExpr(_set,epx); })? ; qvalExpression returns [QValConstructor result] @init { bool minus = false; result = null; } : // constructor for qualitative values aval='qval' T_LPAREN {result = createQualitativeValue(aval);} ( T_NIL {setQualitativeValueDontCare(result);} | ( expr=qualifiedIdentifier {setQualitativeValueLandmark(result,expr);} | ('-' {minus = true;})? T_INFTY {setQualitativeValueInfinity(result,minus);} ) (T_RANGETO ( expr2=qualifiedIdentifier {setQualitativeValueRange(result,expr2);} | T_INFTY {setQualitativeValueRangeInfinity(result,false);} ) )? ) T_COMMA ( T_NIL {setQualitativeDerivDontCare(result);} | ( 'steady' {setQualitativeDerivSteady(result);} | 'inc' {setQualitativeDerivInc(result);} | 'dec' {setQualitativeDerivDec(result);} ) ) T_RPAREN ; identifierExpression returns [Expression result] : // if next token is a tuple-type then create an initialized tuple! {isTuple(input.LT(1).Text)}? aName=T_IDENTIFIER T_LPAREN m_params=methodCallParams T_RPAREN {result = createInitializedTuple(aName,m_params);} | // is some sort of reference res=reference {result = res;} ; reference returns [Expression result] @init { result = null; init = null; } : {!isTuple(input.LT(1).Text)}? // check that the next token is not a reference to a tuple-type aName=qualifiedIdentifier {result = aName;} ( output=accessExpression[result] {result = output;} // call expression | // variable access or method call that takes no params? (do we allow for that? - answer: no!) ) ( pr=T_PRIMED {setIdentifierExpressionPrimed(ref result,pr);} | ('::' T_LPAREN init=expression T_RPAREN)? afold=(T_FOLDLR|T_FOLDRL) T_LPAREN anexpr=expression T_RPAREN {result = createFoldExpression(result,afold,init,anexpr);} )? ; accessExpression[Expression subexpr] returns [Expression result] @init{ UnaryOperator newExpr = null; result = subexpr; } : ( tcall=T_LSQPAREN ac=expression T_RSQPAREN // access tuples, maps { result = createTupleMapAccessExpression(result,ac,tcall); } | bcall=T_LPAREN m_params=methodCallParams T_RPAREN // access method { result = createMethodAccessExpression(result,m_params,bcall); } )+ ( // a[1].c.e()... (T_POINT idn=T_IDENTIFIER {result = addIdentifierAccessExpression(result,idn);})+ (res=accessExpression[result] {result=res;})? )? ; qualifiedIdentifier returns [Expression top] @init { IdentifierExpression selfexpr = null; top = null; } : (self=T_SELF T_POINT {selfexpr = createSelfIdentifierExpression(self);})? idb=T_IDENTIFIER {top = createIdentifierAccessExpression(selfexpr,idb);} (T_POINT idd=T_IDENTIFIER {top = addIdentifierAccessExpression(top,idd);})* ; methodCallParams returns [System.Collections.Generic.List result] @init { result = new System.Collections.Generic.List(); } : (expa=expression {result.Add(expa);} (T_COMMA expb=expression {result.Add(expb);})*)? ; // // ------------ unary Operators ------------ // op_un returns [UnaryOperator expr] @init { expr = null; } : r=op_un_set_list {expr = r;} | r2=op_un_map {expr = r2;} | T_MINUS {expr = createUnaryOperator(ExpressionKind.unminus);} | T_NOT {expr = createUnaryOperator(ExpressionKind.not);} | T_ABS {expr = createUnaryOperator(ExpressionKind.abs);} ; op_un_set_list returns [UnaryOperator expr] @init { expr = null; } : T_CARD // list of A -> int (does not respect dupes, i.e. dupes do not count) {expr = createUnaryOperator(ExpressionKind.card);} | T_DCONC // list of list of A -> list of A {expr = createUnaryOperator(ExpressionKind.dconc);} | T_DINTER // list of list of A -> list of A (intersection, does not respect dupes) {expr = createUnaryOperator(ExpressionKind.dinter);} | T_DUNION // list of list of A -> list of A (union, does not respect dupes) {expr = createUnaryOperator(ExpressionKind.dunion);} | T_ELEMS // list of A -> list of A (does not respect dupes) {expr = createUnaryOperator(ExpressionKind.elems);} | T_HEAD // list of A -> A {expr = createUnaryOperator(ExpressionKind.head);} | T_INDS // list of A -> list of int {expr = createUnaryOperator(ExpressionKind.inds);} | T_LEN // list of A -> int (dupes count) {expr = createUnaryOperator(ExpressionKind.len);} | T_TAIL // list of A -> list of A {expr = createUnaryOperator(ExpressionKind.tail);} ; op_un_map returns [UnaryOperator expr] @init { expr = null; } : T_DOM // map A to B -> list of A {expr = createUnaryOperator(ExpressionKind.dom);} | T_RNG // map A to B -> list of B {expr = createUnaryOperator(ExpressionKind.range);} | T_MERGE // list of map A to B -> map A to B {expr = createUnaryOperator(ExpressionKind.merge);} ; // // ============== LEXER ================= // T_WS : (' '|'\r'|'\t'|'\u000C'|'\n') {$channel=HIDDEN;} ; T_COMMENT : '/*' .* '*/' {$channel=HIDDEN;} ; LINE_COMMENT : '#' ~('\n'|'\r')* '\r'? '\n' {$channel=HIDDEN;} ; T_PRIMED : '\''; T_STRINGLITERAL : '"' ( ( '"' '"' )=> '"' | ~'"' )* '"' ; T_ABORT : 'abort'; T_ACTIONS : 'actions'; T_ASSIGNMENT : ':='; T_AUTOCONS: 'autocons'; T_BAR : '|'; T_BOOL : 'bool'; T_CBRL : '{'; T_CBRR : '}'; T_COLON : ':'; T_COMMA : ','; T_CONT : 'qual'; T_CHAR : 'char'; T_CTRL : 'ctr'; T_SYSTEM : 'system'; T_DO : 'do'; T_ELSE : 'else'; T_END : 'end'; T_EQUAL : '='; T_EXISTS: 'exists'; T_FLOAT : 'float'; T_FORALL: 'forall'; T_FALSE : 'false'; T_IF : 'if'; T_IN : 'in'; T_INT : 'int'; T_KILL : 'kill'; T_LIST : 'list'; T_LPAREN: '('; T_LSQPAREN: '['; T_MAP : 'map'; T_MAPS : '->'; T_METHODS : 'methods'; T_NEW : 'new'; T_NIL : 'nil'; T_NONDET: '[]'; T_OBS : 'obs'; T_OD : 'od'; T_OF : 'of'; T_PRIO : '//'; T_REQUIRES : 'requires'; T_RPAREN: ')'; T_RSQPAREN: ']'; T_QUANTITY : 'qspace'; T_SELF : 'self'; T_SET : 'set'; T_SEMICOLON : ';'; T_STATIC: 'static'; T_SKIP : 'skip'; T_THEN : 'then'; T_TRUE : 'true'; T_TO : 'to'; T_TYPES : 'types'; T_VAR : 'var'; T_WITH : 'with'; // for nondet assignment //T_ACTION: 'action'; //BOOL T_AND : 'and'; T_BIIMPLIES : '<=>'; T_IMPLIES : '=>'; //VDM-Style T_NOT : 'not'; //VDM-Style T_NOTEQUAL: '<>'; //VDM-Style T_OR : 'or'; //Numeric (equal, not equal same as in BOOL) T_ABS : 'abs'; T_DIV : '/'; T_GREATER : '>'; T_GREATEREQUAL : '>='; T_IDIV : 'div'; T_LESS : '<'; T_LESSEQUAL : '<='; //VDM-Style T_MOD : 'mod'; //VDM-Style T_POW : '**'; T_PROD : '*'; T_DERIV : 'dt'; // set/list T_CARD : 'card'; T_CONC : '^'; T_DCONC : 'conc'; T_DIFF : '\\'; T_DINTER: 'dinter'; T_DUNION: 'dunion'; T_ELEMS : 'elems'; T_HEAD : 'hd'; T_INDS : 'inds'; T_INTER : 'inter'; T_LEN : 'len'; // differs from T_CARD, as card does not count dupes.. T_SEQMOD_MAPOVERRIDE : '++'; T_SUBSET: 'subset'; T_TAIL : 'tl'; T_UNION : 'union'; T_FOLDLR : ':>:'; T_FOLDRL : ':<:'; // maps T_DOM : 'dom'; T_DOMRESBY : '<-:'; T_DOMRESTO : '<:'; T_RNG : 'rng'; T_RNGRESBY : ':->'; T_RNGRESTO : ':>'; T_MERGE : 'merge'; T_MUNION: 'munion'; T_CONSTS: 'consts'; // numbers T_INFTY : (T_MINUS|T_SUM)? 'inf' ; // INTNUMBER, FLOATNUMBER, RANGETO, T_MINUS, T_PLUS are set within // FLOAT_OR_INT_OR_RANGE fragment T_INTNUMBER : ; fragment T_FLOATNUMBER : ; fragment T_RANGETO : ; FLOAT_OR_INT_OR_RANGE : (T_MINUS|T_SUM)? T_DIGIT+ ( // at this stage, we could face an int, int..int (=range), int.exp (=float), int.exp..int.exp (=float range) etc.. (T_POINT T_POINT) => {$type=T_INTNUMBER;} | (T_POINT T_DIGIT) => T_POINT T_DIGIT+ (('e'|'E') (T_MINUS|T_SUM)? T_DIGIT+)? {$type=T_FLOATNUMBER;} | {$type=T_INTNUMBER;} ) | T_POINT ( // could be point or range.. T_POINT {$type=T_RANGETO;} | {$type=T_POINT;} ) | T_MINUS {$type=T_MINUS;} | T_SUM {$type=T_SUM;} ; fragment T_MINUS: '-'; fragment T_SUM : '+'; fragment T_POINT: '.'; // identifiers T_IDENTIFIER : T_LETTER (T_LETTER|T_DIGIT)* ; //T_PRIMEDIDENTIFIER // : T_IDENTIFIER '\''; fragment T_LETTER : '$' | 'A'..'Z' | 'a'..'z' | '_' ; fragment T_DIGIT: '0'..'9';