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.visitors;

import java.util.ArrayList;

import java.util.Iterator;

import java.util.LinkedList;

import java.util.Stack;

/// <summary>

/// Requires: ReplaceOpaqueVisitor

///

/// After we have an AST without any Opaquetypes, we still need to replace all the

/// UnresolvedIdentifierExpressions. We also need to compute the expression types,

/// which is also necessary to resolve all the identifiers. So, this visitor

/// goes over all expressions and

///   - resolves all identifiers

///   - calculates resulting types (incl. coercion)

/// </summary>

public final class OoaResolveExpressionsVisitor extends OoaCompleteAstTraversalVisitor

{

	// we allow for free variable in expressions. collect them here.

	private final Stack<SymbolTable> m_freeVariables = new Stack<SymbolTable>();

	private Expression m_entryExpression = null;

	// helpers that replace the old expression in the AST by the new one.

	private void ReplaceExpression(IAst parent, Expression subElement, Expression newExpression)

	{

		switch (parent.nodeType())

		{

			case identifier:

				ReplaceExpressionInIdentifier((Identifier)parent, subElement, newExpression);

				break;

			case statement:

				ReplaceExpressionInStatement((Statement)parent, subElement, newExpression);

				break;

			default:

				throw new NotImplementedException();

		}

	}

	private void ReplaceExpressionInIdentifier(Identifier identifier, Expression subElement, Expression newExpression)

	{

		switch (identifier.kind())

		{

			case AttributeIdentifier:

				final AttributeIdentifier ident = (AttributeIdentifier)identifier;

				assert(ident.initializer() == subElement); // ref equ.

				ident.SetInitializer(newExpression);

				break;

			case Constant:

				final ConstantIdentifier aconst = (ConstantIdentifier)identifier;

				assert(aconst.Value() == subElement); // ref equ

				aconst.SetValue(newExpression);

				if (newExpression.kind() != ExpressionKind.Value)

					Error(aconst.Value(), String.format("%s not a constant!", aconst.tokenText()));

				break;

			default:

				throw new NotImplementedException();

		}

	}

	private void ReplaceExpressionInStatement(Statement statement, Expression subElement, Expression newExpression)

	{

		switch (statement.kind())

		{

			case GuardedCommand:

				final GuardedCommand gc = (GuardedCommand)statement;

				assert(gc.guard() == subElement); // ref eq

				gc.SetGuard(newExpression);

			break;

			case SeqBlock:

				final SeqBlock sqblock = (SeqBlock)statement;

				assert(sqblock.filter() == subElement); // ref eq

				sqblock.SetFilter(null);

				// we convert the filter to a guarded command...

				final SeqBlock implseq = new SeqBlock(sqblock.line(), sqblock.pos());

				implseq.SetStatements(sqblock.statements());

				final GuardedCommand implguard = new GuardedCommand(newExpression, implseq, sqblock.line(), sqblock.pos());

				sqblock.SetStatements(new LinkedList<Statement>());

				sqblock.AddStatement(implguard);

				break;

			case Assignment:

				final Assignment zw = (Assignment)statement;

				boolean found = false;

				if (zw.nondetExpression() == subElement) // ref eq

				{

					zw.SetNondetExpression(newExpression);

					found = true;

				}

				else

				{

					int cntr = 0;

					while (cntr < zw.places().size()) {

						if (zw.places().get(cntr) == subElement) { // ref eq

							zw.places().set(cntr, newExpression);

							found = true;

							break;

						}

						cntr ++;

					}

					if (!found) {

						cntr = 0;

						while (cntr < zw.values().size()) {

							if (zw.values().get(cntr) == subElement) { // ref eq.

								zw.values().set(cntr, newExpression);

								found = true;

								break;

							}

							cntr ++;

						}

					}

				}

				assert(found);

				break;

			case MethodCall:

				final Call call = (Call)statement;

				assert(call.callExpression() == subElement); // ref eq.

				call.SetCallExpression(newExpression);

				break;

			default:

				throw new NotImplementedException();

		}

	}

	// helper that returns null and adds an error message in the parserstate errorlist.

	private Expression Error(Expression expression, String p)

	{

		final ParserError error = new ParserError(m_ParserState.filename,

				expression.line(), expression.pos(), p);

		m_ParserState.AddErrorMessage(error);

		return null;

	}

	private void Info(Expression expression, String p)

	{

		final ParserMessage msg = new ParserMessage(m_ParserState.filename,

				expression.line(), expression.pos(), p);

		m_ParserState.AddMessage(msg);

	}

	// helper that adds a warning message to the output

	private void Warning(Identifier expression, String p)

	{

		final ParserWarning warning = new ParserWarning(m_ParserState.filename,

				expression.line(), expression.column(), p);

		m_ParserState.AddWarningMessage(warning);

	}

	private void Warning(Expression expression, String p)

	{

		final ParserWarning warning = new ParserWarning(m_ParserState.filename,

				expression.line(), expression.pos(), p);

		m_ParserState.AddWarningMessage(warning);

	}

	private final ArrayList<TupleConstructor> m_matcherList = new ArrayList<TupleConstructor>();

	///

	///   Resolve Expressions

	///

	private Expression ResolveExpression(TernaryOperator expression)

	{

		if (expression.kind() == ExpressionKind.conditional)

		{

			final Expression left = ResolveExpression(expression.left());

			Expression mid = ResolveExpression(expression.mid());

			Expression right = ResolveExpression(expression.right());

			if (left == null || mid == null || right == null)

				return null;

			if (left.type() == null || left.type().kind() != TypeKind.BoolType)

				return Error(expression, "Conditional: Condition not a bool");

			if (mid.type() == null || right.type() == null)

				return Error(expression, "Conditional: Then or Else branch has void-type");

			final UlyssesType acover = UlyssesType.CoverType(mid.type(), right.type());

			if (acover == null)

				return Error(expression, String.format(

					"Conditional: Then and Else branch must be of same type. (%s <> %s)",

					mid.type().toString(), right.type().toString()));

			if (!UlyssesType.TypeEqual(acover, mid.type()))

			{

				mid = new UnaryOperator(ExpressionKind.Cast, mid, mid.line(), mid.pos());

				mid.SetType(acover);

			}

			if (!UlyssesType.TypeEqual(acover, right.type()))

			{

				right = new UnaryOperator(ExpressionKind.Cast, right, right.line(), right.pos());

				right.SetType(acover);

			}

			expression.SetLeftChild(left);

			expression.SetMidChild(mid);

			expression.SetRightChild(right);

			expression.SetType(mid.type());

			return expression;

		}

		else if (expression.kind() == ExpressionKind.foldLR || expression.kind() == ExpressionKind.foldRL)

		{

			CallExpression leftcall = expression.left().kind() != ExpressionKind.Call

				? new CallExpression(expression.left(), new ArrayList<Expression>(), expression.line(),

					expression.pos(), expression.definingScope())

				: (CallExpression)expression.left();

			leftcall = (CallExpression)ResolveExpression(leftcall, true);

			if (leftcall == null)

				return null;

			final Expression afun = ResolveExpression(leftcall.child());

			leftcall.SetChild(afun);

			if (afun == null || afun.type() == null || afun.type().kind() != TypeKind.FunctionType)

				return Error(expression, "Fold/Map operation needs a method or named action as LHS");

			final FunctionType funType = (FunctionType)afun.type();

			if (funType.returnType() == null && expression.mid() != null)

				return Error(expression, "Fold operation needs a method with matching return type");

			if (funType.returnType() != null && expression.mid() == null)

				Warning(expression, "Map operation will discard result of function");

			final boolean isMap = expression.mid() == null;

			Expression mid = expression.mid();

			if (!isMap)

			{

				mid = ResolveExpression(mid);

				if ((funType.parameter().size() - leftcall.arguments().size()) != 2)

					return Error(expression, "Function used in fold operation needs 2 not-instantiated parameters");

			} else if ((funType.parameter().size() - leftcall.arguments().size()) != 1)

				return Error(expression, "Function used in map operation needs one not-instantiated parameter");

			final Expression right = ResolveExpression(expression.right());

			if (right == null || right.type() == null || right.type().kind() != TypeKind.ListType)

				return Error(expression, "Fold/Map operation needs list as RHS");

			if (!isMap)

			{

				final int nextToLast = funType.parameter().size() - 2;

				final UlyssesType initCover = UlyssesType.CoverType(funType.parameter().get(nextToLast), mid.type());

				if (initCover == null)

					return Error(expression, "Next to last parameter does not match initializer type in map operation.");

				if (!UlyssesType.TypeEqual(mid.type(), initCover))

					mid = new UnaryOperator(ExpressionKind.Cast, mid, mid.line(), mid.pos());

				mid.SetType(initCover);

				//List<Expression> args = new List<Expression> ();

				leftcall.arguments().add(new IdentifierExpression(new ParameterIdentifier("_result", initCover, null), 0, 0));

				leftcall.arguments().add(new IdentifierExpression(new ParameterIdentifier("_elem", funType.parameter().peekLast(), null), 0, 0));

				//leftcall.SetArguments(args);

			}

			// UlyssesType listCover = UlyssesType.CoverType(funType.parameter.Last.Value, ((ListType)right.type).innerType);

			// if (listCover == null)

			if (!UlyssesType.TypeEqual(funType.parameter().peekLast(), ((ListType)right.type()).innerType()))

				return Error(expression, "Last paramter does not match inner-type of list in fold/map operation");

			expression.SetLeftChild(leftcall);

			expression.SetMidChild(mid);

			expression.SetRightChild(right);

			if (!isMap)

				expression.SetType(funType.returnType());

			else

				expression.SetType(new NullType());

			return expression;

		} else

			throw new ArgumentException();

	}

	private Expression ResolveExpression(ForallQuantifier expression)

	{

		final Expression child = ResolveExpression(expression.child());

		if (child == null)

			return null;

		expression.SetType(new BoolType(null));

		expression.SetChild(child);

		return expression;

	}

	private Expression ResolveExpression(ExistsQuantifier expression)

	{

		final Expression child = ResolveExpression(expression.child());

		if (child == null)

			return null;

		expression.SetType(new BoolType(null));

		expression.SetChild(child);

		return expression;

	}

	private Expression ResolveExpression(ListConstructor expression)

	{

		UlyssesType type = null;

		ListType restype = null;

		Expression comprehension = null;

		if (expression.comprehension() != null)

		{

			comprehension = ResolveExpressionNewScope(expression.comprehension());

			if (comprehension == null)

				return null;

			if (comprehension.type() == null)

				return Error(expression, "List comprehension has void expression");

			if (comprehension.type().kind() != TypeKind.BoolType)

				return Error(expression, "List comprehension has to be bool-expression");

			expression.SetComprehension(comprehension);

			if (expression.elements().size() != 1)

				return Error(expression, "List comprehension expects one initializer expression");

		}

		final ArrayList<Expression> newitems = new ArrayList<Expression>();

		if (expression.elements().size() == 0 || expression.elements().get(0) == null || (

		        expression.elements().get(0).kind() == ExpressionKind.Value &&

		        expression.elements().get(0) instanceof ValueExpression<?> &&

		        ((ValueExpression<?>)expression.elements().get(0)).value() == null))

		{

			// empty list

			type = new NullType();

		}

		else

		{

			final ArrayList<Expression> tmpitems = new ArrayList<Expression>();

			for (final Expression item: expression.elements())

			{

				final Expression element = ResolveExpression(item);

				if (element == null)

					return null;

				if (element.type() == null)

					return Error(expression, "Void expression in list initializer");

				if (element.kind() == ExpressionKind.Value &&

				    element instanceof ValueExpression<?> &&

				    ((ValueExpression<?>)element).value() == null)

				{

					return Error(expression, "Not-In-List (nil) values not allowed in a list");

				}

				// calculate the type we're constructing

				if (type == null)

					type = element.type();

				type = UlyssesType.CoverType(type, element.type());

				if (type == null)

					return Error(expression, "List constructor needs matching types");

				tmpitems.add(element);

			}

			// now we have the resulting type - we still need to insert casts that might be necessary

			for (final Expression item: tmpitems)

			{

				if (!UlyssesType.TypeEqual(item.type(), type))

				{

					final Expression cast = new UnaryOperator(ExpressionKind.Cast, item, item.line(), item.pos());

					cast.SetType(type);

					newitems.add(cast);

				}

				else

					newitems.add(item);

			}

		}

		expression.SetElements(newitems);

		if (comprehension == null)

			restype = new ListType(type, newitems.size(), null);

		else

			restype = new ListType(type, -1, null); // we do not know anything about the bound

		expression.SetType(restype);

		return expression;

	}

	private Expression ResolveExpression(SetConstructor expression)

	{

		UlyssesType type = null;

		ListType restype = null;

		Expression comprehension = null;

		if (expression.comprehension() != null)

		{

			comprehension = ResolveExpressionNewScope(expression.comprehension());

			if (comprehension == null)

				return null;

			if (comprehension.type() == null)

				return Error(expression, "Set comprehension has void expression");

			if (comprehension.type().kind() != TypeKind.BoolType)

				return Error(expression, "Set comprehension has to be bool-expression");

			expression.SetComprehension(comprehension);

			if (expression.items().size() != 1)

				return Error(expression, "Set comprehension expects one initializer expression");

		}

		final ArrayList<Expression> newitems = new ArrayList<Expression>();

		for (final Expression item: expression.items())

		{

			final Expression element = ResolveExpression(item);

			if (element == null)

				return null;

			if (element.type() == null)

				return Error(expression, "Void expression in set initializer");

			if (type == null)

				type = element.type();

			type = UlyssesType.CoverType(type, element.type());

			if (type == null)

				return Error(expression, "Set initializer needs matching types");

			newitems.add(element);

		}

		expression.SetItems(newitems);

		restype = new ListType(type, newitems.size(), null);

		expression.SetType(restype);

		return expression;

	}

	private Expression ResolveExpression(MapConstructor expression)

	{

		UlyssesType domain = null;

		UlyssesType range = null;

		final ArrayList<MapConstructor.MapItem> newitems = new ArrayList<MapConstructor.MapItem>();

		for(final MapItem item: expression.items())

		{

			final Expression domexpr = ResolveExpression(item.key);

			if (domexpr == null)

				return null;

			if (domexpr.type() == null)

				return Error(expression, "Domain initializing expression void");

			if (domain == null)

				domain = domexpr.type();

			final Expression rangeexpr = ResolveExpression(item.value);

			if (rangeexpr == null)

				return null;

			if (rangeexpr.type() == null)

				return Error(expression, "Range initializing expression void");

			if (range == null)

				range = rangeexpr.type();

			domain = UlyssesType.CoverType(domain, domexpr.type());

			range = UlyssesType.CoverType(range, rangeexpr.type());

			if (domain == null)

				return Error(expression, "Types of domain expressions do not match");

			if (range == null)

				return Error(expression, "Types of range expressions do not match");

			newitems.add(new MapConstructor.MapItem(domexpr, rangeexpr));

		}

		expression.SetItems(newitems);

		final MapType resulttype = new MapType(domain, range, newitems.size(), null);

		expression.SetType(resulttype);

		return expression;

	}

	private Expression ResolveExpression(TupleConstructor expression)

	{

		final TupleType typeToConstruct = (TupleType)expression.tupleType().type();

		if (expression.values().size() != typeToConstruct.innerTypes().size())

			return Error(expression, String.format("Tuple constructor has wrong arity. (%s <> %s)",

				typeToConstruct.innerTypes().size(), expression.values().size()));

		//TupleType resulttype = new TupleType(null);

		final ArrayList<Expression> newvalexprs = new ArrayList<Expression>();

		final Iterator<UlyssesType> innerTargetType = typeToConstruct.innerTypes().iterator();

		int freeVarCount = 0;

		for (final Expression initexpr: expression.values())

		{

			final UlyssesType innerTargetTypeValue = innerTargetType.next();

			Expression newval = ResolveExpression(initexpr);

			if (newval == null)

				return null;

			if (newval.type() == null)

				return Error(expression, "Element has void type");

			if (newval.type().kind() == TypeKind.Any)

			{

				// free var - so set type.

				final AnyType freevar = (AnyType)newval.type();

				freevar.VariableIdentifier().SetType(innerTargetTypeValue);

				freevar.VariableIdentifier().SetInitialized(true);

				freeVarCount++;

			}

			else

			{

				final UlyssesType acover = UlyssesType.CoverType(innerTargetTypeValue, newval.type());

				if (acover == null || !UlyssesType.TypeEqualByKind(innerTargetTypeValue, acover))

					return Error(expression,

						String.format("Element in tuple constructor has non-matching type (%s <> %s)",

								innerTargetTypeValue.toString(), newval.type().toString()));

				if (!UlyssesType.TypeEqual(acover, newval.type()))

				{

					newval = new UnaryOperator(ExpressionKind.Cast, newval, newval.line(), newval.pos());

					newval.SetType(acover);

				}

				if (UlyssesType.FirstTypeLessRange(innerTargetTypeValue, acover)) {

					Warning(expression,

						String.format("Tuple constructor may over/underflow: %s := %s",

								innerTargetTypeValue.toString(), acover.toString()));

					newval = new UnaryOperator(ExpressionKind.Cast, newval, newval.line(), newval.pos());

					newval.SetType(innerTargetTypeValue);

				}

			}

			newvalexprs.add(newval);

			//resulttype.AddType(newval.type);

		}

		if (freeVarCount > 0)

		{

			if (freeVarCount != expression.values().size())

				return Error(expression, String.format("Tuple constructor must have 0 or #elems (%s) free variables", expression.values().size()));

			else

			{

				expression.SetIsMatcher(true); // mark this tuple constructor as matcher, since this is the only thing it does..

				m_matcherList.add(expression); // matcher has to be bound by one equality

			}

		}

		expression.SetTupleValues(newvalexprs);

		//expression.SetType(resulttype);

		expression.SetType(typeToConstruct); // the constructor always will create the correct type!

		return expression;

	}

	private Expression ResolveExpression(QValConstructor expression)

	{

		Expression basevalue = null;

		Expression rangevalue = null;

		basevalue = ResolveExpression(expression.value()[0]);

		if (basevalue == null || basevalue.kind() != ExpressionKind.Access

		    || basevalue.type() == null || basevalue.type().kind() != TypeKind.QrType)

			return Error(expression, "Landmark expected.");

		expression.SetType(basevalue.type());

		expression.SetValue(basevalue);

		if (expression.value().length == 2)

		{

			rangevalue = ResolveExpression(expression.value()[1]);

			if (rangevalue == null || rangevalue.kind() != ExpressionKind.Access

			    || rangevalue.type() == null || rangevalue.type().kind() != TypeKind.QrType)

				return Error(expression, "Landmark expected.");

			if (!UlyssesType.TypeEqual(basevalue.type(), rangevalue.type()))

				return Error(expression, String.format("Quantity spaces do not match: %s <> %s",

						basevalue.type().toString(),

						rangevalue.type().toString()));

			expression.AddRange(rangevalue);

		}

		return expression;

	}

	private Expression ResolveExpression(IdentifierExpression expression)

	{

		// nothing to do here, since we do not have any consts that may be

		// folded

		if ((expression.identifier().kind() == IdentifierKind.MethodIdentifier

		       || expression.identifier().kind() == IdentifierKind.NamedActionIdentifier)

		    && !m_entryExpression.callTargets().contains(expression.identifier()))

		{

			m_entryExpression.callTargets().add((FunctionIdentifier)expression.identifier());

		}

		return expression;

	}

	private Expression ResolveExpression(UnresolvedIdentifierExpression expression)

	{

		Identifier anid;

		//Identifier self = m_ParserState.Lookup("self");

		if (m_freeVariables.peek().Defined(expression.tokenText()))

			anid = m_freeVariables.peek().Get(expression.tokenText());

		else

			anid = m_ParserState.Lookup(expression.tokenText(), expression.scope());

		if (anid != null)

		{

			switch (anid.kind())

			{

			case TypeIdentifier:

				// only return a TypeExpression if this TypeIdentifier didn't come from a "self"

				if (anid instanceof SelfTypeIdentifier) {

					final IdentifierExpression result = new IdentifierExpression(anid, expression.line(), expression.pos());

					result.setIsSelf(true);

					return result;

				} else

					return new TypeExpression(anid.type(), expression.line(), expression.pos());

			case MethodIdentifier:

				m_entryExpression.callTargets().add((FunctionIdentifier)anid);

				final SelfTypeIdentifier selfid = (SelfTypeIdentifier)m_ParserState.Lookup("self", expression.scope());

				if ((selfid != null) && ((OoActionSystemType)(selfid).type()).symbols().Defined(anid))

				{

					// if it's a self access, add a self identifier (needed by cadp backend, e.g.)

					// self.<method> is handled in a separate method and does not call us here!! (hence this code is working)

					final IdentifierExpression aself = new IdentifierExpression(selfid, expression.line(), expression.pos());

					aself.setIsSelf(true);

					final AccessExpression localaccess = new AccessExpression(aself, new IdentifierExpression(anid, expression.line(), expression.pos()),

							expression.line(), expression.pos());

					ResolveExpression(localaccess);

					return localaccess;

				}

				else

				{

					return new IdentifierExpression(anid, expression.line(), expression.pos());

				}

			case NamedActionIdentifier:

				m_entryExpression.callTargets().add((FunctionIdentifier)anid);

				return new IdentifierExpression(anid, expression.line(), expression.pos());

			case Constant:

				if (((ConstantIdentifier)anid).Value() != null)

					return ((ConstantIdentifier)anid).Value().Clone();

				else

					return null;

			default:

				return new IdentifierExpression(anid, expression.line(), expression.pos());

			}

		}

		else

		{

			final ExpressionVariableIdentifier freeVar =

					new ExpressionVariableIdentifier(expression.tokenText(), expression.line(), expression.pos());

			freeVar.SetType(new AnyType(freeVar));

			m_freeVariables.peek().AddIdentifier(freeVar);

			// add a warning about free variables - do not change text without changing the text in ooaTypeCheckVisitor..

			Warning(freeVar, String.format("Free variable in expression: '%s'.", freeVar.tokenText()));

			return new IdentifierExpression(freeVar, expression.line(), expression.pos());

		}

	}

	private Expression ResolveExpression(TupleMapAccessExpression expression)

	{

		final Expression child = ResolveExpression(expression.child());

		if (child == null)

			return null;

		final Expression arg = ResolveExpression(expression.argument());

		if (arg == null)

			return null;

		assert(child.type() != null);

		if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.TupleType))

		{

			if ((arg.kind() != ExpressionKind.Value)

			    || (((LeafExpression)arg).valueType() != LeafTypeEnum.integer))

			{

				return Error(expression, "Argument to tuple access must be constant integer value!");

			}

			final TupleType aTuple = (TupleType)child.type();

			@SuppressWarnings("unchecked")

			final

			ValueExpression<Integer> aval = (ValueExpression<Integer>)arg;

			if ((aval.value() < 0) || (aval.value() >= aTuple.innerTypes().size()))

			{

				return Error(expression, "Argument to tuple access has to be in range 0..#elems-1");

			}

//			LinkedListNode<UlyssesType> anode = aTuple.innerTypes().First;

//			int target = aval.value();

//			while (target > 0)

//			{

//				target--;

//				anode = anode.Next;

//			}

//			expression.SetType(anode.Value);

			expression.SetType(aTuple.innerTypes().get(aval.value()));

		}

		else if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.MapType))

		{

			final MapType amap = (MapType)child.type();

			expression.SetType(amap.toType());

		}

		else if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.ListType))

		{

			// we allow element access of lists via list[i]

			final ListType alist = (ListType)child.type();

			expression.SetType(alist.innerType());

		}

		else

		{

			return Error(expression, "Not a list, tuple, or map instance");

		}

		expression.SetArgument(arg);

		expression.SetChild(child);

		return expression;

	}

	private Expression ResolveExpression(CallExpression expression)

	{

		return ResolveExpression(expression, false);

	}

	private Expression ResolveExpression(CallExpression expression, boolean allowFewerParameters)

	{

		// calc type of child

		final Expression child = ResolveExpression(expression.child());

		if (child == null)

			return null;

		assert(child.type() != null);

		expression.SetChild(child);

		if (child.type().kind() != TypeKind.FunctionType)

		{

			return Error(expression, "No function to call!");

		}

		final FunctionType funtype = (FunctionType)child.type();

//		// check whether call of named action is allowed

//		if (funtype.functionType() != FunctionTypeEnum.Method)

//		{

//			// see if call is allowed: must not be called from within a named action

//			IScope callingScope = expression.scope();

//			while (callingScope != null)

//			{

//				if (callingScope instanceof NamedActionIdentifier || callingScope instanceof MethodIdentifier)

//					return Error(expression, "Call of named Action only allowed in do-od block!");

//				callingScope = callingScope.GetParentScope();

//			}

//		}

		// check arguments

		final int argsSpec = funtype.parameter().size();

		final int argsHave = expression.arguments().size();

		if (argsHave < argsSpec && !allowFewerParameters)

		{

			return Error(expression, "Too few parameters in function call");

		}

		if (argsHave > argsSpec)

		{

			return Error(expression, "Too much parameters in function call");

		}

		final ArrayList<Expression> newargs = new ArrayList<Expression>();

		final Iterator<UlyssesType> demandedArgType = funtype.parameter().iterator();

		for (final Expression arg: expression.arguments())

		{

			final UlyssesType demandedArgTypeValue = demandedArgType.next();

			Expression newarg = ResolveExpression(arg);

			if (newarg == null)

				return null;

			if (newarg.GetUninitializedFreeVariables().size() > 0)

				Error(arg, String.format("Undefined variable '%s'",

					newarg.GetUninitializedFreeVariables().get(0).tokenText()));

			final Expression constantvalue = newarg.kind() == ExpressionKind.Value ? newarg : null;

			final UlyssesType acover = UlyssesType.CoverType(newarg.type(), demandedArgTypeValue);

			if (acover == null || !UlyssesType.TypeEqualByKind(demandedArgTypeValue, acover))

				return Error(arg, String.format("Argument type does not match; expected: %s delivered: %s",

						demandedArgTypeValue.toString(), newarg.type().toString()));

			newarg = UnaryOperator.TryCoerceUp(newarg, acover);

			if (UlyssesType.FirstTypeLessRange(demandedArgTypeValue, acover))

			{

				if (constantvalue == null)

				{

					Warning(arg, String.format("Call parameter may over/underflow: %s := %s",

							demandedArgTypeValue.toString(), acover.toString()));

					final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, newarg, newarg.line(), newarg.pos());

					cast.SetType(demandedArgTypeValue);

					newarg = cast;

				}

				else

				{

					Error(arg, String.format("Call parameter out of range (%s  := %s)",

							demandedArgTypeValue.toString(), constantvalue.toString()));

				}

			}

			newargs.add(newarg);

		}

		expression.SetArguments(newargs);

		if (funtype.returnType() != null)

			expression.SetType(funtype.returnType());

		return expression;

	}

	private Expression ResolveExpression(AccessExpression expression)

	{

		Expression lhs = ResolveExpression(expression.left());

		if (lhs == null)

			return null;

		if (!(expression.right() instanceof UnresolvedIdentifierExpression))

		{

			expression.SetRightChild(ResolveExpression(expression.right()));

			expression.SetType(expression.right().type());

			return expression;

		}

		final boolean selfAccess = (lhs.kind() == ExpressionKind.Identifier) && ((IdentifierExpression)lhs).isSelf();

		final boolean staticAccess = lhs.kind() == ExpressionKind.Type;

		final UnresolvedIdentifierExpression access = (UnresolvedIdentifierExpression)expression.right();

		// atype could be null...

		UlyssesType atype = lhs.type();

		if ((lhs.kind() == ExpressionKind.Call) && (atype == null))

		{

			return Error(access, "Can not access return type of void-function");

		}

		else if (atype == null)

		{

			return Error(access, "Can not access member of a void type");

		}

		// if we did not apply a call expression to a function

		if (atype.kind() == TypeKind.FunctionType)

		{

			// we can access the return val...

			final FunctionType fun = (FunctionType)atype;

			// check arity

			if (fun.parameter().size() > 0)

				return Error(access, "Implicit function call not possible: Too few parameters.");

			// check return type

			if (fun.returnType() == null)

				return Error(access, "Can not access return type of void-function!");

			// call ok

			atype = fun.returnType();

			// but add callExpression

			lhs = new CallExpression(lhs, null, lhs.line(), lhs.pos(), null); // we do not know the scope

			lhs.SetType(atype);

		}

		// update left child

		expression.SetLeftChild(lhs);

		switch (atype.kind())

		{

		case OoActionSystemType:

			final Identifier anid = ((OoActionSystemType)atype).ResolveIdentifier(access.tokenText());

			if (anid != null)

			{

				if (anid.kind() == IdentifierKind.MethodIdentifier && !m_entryExpression.callTargets().contains(anid))

					m_entryExpression.callTargets().add((FunctionIdentifier)anid);

				if (staticAccess)

				{

					if ((anid.kind() == IdentifierKind.AttributeIdentifier) &&

							(((AttributeIdentifier)anid).isStatic()))

					{

						final IdentifierExpression newrhs = new IdentifierExpression(anid, access.line(), access.pos());

						expression.SetRightChild(newrhs);

					}

					else

						return Error(access, "Can not access non-static member of an action system");

				}

				else

				{

					if (anid.kind() != IdentifierKind.MethodIdentifier && !selfAccess)

						return Error(access, "Can only access methods of action system objects");

					else

					{

						final IdentifierExpression newrhs = new IdentifierExpression(anid, access.line(), access.pos());

						expression.SetRightChild(newrhs);

					}

				}

			}

			else

				return Error(access, String.format("%s no member of %s",

						access.tokenText(), ((OoActionSystemType)atype).identifier().tokenText()));

			break;

		case EnumeratedType:

			final EnumType anEnum = (EnumType)atype;

			if (!staticAccess)

			{

				return Error(access, "Enum values can only be accessed statically.");

			}

			if (anEnum.symbolTable().Defined(access.tokenText()))

			{

				final Identifier enumid = anEnum.symbolTable().Get(access.tokenText());

				final IdentifierExpression newrhs = new IdentifierExpression(enumid, access.line(), access.pos());

				expression.SetRightChild(newrhs);

			}

			else

				return Error(access, String.format("%s not contained in enum %s",

						access.tokenText(), anEnum.identifier().tokenText()));

			break;

		case QrType:

			final QrType aQualitativeType = (QrType)atype;

			if (!staticAccess)

			{

				return Error(access, "QSpace values can only be accessed statically.");

			}

			if (aQualitativeType.symbolTable().Defined(access.tokenText()))

			{

				final Identifier landmark = aQualitativeType.symbolTable().Get(access.tokenText());

				final IdentifierExpression newrhs = new IdentifierExpression(landmark, access.line(), access.pos());

				expression.SetRightChild(newrhs);

			}

			else

				return Error(access, String.format("%s not contained in qspace %s",

						access.tokenText(), aQualitativeType.identifier().tokenText()));

			break;

		default:

			/*error, we can not access an element with '.' in any other type*/

			return Error(expression, "Expected: System, Enum, Func, or QR type");

		}

		expression.SetType(expression.right().type());

		return expression;

	}

	private Expression ResolveExpression(UnaryOperator expression)

	{

		final Expression child = ResolveExpression(expression.child());

		// if there was some error, then exit

		if (child == null)

			return null;

		if (child.type() == null)

			return Error(expression, "Can not apply unary operator to void-expression");

		switch (expression.kind())

		{

		case Primed:

			expression.SetType(child.type());

			break;

			/*map unary*/

		case dom:           // map A to B -> list of A

			if (child.type().kind() != TypeKind.MapType)

				return Error(expression, "Domain operator only applicable to map types.");

			MapType amap = (MapType)child.type();

			ListType list = new ListType(amap.fromType(), amap.maxNumberOfElements(), null);

			expression.SetType(list);

			break;

		case range:         // map A to B -> list of B

			if (child.type().kind() != TypeKind.MapType)

				return Error(expression, "Range operator only applicable to map types.");

			amap = (MapType)child.type();

			list = new ListType(amap.toType(), amap.maxNumberOfElements(), null);

			expression.SetType(list);

			break;

		case merge:         // list of map A to B -> map A to B

			if ((child.type().kind() == TypeKind.ListType) &&

					(((ListType)child.type()).innerType().kind() == TypeKind.MapType))

			{

				expression.SetType(((ListType)child.type()).innerType());

				break;

			}

			else

				return Error(expression, "Merge operator only applicable to a list of maps");

			/*set/list unary*/

		case card:       // list of A -> int (does not respect dupes, i.e. dupes do not count)

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Cardinality operator only applicable to list types.");

			expression.SetType(new IntType(0, ((ListType)child.type()).maxNumberOfElements(), null));

			break;

		case dconc:      // list of list of A -> list of A

			if ((child.type().kind() == TypeKind.ListType)

					&& (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

			{

				list = (ListType)child.type();

				final ListType innerlist = (ListType)list.innerType();

				final int maxnumber = innerlist.maxNumberOfElements() * list.maxNumberOfElements();

				expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

				break;

			}

			else

				return Error(expression, "Distributed Concatenation operator only applicable to list of lists");

		case dinter:     // list of list of A -> list of A (intersection, does not respect dupes)

			if ((child.type().kind() == TypeKind.ListType)

					&& (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

			{

				list = (ListType)child.type();

				final ListType innerlist = (ListType)list.innerType();

				final int maxnumber = innerlist.maxNumberOfElements();

				expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

				break;

			}

			else

				return Error(expression, "Distributed Intersection operator only applicable to list of lists");

		case dunion:     // list of list of A -> list of A (union, does not respect dupes)

			if ((child.type().kind() == TypeKind.ListType)

					&& (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

			{

				list = (ListType)child.type();

				final ListType innerlist = (ListType)list.innerType();

				// better upper limit?!

						final int maxnumber = innerlist.maxNumberOfElements() * list.maxNumberOfElements();

						expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

						break;

			}

			else

				return Error(expression, "Distributed Union operator only applicable to list of lists");

		case elems:      // list of A -> list of A (does not respect dupes)

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Element operator only applicable to list");

			expression.SetType(child.type());

			break;

		case head:       // list of A -> A

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Head operator only applicable to list");

			expression.SetType(((ListType)child.type()).innerType());

			break;

		case inds:       // list of A -> list of int

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Indices operator only applicable to list");

			list = (ListType)child.type();

			final IntType inner = new IntType(0, list.maxNumberOfElements(), null);

			expression.SetType(new ListType(inner, list.maxNumberOfElements(), null));

			break;

		case len:        // list of A -> int (dupes count)

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Length operator only applicable to list");

			list = (ListType)child.type();

			expression.SetType(new IntType(0, list.maxNumberOfElements(), null));

			break;

		case tail:       // list of A -> list of A

			if (child.type().kind() != TypeKind.ListType)

				return Error(expression, "Tail operator only applicable to list");

			list = (ListType)child.type();

			if (list.maxNumberOfElements() == 0)

				return Error(expression, "Tail operator only applicable to list of length > 0");

			final int newmaxelems = list.maxNumberOfElements() - 1;

			if (newmaxelems == 0)

				Warning(expression, "Tail operator returns empty list.");

			// set the return type null when list is empty?

			expression.SetType(new ListType(list.innerType(), newmaxelems, null));

			break;

			/*unary numberic*/

		case unminus:

			if (!child.type().IsNumeric())

				return Error(expression, "Unary minus only applicable to numeric types");

			expression.SetType(Expression.ArithmeticCover(child.type(), null, expression.kind()));

			break;

		case unplus:

			if (!child.type().IsNumeric())

				return Error(expression, "Unary plus only applicable to numeric types");

			expression.SetType(child.type());

			break;

		case abs:

			if (!child.type().IsNumeric())

				return Error(expression, "Abs only applicable to numeric types");

			expression.SetType(child.type());

			break;

		case not:

			if (/*!IsNumeric(child.type) && */

					(child.type().kind() != TypeKind.BoolType))

				return Error(expression, "Not only applicable to bool types");

			expression.SetType(child.type());

			break;

			/*unary quantors*/

		case forall:

			expression.SetType(new BoolType(null));

			break;

		case exists:

			expression.SetType(new BoolType(null));

			break;

		default:

			throw new NotImplementedException();

		}

		expression.SetChild(child);

		return expression;

	}

	@SuppressWarnings("unchecked")

	private Expression ResolveExpression(BinaryOperator expression)

	{

		Expression lhs = ResolveExpression(expression.left());

		Expression rhs = ResolveExpression(expression.right());

		// if there was some error, then exit

		if ((lhs == null) || (rhs == null))

			return null;

		final UlyssesType lt = lhs.type();

		final UlyssesType rt = rhs.type();

		if ((lt == null) || (rt == null))

			return Error(expression, "Binary operator not applicable to void-type subexpression.");

		switch (expression.kind())

		{

		/*map operators*/

		case domresby:   // list of A * map A to B -> map A to B

		case domresto:   // list of A * map A to B -> map A to B

			if (lt.kind() != TypeKind.ListType)

				return Error(expression, "Domain restriction operator expects list on LHS");

			if (rt.kind() != TypeKind.MapType)

				return Error(expression, "Domain restriction operator expects map on RHS");

			ListType domlist = (ListType)lt;

			MapType domMap = (MapType)rt;

			if (!UlyssesType.TypeEqual(domlist.innerType(), domMap.fromType()))

				return Error(expression, "Inner type of list and domain-type of map do not match");

			// since this is a restriction, maxnumofelems is ok

			expression.SetType(domMap);

			break;

		case rngresby:   // map A to B * list of B -> map A to B

		case rngresto:   // map A to B * list of B -> map A to B

			if (lt.kind() != TypeKind.MapType)

				return Error(expression, "Range restriction operator expects map on LHS");

			if (rt.kind() != TypeKind.ListType)

				return Error(expression, "Rangle restriction operator expects list on RHS");

			final ListType rangelist = (ListType)rt;

			domMap = (MapType)lt;

			if (!UlyssesType.TypeEqual(rangelist.innerType(), domMap.fromType()))

				return Error(expression, "Inner type of list and rangle-type of map do not match");

			// since this is a restriction, maxnumofelems is ok

			expression.SetType(domMap);

			break;

		case munion:     // map A to B * map A to B -> map A to B

			if (lt.kind() != TypeKind.MapType ||

			rt.kind() != TypeKind.MapType)

				return Error(expression, "Map union expects maps on LHS and RHS");

			domMap = (MapType)lt;

			MapType rngMap = (MapType)rt;

			if (!UlyssesType.TypeEqual(domMap.fromType(), rngMap.fromType()) ||

					!UlyssesType.TypeEqual(domMap.toType(), rngMap.toType()))

				return Error(expression, "Domain and Range types of maps must be equal");

			// union may change maximum number of elements..

			final MapType resMap = new MapType(domMap.fromType(), domMap.toType(),

					domMap.maxNumberOfElements() + rngMap.maxNumberOfElements(), null);

			expression.SetType(resMap);

			break;

			/*set/list binary*/

		case conc:       // list of A * list of A -> list of A

			if (lt.kind() != TypeKind.ListType ||

			rt.kind() != TypeKind.ListType)

				return Error(expression, "List concatenation expects two lists.");

			ListType la = (ListType)lt;

			ListType lb = (ListType)rt;

			if (lb.innerType().kind() == TypeKind.Null || lb.maxNumberOfElements() == 0)

				return lhs;

			if (la.innerType().kind() == TypeKind.Null || la.maxNumberOfElements() == 0)

				return rhs;

			if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

				return Error(expression, String.format("Set/List concatenation expects two lists of same type. (%s <> %s)", la.toString(), lb.toString()));

			ListType resultList = new ListType(la.innerType(),

					la.maxNumberOfElements() + lb.maxNumberOfElements(), null);

			expression.SetType(resultList);

			break;

		case diff:       // list of A * list of A -> list of A (does not respect dupes)

			if (lt.kind() != TypeKind.ListType ||

			rt.kind() != TypeKind.ListType)

				return Error(expression, "Set difference expects two lists.");

			la = (ListType)lt;

			lb = (ListType)rt;

			if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

				return Error(expression, "Set difference expects two lists of same type.");

			expression.SetType(la);

			break;

		case inter:      // list of A * list of A -> list of A (does not respect dupes)

			if (lt.kind() != TypeKind.ListType ||

			rt.kind() != TypeKind.ListType)

				return Error(expression, "Set intersection expects two lists.");

			la = (ListType)lt;

			lb = (ListType)rt;

			if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

				return Error(expression, "Set intersection expects two lists of same type.");

			expression.SetType(la.maxNumberOfElements() > lb.maxNumberOfElements() ? la : lb);

			break;

		case elemin:     // A * list of A -> bool

		case notelemin:  // A * list of A -> bool

			if (rt.kind() != TypeKind.ListType)

				return Error(expression, "Element (not) in operator expects list-type as RHS.");

			lb = (ListType)rt;

			if (lhs.kind() == ExpressionKind.Value)

				lhs = UnaryOperator.TryCoerceUp(lhs, lb.innerType());

			final UlyssesType leftType = lhs.type();

			if (!UlyssesType.TypeEqual(leftType, lb.innerType()))

				return Error(expression, String.format("List and element must be of same type: %s in %s",

						lt == null ? "<null>" : lt.toString(), lb ==null || lb.innerType() == null ? "<null>" : lb.innerType().toString()));

			expression.SetType(new BoolType(null));

			break;

		case subset:     // list of A * list of A -> bool (does not respect dupes)

			if (lt.kind() != TypeKind.ListType ||

			rt.kind() != TypeKind.ListType)

				return Error(expression, "Subset operation expects two lists.");

			la = (ListType)lt;

			lb = (ListType)rt;

			if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

				return Error(expression, "Subset operation expects two lists of same type.");

			expression.SetType(new BoolType(null));

			break;

		case union:      // list of A * list of A -> list of A (does not respect dupes)

			if (lt.kind() != TypeKind.ListType ||

			rt.kind() != TypeKind.ListType)

				return Error(expression, "Set union expects two lists.");

			la = (ListType)lt;

			lb = (ListType)rt;

			if (la.innerType().kind() == TypeKind.Null || la.maxNumberOfElements() == 0)

				return rhs;

			if (lb.innerType().kind() == TypeKind.Null || lb.maxNumberOfElements() == 0)

				return lhs;

			if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

				return Error(expression, "Set union expects two lists of same type.");

			resultList = new ListType(la.innerType(),

					la.maxNumberOfElements() + lb.maxNumberOfElements(), null);

			expression.SetType(resultList);

			break;

			/*numeric binary*/

		case pow:

			if (!lt.IsNumeric() || !rt.IsNumeric())

				return Error(expression, "Operator expects LHS and RHS to be numeric");

			if (lt.kind() == TypeKind.IntType && rt.kind() == TypeKind.IntType)

				expression.SetType(lt);

			else

				if (lt.kind() == TypeKind.FloatType)

					expression.SetType(lt);

				else

				{

					final IntType anint = (IntType)lt;

					expression.SetType(new FloatType(anint.rangeLow(), anint.rangeHigh(),

							FloatType.defaultPrecision(), null));

				}

			break;

		case idiv:

		case mod:

			if (rt.kind() != TypeKind.IntType || lt.kind() != TypeKind.IntType)

				return Error(expression, "Operator expects LHS and RHS to be integer");

			expression.SetType(Expression.ArithmeticCover(lt, rt, expression.kind()));

			break;

		case div:

			if (!rt.IsNumeric() || !lt.IsNumeric())

				return Error(expression, "Operator expects LHS and RHS to be numeric");

			if (lhs.type() instanceof ValuedEnumType)

				lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type()).getIntType());

			if (rhs.type() instanceof ValuedEnumType)

				rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type()).getIntType());

			UlyssesType cover = Expression.ArithmeticCover(lt, rt, expression.kind());

			expression.SetType(cover);

			break;

		case minus:

			if (!rt.IsNumeric() || !lt.IsNumeric())

				return Error(expression, "Operator expects LHS and RHS to be numeric");

			if (lhs.type() instanceof ValuedEnumType)

				lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type()).getIntType());

			if (rhs.type() instanceof ValuedEnumType)

				rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type()).getIntType());

			cover = Expression.ArithmeticCover(lt, rt, expression.kind());

			expression.SetType(cover);

			break;

		case prod:

			if (!rt.IsNumeric() || !lt.IsNumeric())

				return Error(expression, "Operator expects LHS and RHS to be numeric");

			if (lhs.type() instanceof ValuedEnumType)

				lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type()).getIntType());

			if (rhs.type() instanceof ValuedEnumType)

				rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type()).getIntType());

			cover = Expression.ArithmeticCover(lt, rt, expression.kind());

			expression.SetType(cover);

			break;

		case sum:

			if (!rt.IsNumeric() || !lt.IsNumeric())

				return Error(expression, "Operator expects LHS and RHS to be numeric");

			if (lhs.type() instanceof ValuedEnumType)

				lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type()).getIntType());

			if (rhs.type() instanceof ValuedEnumType)

				rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type()).getIntType());

			cover = Expression.ArithmeticCover(lt, rt, expression.kind());

			expression.SetType(cover);

			break;

		case greater:

		case greaterequal:

		case less:

		case lessequal:

			if (!((rt.IsNumeric() && lt.IsNumeric()) || (rt.IsQualitative() && lt.IsQualitative())))

				return Error(expression, "Operator expects LHS and RHS to be numeric or qualitative");

			cover = UlyssesType.CoverType(lt, rt);

			if (cover != null)

			{

				lhs = UnaryOperator.TryCoerceUp(lhs, cover);

				rhs = UnaryOperator.TryCoerceUp(rhs, cover);

				expression.SetType(new BoolType(null));

			}

			else

				return Error(expression, String.format("Operator expects LHS and RHS to be of same type (%s <> %s)", lhs.type().toString(), rhs.type().toString()));

			break;

			/*bool binary*/

		case and:

			if (rt.kind() != TypeKind.BoolType || lt.kind() != TypeKind.BoolType)

				return Error(expression, "Operator expects LHS and RHS of bool.");

			expression.SetType(rt);

			// little bit of optimization..

			if (rhs.kind() == ExpressionKind.Value

					&& ((ValueExpression<Boolean>)rhs).value() == false)

				return rhs;

			else if (lhs.kind() == ExpressionKind.Value

					&& ((ValueExpression<Boolean>)lhs).value() == false)

				return lhs;

			// if both are true, then this will be taken care of in constant folding.

			break;

		case biimplies:

			if (rt.kind() != TypeKind.BoolType || lt.kind() != TypeKind.BoolType)

				return Error(expression, "Operator expects LHS and RHS of bool.");

			expression.SetType(rt);

			break;

		case implies:

			if (rt.kind() != TypeKind.BoolType || lt.kind() != TypeKind.BoolType)

				return Error(expression, "Operator expects LHS and RHS of bool.");

			expression.SetType(rt);

			// ex falso...

			if (lhs.kind() == ExpressionKind.Value

					&& ((ValueExpression<Boolean>)lhs).value() == false)

			{

				final Expression shortcut = new ValueExpression<Boolean>(true, expression.line(), expression.pos(), Boolean.class);

				shortcut.SetType(lt);

				return shortcut;

			}

			break;

		case or:

			if (rt.kind() != TypeKind.BoolType || lt.kind() != TypeKind.BoolType)

				return Error(expression, "Operator expects LHS and RHS of bool.");

			expression.SetType(rt);

			if (rhs.kind() == ExpressionKind.Value

					&& ((ValueExpression<Boolean>)rhs).value() == true)

				return rhs;

			else if (lhs.kind() == ExpressionKind.Value

					&& ((ValueExpression<Boolean>)lhs).value() == true)

				return lhs;

			break;

			/*other binary*/

		case equal:

		case notequal:

			cover = UlyssesType.CoverType(lt, rt);

			if (cover != null)

			{

				/* see whether we have a tuple-matcher on one side.. */

				if (expression.kind() == ExpressionKind.equal)

				{

					if (lhs.kind() == ExpressionKind.TupleConstr &&

							((TupleConstructor)lhs).isMatcher())

					{

						if (rhs.kind() == ExpressionKind.TupleConstr &&

								((TupleConstructor)rhs).isMatcher())

							return Error(expression, "Free variables on both sides of the equality sign in tuple constructors.");

						m_matcherList.remove(lhs);

					}

					else if (rhs.kind() == ExpressionKind.TupleConstr &&

							((TupleConstructor)rhs).isMatcher())

					{

						if (lhs.kind() == ExpressionKind.TupleConstr &&

								((TupleConstructor)lhs).isMatcher())

							return Error(expression, "Free variables on both sides of the equality sign in tuple constructors.");

						m_matcherList.remove(rhs);

					}

				}

				lhs = UnaryOperator.TryCoerceUp(lhs, cover);

				rhs = UnaryOperator.TryCoerceUp(rhs, cover);

				expression.SetType(new BoolType(null));

			}

			else

				return Error(expression, String.format("Operator expects LHS and RHS to be of same type (%s <> %s)", lhs.type().toString(), rhs.type().toString()));

			break;

		case seqmod_mapoverride:

			if (rt.kind() != TypeKind.MapType)

				return Error(expression, "Map expected as RHS on sequence modification or map override.");

			// list of A * map int to A -> list of A or

			if (lt.kind() == TypeKind.ListType)

			{

				// we're in sequence modification.

				domlist = (ListType)lt;

				rngMap = (MapType)rt;

				if (rngMap.fromType().kind() != TypeKind.IntType)

					return Error(expression, "Domain of map has to be integer");

				if (!UlyssesType.TypeEqual(domlist.innerType(), rngMap.toType()))

					return Error(expression, "Type of list expected to match range of map");

				// since we only replace elements in the list (by matching ones from the map),

				// we're save to return the original list..

				expression.SetType(lt);

			}

			// map A to B * map A to B -> map A to B

			else if (lt.kind() == TypeKind.MapType)

			{

				domMap = (MapType)lt;

				rngMap = (MapType)rt;

				if (!UlyssesType.TypeEqual(domMap.fromType(), rngMap.fromType()) ||

						!UlyssesType.TypeEqual(domMap.toType(), rngMap.toType()))

					return Error(expression, "Maps need same domain and range types");

				// since we override entries in the first map:

				expression.SetType(domMap);

			}

			else

				return Error(expression, "Sequence Modification or Map override expects list or map as LHS");

			break;

		default:

			throw new NotImplementedException();

		}

		// set subtrees.

		expression.SetLeftChild(lhs);

		expression.SetRightChild(rhs);

		// we only allow:  a = MyTuple(c,d) style matchers

		if (m_matcherList.size() > 0)

		{

			m_matcherList.clear();

			return Error(expression, "Free variables in tuple constructor only allowed in expressions of the form 'atuple = ATupleConstructor(free1,free2...)'");

		}

		// try simple constant folding

		return ApplyConstantFolding(expression);

	}