OoasTools

/**

  *

  *                      OOAS Compiler

  *

  *       Copyright 2015, AIT Austrian Institute of Technology.

  * This code is based on the C# Version of the OOAS Compiler, which is

  * copyright 2015 by the Institute of Software Technology, Graz University

  * of Technology with portions copyright by the AIT Austrian Institute of

  * Technology. All rights reserved.

  *

  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.

  *

  * If you modify the file please update the list of contributors below to in-

  * clude your name. Please also stick to the coding convention of using TABs

  * to do the basic (block-level) indentation and spaces for anything after

  * that. (Enable the display of special chars and it should be pretty obvious

  * what this means.) Also, remove all trailing whitespace.

  *

  * Contributors:

  *               Willibald Krenn (AIT)

  *               Stephan Zimmerer (AIT)

  *               Markus Demetz (AIT)

  *               Christoph Czurda (AIT)

  *

  */

package org.momut.ooas.parser;

import java.util.LinkedHashMap;

import java.util.LinkedList;

import java.util.List;

import org.antlr.runtime.MismatchedTokenException;

import org.antlr.runtime.Parser;

import org.antlr.runtime.RecognitionException;

import org.antlr.runtime.RecognizerSharedState;

import org.antlr.runtime.Token;

import org.antlr.runtime.TokenStream;

public class ooaCustomParser extends Parser

{

	public ParserState pState;

	public boolean IsRightToLeft(ExpressionKind type)

	{

		return type == ExpressionKind.implies; // implication has right grouping

	}

	public int GetOperatorPrecedence(ExpressionKind type)

	{

		switch (type)

		{

		/*Family of Evaluators*/

		case abs:    // T_ABS:

		case card:   // T_CARD:

		case dom:    // T_DOM:

		case range:  // T_RNG:

		case merge:  // T_MERGE:

		case len:    // T_LEN:

		case elems:  // T_ELEMS:

		case head:   // T_HEAD:

		case tail:   // T_TAIL:

		case conc:   // T_CONC:

		case inds:   // T_INDS:

		case dinter: // T_DINTER:

		case dunion: // T_DUNION:

			return 1;

		case domresby:   // T_DOMRESBY:

		case domresto:   // T_DOMRESTO:

		case rngresby:   // T_RNGRESBY:

		case rngresto:   // T_RNGRESTO:

			return 2;

		case div:    // T_DIV:

		case idiv:   // T_IDIV:

		case mod:    // T_MOD:

		case prod:   // T_PROD:

		case inter:  // T_INTER:

			return 3;

		case sum:    // T_SUM:

		case minus:  // T_MINUS:

		case union:  // T_UNION:

		case diff:   // T_DIFF:

		case munion: // T_MUNION:

		case seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:

			return 4;

			/*Family of Relations*/

		case less:

		case lessequal:

		case greater:

		case greaterequal:

		case equal:

		case notequal:

		case subset:

		case elemin:

		case notelemin:

			return 5;

			/*Family of Connectives*/

		case and:    // T_AND:

			return 6;

		case or:     // T_OR:

			return 7;

		case implies:    // T_IMPLIES:

			return 8;

		case biimplies:  // T_BIIMPLIES:

			return 9;

		default:

			throw new NotImplementedException("operator not supported: " + type.toString());

			// return 0;

		}

	}

	/*taken from antlr homepage:

     http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser

	 */

	int findPivot(List<BinaryOperator> operators, int startIndex, int stopIndex)

	{

		int pivot = startIndex;

		final BinaryOperator binop = operators.get(pivot);

		int pivotRank = GetOperatorPrecedence(binop.kind());

		for (int i = startIndex + 1; i <= stopIndex; i++)

		{

			final ExpressionKind type = operators.get(i).kind();

			final int current = GetOperatorPrecedence(type);

			final boolean rtl = IsRightToLeft(type);

			if (current > pivotRank || (current == pivotRank && rtl))

			{

				pivot = i;

				pivotRank = current;

			}

		}

		return pivot;

	}

	Expression createPrecedenceTree(

			List<Expression> expressions,

			List<BinaryOperator> operators,

			int startIndex,

			int stopIndex)

	{

		if (stopIndex == startIndex)

			return expressions.get(startIndex);

		final int pivot = findPivot(operators, startIndex, stopIndex - 1);

		final BinaryOperator result = operators.get(pivot);

		result.SetLeftChild(createPrecedenceTree(expressions, operators, startIndex, pivot));

		result.SetRightChild(createPrecedenceTree(expressions, operators, pivot + 1, stopIndex));

		return result;

	}

	Expression createPrecedenceTree(List<Expression> expressions, List<BinaryOperator> operators)

	{

		return createPrecedenceTree(expressions, operators, 0, expressions.size() - 1);

	}

	/* add error message to state. */

	private void doError(Token aToken, String aMessage)

	{

		pState.AddErrorMessage(

				new ParserError(pState.filename, aToken, aMessage));

	}

	/* add warning message to state */

	private void doWarning(Token id1, String p)

	{

		pState.AddWarningMessage(new ParserWarning(pState.filename, id1, p));

	}

	private void doError(String aMessage)

	{

		pState.AddErrorMessage(

				new ParserError(pState.filename, 0, 0, aMessage));

	}

	/* init global state */

	 void initializeTopLevelParserState()

	{

		pState.ooaSystem = new MainModule();

		pState.PushResolveStack(pState.ooaSystem);

	}

	private IScope GetScope()

	{

		return pState.currentScope;

	}

	/*create a named constant*/

	 void addNamedConst(Token aName, Expression anExpr)

	{

		if (pState.currentScope.ResolveIdentifier(aName.getText()) == null)

		{

			/* needs to be a constant... */

			final ConstantIdentifier aConst = new ConstantIdentifier(aName, anExpr, GetScope());

			final OoaResolveExpressionsVisitor resolver = new OoaResolveExpressionsVisitor(pState);

			aConst.Accept(resolver);

			if (aConst.Value() == null || aConst.Value().type() == null || aConst.Value().kind() != ExpressionKind.Value)

			{

				doError(aName, String.format("%s not a constant!", aName.getText()));

			}

			else

			{

				aConst.SetType(aConst.Value().type());

				pState.currentScope.AddIdentifier(aConst, null);

			}

		}

		else

			doError(aName, String.format("%s already defined!", aName.getText()));

	}

	/* create a named type; we're on top-level here */

	 void createNamedType(Token aName, UlyssesType aType)

	{

		// precond..

		assert(aName != null);

		if (aType == null)

		{

			doError(aName, String.format("%s lacks a type! (Type not added)", aName.getText()));

			return;

		}

		if (pState.currentScope.ResolveIdentifier(aName.getText()) == null)

		{

			final TypeIdentifier newid = new TypeIdentifier(aName, aType, GetScope());

			aType.SetTypeIdentifier(newid);

			pState.currentScope.AddIdentifier(newid, null);

		}

		else

			doError(aName, String.format("%s already defined!", aName.getText()));

	}

	/* create basic structure for an ooa-system descr. resolve stack TOS is now ooa-system symbols */

	OoActionSystemType createOoaType(Token refinesSystemName, boolean autoCons)

	{

		final Identifier refinedSystem = pState.Lookup(refinesSystemName);

		OoActionSystemType refinedSystemType = null;

		if ((refinedSystem != null) && (refinedSystem.type() != null))

		{

			if (refinedSystem.type().kind() != TypeKind.OoActionSystemType)

				doError(refinesSystemName,

						String.format("%s not an object oriented action system", refinesSystemName.getText()));

			else

				refinedSystemType = (OoActionSystemType)refinedSystem.type();

		}

		else if (refinesSystemName != null)

		{

			pState.AddErrorMessage(

					new ParserError(pState.filename, refinesSystemName,

							String.format("Type that's being refined (%s) not found!", refinesSystemName.getText())));

		}

		final OoActionSystemType result = new OoActionSystemType(autoCons, refinedSystemType, null);

		// add 'self' to the symbols.. (self is a keyword, so it can't be defined)

		result.AddIdentifier(new SelfTypeIdentifier("self", result, GetScope()), null);

		pState.PushResolveStack(result);

		return result;

	}

	/* remove ooa-system symbols from resolve stack TOS */

	void fixupOoaType(OoActionSystemType aTypeSymbol)

	{

		if (aTypeSymbol == null)

			return;

		aTypeSymbol.SetupAnonymousName();

		if (aTypeSymbol != null)

			pState.PopResolveStack();

	}

	Expression addCastExpression(Expression e, Token cid)

	{

		assert(e != null);

		final Expression result = new UnaryOperator(ExpressionKind.Cast, e, cid.getLine(), cid.getCharPositionInLine());

		result.SetType(new OpaqueType(new TypeIdentifier(cid, null, GetScope())));

		pState.typesToFixUp.add((OpaqueType)result.type());

		return result;

	}

	/* add a new ooa to the list describing the composition of action systems */

	 void addToIdentifierList(IdentifierList top, Token aName)

	{

		assert(top != null);

		final Identifier aSym = pState.Lookup(aName);

		if (aSym == null)

		{

			doError(aName, String.format("Could not find ooa-system %s!", aName.getText()));

		}

		else if ((aSym.type() == null) || !(aSym.type().kind() == TypeKind.OoActionSystemType))

		{

			doError(aName, String.format("Referenced type (%s) does not have correct type!", aName.getText()));

		}

		else

		{

			final OoActionSystemType aType = (OoActionSystemType)aSym.type();

			if (aType.isInSystemDescription())

				doError(aName, String.format("Referenced type (%s) already used in composition!", aName.getText()));

			else

				aType.SetIsInSystemDescription(true);

			top.AddElement(aSym);

		}

	}

	/* does a fixup run after parsing */

	 void fixUpRun(IdentifierList sysDescr)

	{

		// set system descr.

		pState.ooaSystem.SetSystemDescription(sysDescr);

		// fixup named types

		FixupNamedTypes();

	}

	private void FixupNamedTypes()

	{

		/*named type refs that could not be resolved in the first run, have to

          be resolved now. */

		for (final OpaqueType ntype: pState.typesToFixUp)

		{

			if (ntype.resolvedType() == null)

			{

				//ntype.identifier

				final Identifier asym = pState.Lookup(ntype.identifier().tokenText(), ntype.identifier().definingScope());

				if ((asym == null) || (asym.kind() != IdentifierKind.TypeIdentifier))

				{

					final ParserError error = new ParserError(pState.filename, ntype.identifier().line(), ntype.identifier().column(),

							String.format("Can not resolve %s to a named type", ntype.identifier().tokenText()));

					pState.AddErrorMessage(error);

				}

				else

					ntype.SetResolvedType(asym.type());

			}

		}

		pState.typesToFixUp.clear();

	}

	private boolean TosIsActionSystem()

	{

		return pState.currentScope instanceof OoActionSystemType;

	}

	private int currentLine()

	{

		final Token token = input.LT(-1);

		return token == null ? 0 : token.getLine();

	}

	private int currentPos()

	{

		final Token token = input.LT(-1);

		return token == null ? 0 : token.getCharPositionInLine();

	}

	/* add var symbol to the current action system */

	void createAttribute(Token varname, boolean isStatic, boolean isObs, boolean isCtr, UlyssesType aType, Expression anExpr)

	{

		if (!TosIsActionSystem())

			return;

		if (aType == null)

		{

			doError(varname, String.format("%s lacks type!", varname.getText()));

		}

		if (anExpr == null)

		{

			doError(varname, String.format("%s lacks initializer!", varname.getText()));

		}

		if (isObs == true || isCtr == true)

			if (aType.kind() != TypeKind.QrType)

				doError(varname, "'obs' or 'ctr' on attributes only allowed for qualitative types");

		final AttributeIdentifier var = new AttributeIdentifier(varname, aType, GetScope(), anExpr, isStatic, isObs, isCtr);

		if (pState.currentScope.ResolveIdentifier(varname.getText()) == null)

			pState.currentScope.AddIdentifier(var, null);

		else

			doError(varname, String.format("Can not add %s: Symbol already defined!", varname.getText()));

	}

	/* create a boolean type */

	BoolType createBoolType()

	{

		return new BoolType(null);

	}

	/* create a char type */

	CharType createCharType()

	{

		return new CharType(null);

	}

	/* create an int type */

	@SuppressWarnings("unchecked")

	UlyssesType createIntType(Token rangeLow, Token rangeHigh)

	{

		int low = 0;

		int high = 0;

		if (rangeLow.getType() == ooaLexer.T_INFTY)

			doError(rangeLow, "Infinity not supported.");

		if (rangeLow.getType() == ooaLexer.T_INFTY)

			doError(rangeHigh, "Infinity not supported.");

		if (rangeLow.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(rangeLow, String.format("Constant %s not found", rangeLow.getText()));

			else if (aconst.type().kind() != TypeKind.IntType)

				doError(rangeLow, "Constant must be integer");

			else

				low = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

			try {

				low = Integer.parseInt(rangeLow.getText());

			} catch (final NumberFormatException e) {

				doError(rangeLow, "Can not convert to integer");

			}

		if (rangeHigh.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(rangeHigh, String.format("Constant %s not found", rangeHigh.getText()));

			else if (aconst.type().kind() != TypeKind.IntType)

				doError(rangeHigh, "Constant must be integer");

			else

				high = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

			try {

				high = Integer.parseInt(rangeHigh.getText());

			} catch (final NumberFormatException e) {

				doError(rangeLow, "Can not convert to integer");

			}

		if (high < low)

			doError(rangeHigh, "Lower bound greater than upper bound");

		return new IntType(low, high, null);

	}

	/* create a float type */

	 @SuppressWarnings("unchecked")

	UlyssesType createFloatType(Token rangeLow, Token rangeHigh)

	{

		float low = 0;

		float high = 0;

		if (rangeLow.getType() == ooaLexer.T_INFTY)

			doError(rangeLow, "Infinity not supported.");

		if (rangeLow.getType() == ooaLexer.T_INFTY)

			doError(rangeHigh, "Infinity not supported.");

		if (rangeLow.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(rangeLow, String.format("Constant %s not found", rangeLow.getText()));

			else if (aconst.type().kind() != TypeKind.FloatType)

				doError(rangeLow, "Constant must be float");

			else

				low = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

			try {

				low = Float.parseFloat(rangeLow.getText());

			} catch (final NumberFormatException e) {

				doError(rangeLow, "Can not convert to float (single)");

			}

		if (rangeHigh.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(rangeHigh, String.format("Constant %s not found", rangeHigh.getText()));

			else if (aconst.type().kind() != TypeKind.FloatType)

				doError(rangeHigh, "Constant must be integer");

			else

				high = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

			try {

				high = Float.parseFloat(rangeHigh.getText());

			} catch (final NumberFormatException e){

				doError(rangeHigh, "Can not convert to float (single)");

			}

		if (high < low)

			doError(rangeHigh, "Lower bound greater than upper bound");

		/* precision */

		final float afterc_low = low -  (float)Math.floor(low); //(float)Convert.ToInt32(low);

		final float afterc_high = high - (float)Math.floor(high); //(float)Convert.ToInt32(high);

		final float precision = afterc_low < afterc_high ? afterc_low : afterc_high;

		return new FloatType(low, high, precision, null);

	}

	/* create a list of an enumerated type */

	 UlyssesType createListEnumType(Token alistelem)

	{

		final EnumType hiddenEnumType = new EnumType(null);

		final ListType result = new ListType(hiddenEnumType, 500, null);

		addToListEnumType(result, alistelem);

		return result;

	}

	/* add a new enum symbol to a list with an anonymous enumerated type */

	 void addToListEnumType(UlyssesType aTypeSymbol, Token otherlistelem)

	{

		final EnumType enumtype = (EnumType)((ListType)aTypeSymbol).innerType();

		addToEnumType(enumtype, otherlistelem, null);

	}

	/* create a new enumerated type */

	 UlyssesType createEnumType(Token aRangeValue, Token anIntegerValue)

	{

		EnumType result;

		if (anIntegerValue == null)

			result = new EnumType(null);

		else

			result = new ValuedEnumType(null);

		addToEnumType(result, aRangeValue, anIntegerValue);

		return result;

	}

	/* add a new enum symbol to the enumerated type */

	 void addToEnumType(UlyssesType aTypeSymbol, Token otherRangeValue, Token anIntegerValue)

	{

		final EnumType anEnum = (EnumType)aTypeSymbol;

		if (anEnum.symbolTable().Defined(otherRangeValue.getText()))

		{

			doError(otherRangeValue, String.format("Element '%s' already defined!", otherRangeValue.getText()));

			return;

		}

		/* for now we allow the usage of enum-ids without specifying the actual enum type,

		 * e.g., x = some_enum_id, hence all enum identifier must be globally unique.

		 * This decision could be reverted at later time...

		 */

		final Identifier sym = pState.Lookup(otherRangeValue);

		if (sym != null)

		{

			doError(otherRangeValue, String.format("Element '%s' already defined!", otherRangeValue.getText()));

			return;

		}

		EnumIdentifier enumval;

		if (anIntegerValue == null)

		{

			if (aTypeSymbol instanceof ValuedEnumType)

			{

				doError(otherRangeValue, String.format("Element '%s' needs integer value!", otherRangeValue.getText()));

				return;

			}

			enumval = new EnumIdentifier(otherRangeValue, (EnumType)aTypeSymbol, GetScope());

		}

		else

		{

			if (!(aTypeSymbol instanceof ValuedEnumType))

			{

				doError(otherRangeValue, String.format("Element '%s' must not have integer value!", otherRangeValue.getText()));

				return;

			}

			enumval = new EnumIdentifier(otherRangeValue, Integer.parseInt(anIntegerValue.getText()), (EnumType)aTypeSymbol, GetScope());

		}

		((EnumType)aTypeSymbol).AddEnumSymbol(enumval);

		/* add the enum id to 'global' state */

		pState.currentScope.AddIdentifier(enumval, null);

	}

	/* get a named type */

	 UlyssesType getNamedType(Token aType)

	{

		UlyssesType result = null;

		final Identifier sym = pState.Lookup(aType);

		if (sym == null)

		{

			/* we might not have seen this type yet - so do a fixup run later */

			result = new OpaqueType(new TypeIdentifier(aType, null, GetScope()));

			pState.typesToFixUp.add((OpaqueType)result);

		}

		else if (sym.kind() == IdentifierKind.TypeIdentifier)

			result = ((TypeIdentifier)sym).type();

		else

			doError(aType, "Not a named type symbol: " + aType.getText());

		return result;

	}

	/* create a list type */

	 @SuppressWarnings("unchecked")

	UlyssesType createListType(Token numOfElements, UlyssesType innertype)

	{

		if (innertype == null)

			doError(numOfElements, "List type lacks proper element type (null)");

		int numElems = 0;

		if (numOfElements.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(numOfElements, String.format("Constant %s not found", numOfElements.getText()));

			else if (aconst.type().kind() != TypeKind.IntType)

				doError(numOfElements, "Constant must be integer");

			else

				numElems = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

		{

			try {

				numElems = Integer.parseInt(numOfElements.getText());

			} catch (final NumberFormatException e) {

				doError(numOfElements, "Not an integer");

			}

			if (numElems <= 0)

				doError(numOfElements, "Number of elements in a list must be >= 1");

		}

		final ListType result = new ListType(innertype, numElems, null);

		return result;

	}

	/* create a map type */

	 @SuppressWarnings("unchecked")

	UlyssesType createMapType(Token numOfElements, UlyssesType mapfromtype, UlyssesType maptotype)

	{

		if (mapfromtype == null)

			doError(numOfElements, "Map: From-type not set (null)");

		if (maptotype == null)

			doError(numOfElements, "Map: To-type not set (null)");

		int max = 0;

		if (numOfElements.getType() == ooaLexer.T_IDENTIFIER)

		{

			// see whether we can find the constant

			final Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.getText());

			if (aconst == null || aconst.kind() != IdentifierKind.Constant)

				doError(numOfElements, String.format("Constant %s not found", numOfElements.getText()));

			else if (aconst.type().kind() != TypeKind.IntType)

				doError(numOfElements, "Constant must be integer");

			else

				max = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

		}

		else

			try {

				max = Integer.parseInt(numOfElements.getText());

			} catch (final NumberFormatException e) {

				doError(numOfElements, "Not an integer");

			}

		final MapType result = new MapType(mapfromtype, maptotype, max, null);

		return result;

	}

	/* create a tuple type */

	 UlyssesType createTupleType(UlyssesType aType)

	{

		final TupleType result = new TupleType(null);

		addToTupleType(result, aType);

		return result;

	}

	/* add inner type to tuple */

	 void addToTupleType(UlyssesType aTypeSymbol, UlyssesType anotherType)

	{

		final TupleType tuple = (TupleType)aTypeSymbol;

		if (anotherType != null)

			tuple.AddType(anotherType);

		else

			doError("Unknown inner type in tuple");

	}

	/* create a QR type */

	UlyssesType createQrType(Token alandmark)

	{

		final QrType result = new QrType(null);

		addToQrType(result, alandmark);

		return result;

	}

	/* add another landmark to QR type */

	protected void addToQrType(UlyssesType aTypeSymbol, Token otherlandmark)

	{

		final Identifier sym = pState.Lookup(otherlandmark);

		if (sym != null)

		{

			doError(otherlandmark, String.format("Redifinition of %s", otherlandmark.getText()));

			return;

		}

		final LandmarkIdentifier lndmrk = new LandmarkIdentifier(otherlandmark, (QrType)aTypeSymbol, GetScope());

		((QrType)aTypeSymbol).AddLandmark(lndmrk);

	}

	/* gets called after a simple type has been constructed. used to define an internal name*/

	 void fixupSimpleType(UlyssesType aTypeSymbol)

	{

		if (aTypeSymbol != null)

			aTypeSymbol.SetupAnonymousName();

	}

	/* gets called after a simple or complex type has been constructed. used to define an internal name */

	 void fixupComplexType(UlyssesType aTypeSymbol)

	{

		if (aTypeSymbol != null)

			aTypeSymbol.SetupAnonymousName();

	}

	/* create a method symbol */

	 FunctionIdentifier createMethodSymbol(Token mname)

	{

		final Identifier sym = pState.Lookup(mname);

		if (sym != null)

		{

			doError(mname, String.format("Redefinition of %s", mname.getText()));

			return null;

		}

		final FunctionType funtype = new FunctionType(FunctionTypeEnum.Method, new LinkedList<UlyssesType>(), null);

		final MethodIdentifier msym = new MethodIdentifier(mname, funtype, GetScope());

		// funtype.SetTypeIdentifier(msym); -- the type of this function doesn't have a name!

		pState.currentScope.AddIdentifier(msym, null);

		pState.PushResolveStack(msym);

		return msym;

	}

	/* remove local method symbols from resolution stack again */

	protected void popResolveStack(FunctionIdentifier newMethod)

	{

		if (newMethod != null)

			pState.PopResolveStack();

	}

	/* add a return type to a method */

	 void setMethodReturnType(FunctionIdentifier newMethod, UlyssesType rt)

	{

		if (newMethod == null)

			return;

		if (rt == null)

			doError(String.format("Method %s has no return type (null)", newMethod.tokenText()));

		/* set return type */

		((FunctionType)newMethod.type()).SetReturnType(rt);

		/* add hidden return parameter */

		if (newMethod.symbolTable().Defined("result"))

		{

			doError(String.format("Method %s defines 'result'", newMethod.tokenText()));

			return;

		}

		final ParameterIdentifier returnval = new ParameterIdentifier("result", rt, GetScope());

		newMethod.symbolTable().AddIdentifier(returnval);

	}

	/* add a parameter to a method */

	 void addMethodParameter(FunctionIdentifier newMethod, Token paramName, UlyssesType atype)

	{

		if (newMethod == null)

			return;

		if (atype == null)

			doError(paramName, "Parameter has no type (null)");

		if (newMethod.symbolTable().Defined(paramName.getText()) == true)

		{

			doError(paramName, String.format("Parameter '%s' already defined", paramName.getText()));

			return;

		}

		// add parameter to scope

		final ParameterIdentifier param = new ParameterIdentifier(paramName, atype, GetScope());

		newMethod.AddParameter(param);

		// add type of param to signature

		final FunctionType ftype = (FunctionType)newMethod.type();

		ftype.AddParameterType(atype);

	}

	/* set method body of a method */

	 void addMethodBody(FunctionIdentifier newMethod, Block statements)

	{

		if (newMethod == null)

			return;

		if (statements == null)

			doError(String.format("%s has empty body (null)",

					((FunctionType)newMethod.type()).functionType() == FunctionTypeEnum.Method ? "Method" : "Action"));

		newMethod.SetBody(statements);

	}

	/* create a continuous action */

	 FunctionIdentifier createNamedContinuousAction(Token cactionname, FunctionTypeEnum actionTypeEnum)

	{

		return createNamedAction(cactionname, actionTypeEnum);

	}

	/* create a named action */

	 FunctionIdentifier createNamedAction(Token actionname, FunctionTypeEnum actionType)

	{

		final Identifier sym = pState.Lookup(actionname);

		if (sym != null)

		{

			doError(actionname, String.format("Symbol '%s' already defined.", sym.tokenText()));

			return null;

		}

		final FunctionType atype = new FunctionType(actionType, new LinkedList<UlyssesType>(), null);

		final NamedActionIdentifier action = new NamedActionIdentifier(actionname, atype, GetScope());

		// atype.SetTypeIdentifier(action); -- the type of this action doesn't have a name!

		pState.currentScope.AddIdentifier(action, null);

		pState.PushResolveStack(action);

		return action;

	}

	/* add body of action */

	 void addActionBody(FunctionIdentifier newAction, GuardedCommand body)

	{

		// we need a wrapper around the guarded command..

		final Block bdy = new SeqBlock(currentLine(), currentPos());

		addMethodBody(newAction, bdy);

		body.SetParentScope(bdy);

		bdy.AddStatement(body);

	}

	/* add constraints of cont. action */

	 void addContinuousActionBody(FunctionIdentifier newAction, GuardedCommand constraints)

	{

		final Block bdy = new SeqBlock(currentLine(), currentPos());

		bdy.AddStatement(constraints);

		addMethodBody(newAction, bdy);

	}

	/* create a guarded command */

	 GuardedCommand createGuardedCommandStatement()

	 {

		 return new GuardedCommand(null, null, currentLine(), currentPos());

	 }

	 void addExprAndBlockToGuardedCommand(GuardedCommand cmd, Expression expr, Block bdy)

	{

		if (bdy == null)

			doError("Guarded command without body (null)!");

		if (expr == null)

			doError("Guarded command without guard (null)!");

		cmd.SetGuard(expr);

		cmd.SetBody(bdy);

	}

	 GuardedCommand createGuardedCommandStatement(Expression expr, Block bdy, boolean isQualitative)

	{

		final GuardedCommand result = createGuardedCommandStatement();

		addExprAndBlockToGuardedCommand(result, expr, bdy);

		result.SetIsQualitative(isQualitative);

		return result;

	}

	/* add statements to list */

	 void addToStatementList(Block top, Statement stmt)

	{

		if (stmt == null)

			doError("Can not add statement: null!");

		top.AddStatement(stmt);

	}

	/* create a Kill statement */

	 Statement createKillStatement(Token aname)

	{

		final Identifier sym = pState.Lookup(aname);

		if (sym == null)

			doError(aname, "Not defined");

		final KillStatement result = new KillStatement(sym, aname.getLine(), aname.getCharPositionInLine());

		return result;

	}

	/* create a Skip statement */

	 Statement createSkipStatement()

	{

		return new SkipStatement(currentLine(), currentPos());

	}

	/* create a Break statement */

	 Statement createBreakStatement()

	{

		return new BreakStatement(currentLine(), currentPos());

	}

	/* create an Abort statement */

	 Statement createAbortStatement()

	{

		return new AbortStatement(currentLine(), currentPos());

	}

	/* creates a prioritized composition block */

	 Block createPrioBlock(Block top)

	{

		return new PrioBlock(top, currentLine(), currentPos());

	}

	/* creates a nondeterministically composed block */

	 Block createNondetBlock(Block top)

	{

		return new NondetBlock(top, currentLine(), currentPos());

	}

	/* creates a sequentially composed block */

	 SeqBlock createSeqBlock(Block top)

	{

		return new SeqBlock(top, currentLine(), currentPos());

	}

	/* adds a filter expression to seq block */

	protected void addSeqBlockExpression(Block seqList, Expression sexpr)

	{

		seqList.SetFilter(sexpr); /*gets transformed to guarded command in resolvevisitor!*/

	}

	/* create a self identifier */

	 IdentifierExpression createSelfIdentifierExpression(Token self)

	{

		final Identifier id = pState.Lookup("self");

		if (id == null)

		{

			doError(self, "Can not resolve 'self'");

			return null;

		}

		final IdentifierExpression result = new IdentifierExpression(id, self.getLine(), self.getCharPositionInLine());

		result.setIsSelf(true);

		return result;

	}

	/* build up identifier tree... */

	 Expression createIdentifierAccessExpression(IdentifierExpression aself, Token token)

	{

		final Identifier someid = pState.Lookup(token.getText(), GetScope());

		final Identifier self = pState.Lookup("self");

		if (someid != null)

		{

			switch (someid.kind())

			{

			/* all method and attribute accesses are prefixed by self */

			case AttributeIdentifier:

			case MethodIdentifier:

				if (self == null)

					doError(token, "Self access of method: Can not find 'self' symbol! (internal error)");

				aself = new IdentifierExpression(self, token.getLine(), token.getCharPositionInLine());

				aself.setIsSelf(true);

				break;

			default:

				break;

			}

		}

		final IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());

		if (aself != null)

			return new AccessExpression(aself, ident, token.getLine(), token.getCharPositionInLine());

		else

			return ident;

	}

	 AccessExpression addIdentifierAccessExpression(Expression parent, Token token)

	{

		final IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());

		return new AccessExpression(parent, ident, token.getLine(), token.getCharPositionInLine());

	}

	/* we have a primed id; prime the complete subtree.. */

	Expression setIdentifierExpressionPrimed(Expression oldExpr, Token token)

	{

		return new UnaryOperator(ExpressionKind.Primed, oldExpr, token.getLine(), token.getCharPositionInLine());

	}

	/* create a fold operation */

	 Expression createFoldExpression(Expression result, Token afold, Expression initval, Expression anexpr)

	{

		ExpressionKind akind = ExpressionKind.foldLR;

		if (afold.getType() == ooaLexer.T_FOLDLR)

			akind = ExpressionKind.foldLR;

		else if (afold.getType() == ooaLexer.T_FOLDRL)

			akind = ExpressionKind.foldRL;

		else

			assert(false);

		final TernaryOperator op = new TernaryOperator(akind, result, initval, anexpr, currentLine(), currentPos(), GetScope());

		return op;

	}

	/* create a method access */

	 CallExpression createMethodAccessExpression(Expression subexpr, List<Expression> m_params, Token token)

	{

		assert(subexpr != null);

		return new CallExpression(subexpr, m_params, token.getLine(), token.getCharPositionInLine(), GetScope());

	}

	/* create a tuple or map access */

	 TupleMapAccessExpression createTupleMapAccessExpression(Expression subexpr, Expression ac, Token token)

	{

		assert(subexpr != null);

		return new TupleMapAccessExpression(subexpr, ac, token.getLine(), token.getCharPositionInLine());

	}

	/* create a method call statement; has to be resolved in a second run */

	 Statement createCallStatement(Expression aqname)

	{

		return new Call(aqname, currentLine(), currentPos());

	}

	/* create a single assignment statement */

	 Statement createSingleAssignmentStatement(Expression aqname, Expression aexp)

	{

		final Assignment result = new Assignment(aqname, aexp, null, currentLine(), currentPos());

		return result;

	}

	/* create a multi-assignment statement; has to be resolved in a second run */

	 Statement createMultipleAssignmentStatementLHS(Expression aqname)

	{

		return new Assignment(aqname, null, null, currentLine(), currentPos());

	}

	/* adds an expression to the multi-assign */

	 void addMutlipleAssignmentStatementRHS(Statement result, Expression mexp)

	{

		((Assignment)result).AddValue(mexp);

	}

	/* adds a LHS-var to the multi assign */

	 void addMultipleAssignmentStatementLHS(Statement result, Expression malhs)

	{

		((Assignment)result).AddPlace(malhs);

	}

	/* pop an assignment statement from the resolve stack */

	 void popAssignmentOffResolveStack(Statement result)

	{

		assert(result == pState.currentScope); // ref eq.

		pState.PopResolveStack();

	}

	/* pushes the assignment statement onto resolve stack. */

	 void pushAssignmentOnResolveStack(Statement result)

	{

		assert(result instanceof Assignment);

		pState.PushResolveStack((Assignment)result);

	}

	/* adds a nondet-assignment constraint */

	 void addConstraintToAssignment(Statement result, Expression ndexp)

	{

		((Assignment)result).SetNondetExpression(ndexp);

	}

	/* add a named action call to do-od block */

	 void addNamedActionCallToBlockList(Block top, Token aname, List<Expression> m_params, Token maptoken, Expression amapexpression)

	{

		final Identifier id = pState.Lookup(aname);

		if (id == null)

		{

			doError(aname, String.format("Could not find named action '%s'", aname.getText()));

			return;

		}

		Expression callexpr;

		if (id.kind() == IdentifierKind.MethodIdentifier)

		{

			doError(aname, "Method access in do-od block not allowed.");

			return;

			// access via self

			/*

            Identifier self = pState.Lookup("self");

            if (self == null)

                doError(aname, "Self access of method: Can not find 'self' symbol! (internal error)");

            IdentifierExpression aself = new IdentifierExpression(self, aname.getLine(), aname.getCharPositionInLine());

            aself.setIsSelf(true);

            callexpr = new CallExpression(

                new AccessExpression(aself,

                    new IdentifierExpression(id, aname.getLine(), aname.getCharPositionInLine()), aname.getLine(), aname.getCharPositionInLine()),

                    m_params, aname.getLine(), aname.getCharPositionInLine(), GetScope());

			 */

		}

		else

			callexpr = new CallExpression(

					new IdentifierExpression(id, aname.getLine(), aname.getCharPositionInLine()),

					m_params, aname.getLine(), aname.getCharPositionInLine(), GetScope());

		if (amapexpression != null)

		{

			ExpressionKind akind = ExpressionKind.foldLR;

			if (maptoken.getType() == ooaLexer.T_FOLDLR)

				akind = ExpressionKind.foldLR;

			else if (maptoken.getType() == ooaLexer.T_FOLDRL)

				akind = ExpressionKind.foldRL;

			else

				assert(false);

			callexpr = new TernaryOperator(akind, callexpr, null, amapexpression,

					currentLine(), currentPos(), GetScope());

		}

		final Call statement = new Call(callexpr, currentLine(), currentPos());

		top.AddStatement(statement);

	}

	/*adds skip statement instead of call to do-od block*/

	 void addSkipStatementToBlockList(Block top)

	{

		top.AddStatement(new SkipStatement(currentLine(), currentPos()));

	}

	/* add anonymous action to do-od block */

	 void addToBlockList(Block top, Statement gcmd)

	{

		if (gcmd != null)

			top.AddStatement(gcmd);

	}

	/* add the do-od block to the action system type */

	 void addActionBlock(OoActionSystemType aTypeSymbol, Block bl)

	{

		aTypeSymbol.SetDoOdBlock(bl);

	}

	/* push block */

	 void pushBlockToResolveStack(IScope toPush)

	{

		pState.PushResolveStack(toPush);

	}

	/* pop block */

	 void popBlockFromResolveStack(IScope toPop)

	{

		if (toPop != null)

		{

			assert(pState.currentScope == toPop); // ref eq.

			pState.PopResolveStack();

		}

	}

	/* add block var */

	 void addBlockVariable(Block seqList, Token varname, UlyssesType aType)

	{

		if (aType == null)

		{

			doError(varname, String.format("%s lacks type!", varname.getText()));

		}

		try

		{

			seqList.AddIdentifier(new LocalVariableIdentifier(varname, aType, GetScope()));

		}

		catch (final ArgumentException e)

		{

			doError(varname, String.format("%s redefined!", varname.getText()));

		}

	}

	 QualitativeConstraintStatement createTwoVarConstraintStatement(Token id1, Token id2, QualitativeConstraintOperation op)

	{

		Identifier var1 = pState.Lookup(id1);

		if (var1 == null)

		{

			var1 = new ExpressionVariableIdentifier(id1.getText(), id1.getLine(), id1.getCharPositionInLine());

			var1.SetType(new AnyType((ExpressionVariableIdentifier)var1));

			GetScope().AddIdentifier(var1, null);

			doWarning(id1, String.format("Free variable in qualitative constraint: '%s'.", id1.getText()));

		}

		Identifier var2 = pState.Lookup(id2);

		if (var2 == null)

		{

			var2 = new ExpressionVariableIdentifier(id2.getText(), id2.getLine(), id2.getCharPositionInLine());

			var2.SetType(new AnyType((ExpressionVariableIdentifier)var2));

			GetScope().AddIdentifier(var2, null);

			doWarning(id1, String.format("Free variable in qualitative constraint: '%s'.", id2.getText()));

		}

		final QualitativeConstraintStatement result = new QualitativeConstraintStatement(var1, var2, op, id1.getLine(), id1.getCharPositionInLine());

		return result;

	}

	 QualitativeConstraintStatement createQualEqualConstraintStatement(Token id1, Token id2)

	{

		return createTwoVarConstraintStatement(id1, id2, QualitativeConstraintOperation.Equal);

	}

	 QualitativeConstraintStatement createQualArithConstraintStatement(Token id1, Token id2, Token id3, Token op)

	{

		Identifier var1 = pState.Lookup(id1);

		if (var1 == null)

		{

			var1 = new ExpressionVariableIdentifier(id1.getText(), id1.getLine(), id1.getCharPositionInLine());

			var1.SetType(new AnyType((ExpressionVariableIdentifier)var1));

			GetScope().AddIdentifier(var1, null);

			doWarning(id1, String.format("Free variable in qualitative constraint: '%s'.", id1.getText()));

		}

		Identifier var2 = pState.Lookup(id2);

		if (var2 == null)

		{

			var2 = new ExpressionVariableIdentifier(id2.getText(), id2.getLine(), id2.getCharPositionInLine());

			var2.SetType(new AnyType((ExpressionVariableIdentifier)var2));

			GetScope().AddIdentifier(var2, null);

			doWarning(id1, String.format("Free variable in qualitative constraint: '%s'.", id2.getText()));

		}

		Identifier var3 = pState.Lookup(id3);

		if (var3 == null)

		{

			var3 = new ExpressionVariableIdentifier(id3.getText(), id3.getLine(), id3.getCharPositionInLine());

			var3.SetType(new AnyType((ExpressionVariableIdentifier)var3));

			GetScope().AddIdentifier(var3, null);

			doWarning(id1, String.format("Free variable in qualitative constraint: '%s'.", id3.getText()));

		}

		QualitativeConstraintOperation operation;

		switch (op.getType())

		{

		case ooaParser.T_SUM:

			operation = QualitativeConstraintOperation.Sum;

			break;

		case ooaParser.T_DIFF:

			operation = QualitativeConstraintOperation.Diff;

			break;

		case ooaParser.T_PROD:

			operation = QualitativeConstraintOperation.Prod;

			break;

		default:

			doError(op, String.format("'%s' unknown operation", op.getText()));

			return null;

		}

		final QualitativeConstraintStatement result = new QualitativeConstraintStatement(var1, var2, var3, operation, id1.getLine(), id1.getCharPositionInLine());

		return result;

	}

	 QualitativeConstraintStatement createQualDerivConstraintStatement(Token id1, Token derivid)

	{

		return createTwoVarConstraintStatement(id1, derivid, QualitativeConstraintOperation.Deriv);

	}

	/* creates a general binary operator without any children */

	 BinaryOperator createBinaryOperator(ExpressionKind akind)

	{

		final Token token = input.LT(-1);

		return new BinaryOperator(akind, null, null, token.getLine(), token.getCharPositionInLine());

	}

	/* creates a general unary operator without child */

	 UnaryOperator createUnaryOperator(ExpressionKind unaryOperatorType)

	{

		final Token token = input.LT(-1);

		return new UnaryOperator(unaryOperatorType, null, token.getLine(), token.getCharPositionInLine());

	}

	/* create a conditional expression */

	 Expression createConditionalExpression(Expression ce, Expression te, Expression ee, Token ef)

	{

		return new TernaryOperator(ExpressionKind.conditional, ce, te, ee, ef.getLine(), ef.getCharPositionInLine(), GetScope());

	}

	/* create a quantifier expression */

	 Quantifier createQuantifierExpression(Token t)

	{

		Quantifier result = null;

		if (t.getType() == ooaLexer.T_FORALL)

			result = new ForallQuantifier(null, t.getLine(), t.getCharPositionInLine());

		else

			result = new ExistsQuantifier(null, t.getLine(), t.getCharPositionInLine());

		pState.PushResolveStack(result);

		return result;

	}

	/* add a bound variable to the quantifier */

	 void addBoundVarToQuantifierExpression(Quantifier result, Token id, UlyssesType id_type)

	{

		/*note: this might be a bit harsh, but for now it's easier to demand uniquely named vars,

                without any hiding. Could be fixed in searching only the first resolve level for

                dupes..

		 */

		final Identifier sym = pState.Lookup(id);

		if (sym != null)

			doError(id, String.format("'%s' already defined!", id.getText()));

		else

		{

			if (id_type == null)

				doError(id, String.format("%s lacks type (null).", id.getText()));

			final Identifier newvar = new ExpressionVariableIdentifier(id, id_type, GetScope());

			result.AddIdentifier(newvar, null);

		}

	}

	/* add the expression to the quantifier */

	 void addExpressionToQuantifier(Quantifier result, Expression e)

	{

		result.SetChild(e);

	}

	/* remove local variables from resolve stack */

	 void removeBoundVarsFromResolveStack(Quantifier result)

	{

		if (result != null)

			pState.PopResolveStack();

	}

	/* create a boolean constant */

	 LeafExpression createBoolConstant(boolean p)

	{

		final Token token = input.LT(-1);

		return new ValueExpression<Boolean>(p, token.getLine(), token.getCharPositionInLine(), Boolean.class);

	}

	/* create a nil */

	 LeafExpression createNullPointerConstant()

	{

		final Token token = input.LT(-1);

		return new ValueExpression<Object>(null, token.getLine(), token.getCharPositionInLine(), Object.class);

	}

	/* create a 'self' identifier */

	 LeafExpression createSelfPointer()

	{

		final Token token = input.LT(-1);

		final Identifier self = pState.Lookup("self");

		if (self == null)

		{

			doError(token, "Could not resolve 'self'");

			return new UnresolvedIdentifierExpression(token, GetScope());

		}

		final IdentifierExpression result = new IdentifierExpression(self, token.getLine(), token.getCharPositionInLine());

		result.setIsSelf(true);

		return result;

	}

	/* create a float const */

	 LeafExpression createFloatConstant(Token t_fl)

	{

		return new ValueExpression<Double>(Double.parseDouble(t_fl.getText()), t_fl.getLine(), t_fl.getCharPositionInLine(), Double.class);

	}

	/* create int const */

	 LeafExpression createIntConstant(Token t_in)

	{

		return new ValueExpression<Integer>(Integer.parseInt(t_in.getText()), t_in.getLine(), t_in.getCharPositionInLine(), Integer.class);

	}

	/* set children of binary operator*/

	 Expression addBinaryExpression(BinaryOperator binexpr, Expression expr, Expression e2)

	{

		binexpr.SetLeftChild(expr);

		binexpr.SetRightChild(e2);

		return binexpr;

	}

	/* set child of unary expr */

	 Expression addUnaryExpression(UnaryOperator unexpr, Expression e)

	{

		if (unexpr != null)

		{

			unexpr.SetChild(e);

			return unexpr;

		}

		else

			return e;

	}

	/* create a list */

	 ListConstructor createInitializedList()

	{