OoasTools

/*  

			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 (<class>,"<name>")

  Changes 1.00 to 1.02

  	+ cast operator for objects ( ... as <typename> )

  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 (<expression>).<reference> and

  	              (<expression>).<accessExpression>

  	~ 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<BinaryOperator> operators = new System.Collections.Generic.List<BinaryOperator>();

		System.Collections.Generic.List<Expression> expressions = new System.Collections.Generic.List<Expression>();		

	}

	:	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<Expression> result]

	@init {

		result = new System.Collections.Generic.List<Expression>();

	}

	:	(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';