/**
  *
  *                      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;

import org.momut.ooas.ast.AstNodeTypeEnum;
import org.momut.ooas.ast.IAst;
import org.momut.ooas.ast.expressions.AccessExpression;
import org.momut.ooas.ast.expressions.BinaryOperator;
import org.momut.ooas.ast.expressions.CallExpression;
import org.momut.ooas.ast.expressions.ExistsQuantifier;
import org.momut.ooas.ast.expressions.Expression;
import org.momut.ooas.ast.expressions.ExpressionKind;
import org.momut.ooas.ast.expressions.ForallQuantifier;
import org.momut.ooas.ast.expressions.IdentifierExpression;
import org.momut.ooas.ast.expressions.LeafExpression;
import org.momut.ooas.ast.expressions.ListConstructor;
import org.momut.ooas.ast.expressions.MapConstructor;
import org.momut.ooas.ast.expressions.SetConstructor;
import org.momut.ooas.ast.expressions.TernaryOperator;
import org.momut.ooas.ast.expressions.TupleConstructor;
import org.momut.ooas.ast.expressions.TupleMapAccessExpression;
import org.momut.ooas.ast.expressions.TypeExpression;
import org.momut.ooas.ast.expressions.UnaryOperator;
import org.momut.ooas.ast.expressions.UnresolvedIdentifierExpression;
import org.momut.ooas.ast.expressions.ValueExpression;
import org.momut.ooas.ast.expressions.LeafExpression.LeafTypeEnum;
import org.momut.ooas.ast.expressions.MapConstructor.MapItem;
import org.momut.ooas.ast.identifiers.AttributeIdentifier;
import org.momut.ooas.ast.identifiers.ConstantIdentifier;
import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;
import org.momut.ooas.ast.identifiers.FunctionIdentifier;
import org.momut.ooas.ast.identifiers.Identifier;
import org.momut.ooas.ast.identifiers.IdentifierKind;
import org.momut.ooas.ast.identifiers.ParameterIdentifier;
import org.momut.ooas.ast.identifiers.SelfTypeIdentifier;
import org.momut.ooas.ast.statements.Assignment;
import org.momut.ooas.ast.statements.Call;
import org.momut.ooas.ast.statements.GuardedCommand;
import org.momut.ooas.ast.statements.SeqBlock;
import org.momut.ooas.ast.statements.Statement;
import org.momut.ooas.ast.types.AnyType;
import org.momut.ooas.ast.types.BoolType;
import org.momut.ooas.ast.types.CharType;
import org.momut.ooas.ast.types.EnumType;
import org.momut.ooas.ast.types.FloatType;
import org.momut.ooas.ast.types.FunctionType;
import org.momut.ooas.ast.types.IntType;
import org.momut.ooas.ast.types.ListType;
import org.momut.ooas.ast.types.MapType;
import org.momut.ooas.ast.types.MetaType;
import org.momut.ooas.ast.types.NullType;
import org.momut.ooas.ast.types.OoActionSystemType;
import org.momut.ooas.ast.types.TupleType;
import org.momut.ooas.ast.types.TypeKind;
import org.momut.ooas.ast.types.Type;
import org.momut.ooas.ast.types.ValuedEnumType;
import org.momut.ooas.parser.ParserError;
import org.momut.ooas.parser.ParserMessage;
import org.momut.ooas.parser.ParserState;
import org.momut.ooas.parser.ParserWarning;
import org.momut.ooas.parser.SymbolTable;
import org.momut.ooas.utils.exceptions.ArgumentException;
import org.momut.ooas.utils.exceptions.NotImplementedException;

/// <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 Type acover = Type.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 (!Type.TypeEqual(acover, mid.type()))
			{
				mid = new UnaryOperator(ExpressionKind.Cast, mid, mid.line(), mid.pos());
				mid.SetType(acover);
			}
			if (!Type.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 Type initCover = Type.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 (!Type.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 (!Type.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)
	{
		Type 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 = Type.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 (!Type.TypeEqual(item.type(), type))
				{
					// one exception: lists will not be cast. instead we descend into the inner-most lists and statically update their inner types
					if(item.kind() == ExpressionKind.ListConstr)
					{
						item.Accept(new OoaStaticListCastVisitor((ListType) type));
						item.SetType(type);
						newitems.add(item);
					}
					else
					{
						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)
	{
		Type 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 = Type.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)
	{
		Type domain = null;
		Type 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 = Type.CoverType(domain, domexpr.type());
			range = Type.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<Type> innerTargetType = typeToConstruct.innerTypes().iterator();
		int freeVarCount = 0;
		for (final Expression initexpr: expression.values())
		{
			final Type 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 Type acover = Type.CoverType(innerTargetTypeValue, newval.type());
				if (acover == null || !Type.TypeEqualByKind(innerTargetTypeValue, acover))
					return Error(expression,
						String.format("Element in tuple constructor has non-matching type (%s <> %s)",
								innerTargetTypeValue.toString(), newval.type().toString()));

				if (!Type.TypeEqual(acover, newval.type()))
				{
					newval = new UnaryOperator(ExpressionKind.Cast, newval, newval.line(), newval.pos());
					newval.SetType(acover);
				}
				if (Type.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(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<Type> demandedArgType = funtype.parameter().iterator();
		for (final Expression arg: expression.arguments())
		{
			final Type 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 Type acover = Type.CoverType(newarg.type(), demandedArgTypeValue);
			if (acover == null || !Type.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 (Type.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...
		Type 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);


		if (staticAccess) {
			if (atype.kind() != TypeKind.MetaType)
				return Error(access, "Expected meta type.");
			atype = ((MetaType)atype).Type();
		}


		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;
		default:
			/*error, we can not access an element with '.' in any other type*/
			return Error(expression, "Expected: System, Enum, or Function");
		}

		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 Type lt = lhs.type();
		final Type 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 (!Type.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, "Range restriction operator expects list on RHS");
			final ListType rangelist = (ListType)rt;
			domMap = (MapType)lt;
			if (!Type.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 (!Type.TypeEqual(domMap.fromType(), rngMap.fromType()) ||
					!Type.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 (!Type.TypeEqual(la.innerType(), lb.innerType())) {
				final ListType coverType = (ListType) Type.CoverType(la, lb);
				if(coverType == null)
					return Error(expression, String.format("Set/List concatenation expects two lists of same type. (%s <> %s)", la.toString(), lb.toString())); // FIXME adjust error message

				if(!Type.TypeEqual(la, coverType))
					lhs.Accept(new OoaStaticListCastVisitor(coverType));
				if(!Type.TypeEqual(lb, coverType))
					rhs.Accept(new OoaStaticListCastVisitor(coverType));

				expression.SetType(new ListType(coverType.innerType(), la.maxNumberOfElements() + lb.maxNumberOfElements(), null));
			} else
				expression.SetType(new ListType(la.innerType(), la.maxNumberOfElements() + lb.maxNumberOfElements(), null));

			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 (!Type.TypeEqual(la.innerType(), lb.innerType())) {
				final ListType coverType = (ListType) Type.CoverType(la, lb);
				if(coverType == null)
					return Error(expression, "Set difference expects two lists of same type."); // FIXME adjust error message

				if(!Type.TypeEqual(la, coverType))
					lhs.Accept(new OoaStaticListCastVisitor(coverType));
				if(!Type.TypeEqual(lb, coverType))
					rhs.Accept(new OoaStaticListCastVisitor(coverType));

				expression.SetType(coverType);
			} else
				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 (!Type.TypeEqual(la.innerType(), lb.innerType())) {
				final ListType coverType = (ListType) Type.CoverType(la, lb);
				if(coverType == null)
					return Error(expression, "Set intersection expects two lists of same type.");
				if(!Type.TypeEqual(la, coverType))
					lhs.Accept(new OoaStaticListCastVisitor(coverType));
				if(!Type.TypeEqual(lb, coverType))
					rhs.Accept(new OoaStaticListCastVisitor(coverType));
				expression.SetType(coverType);
			} else
				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 Type leftType = lhs.type();
			if (!Type.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 (!Type.TypeEqual(la.innerType(), lb.innerType())) {
				final ListType coverType = (ListType) Type.CoverType(la, lb);
				if(coverType == null)
					return Error(expression, "Subset operation expects two lists of same type.");

				if(!Type.TypeEqual(la, coverType))
					lhs.Accept(new OoaStaticListCastVisitor(coverType));
				if(!Type.TypeEqual(lb, coverType))
					rhs.Accept(new OoaStaticListCastVisitor(coverType));
			}
			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 (!Type.TypeEqual(la.innerType(), lb.innerType())) {
				final ListType coverType = (ListType) Type.CoverType(la, lb);
				if(coverType == null)
					return Error(expression, "Set union expects two lists of same type.");
				if(!Type.TypeEqual(la, coverType))
					lhs.Accept(new OoaStaticListCastVisitor(coverType));
				if(!Type.TypeEqual(lb, coverType))
					rhs.Accept(new OoaStaticListCastVisitor(coverType));

				expression.SetType(new ListType(coverType.innerType(), la.maxNumberOfElements() + lb.maxNumberOfElements(), null));
			} else
				expression.SetType(new ListType(la.innerType(), la.maxNumberOfElements() + lb.maxNumberOfElements(), null));
			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());
			Type 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()) ))
				return Error(expression, "Operator expects LHS and RHS to be numeric");
			cover = Type.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 = Type.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);
					}

					/* This adds support for "equality-style assignments" in expressions. Not yet supported by the backend though :(
					if (lhs.type().kind() == TypeKind.Any || rhs.type().kind() == TypeKind.Any)
					{
						if (lhs.type().kind() == TypeKind.Any && rhs.type().kind() == TypeKind.Any)
							return Error(expression, "Free variables on both sides of equality sign.");
						// free var - so set type and mark initialized
						final AnyType freevar =  lhs.type().kind() == TypeKind.Any ? (AnyType)lhs.type() : (AnyType)rhs.type();
						freevar.VariableIdentifier().SetType(cover);
						freevar.VariableIdentifier().SetInitialized(true);
						lhs.SetType(cover);
					}
					*/
				}

				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 (!Type.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 (!Type.TypeEqual(domMap.fromType(), rngMap.fromType()) ||
						!Type.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);
	}


	///
	///  We're also doing a bit of constant folding here.
	///

	@SuppressWarnings("unchecked")
	private Expression ApplyConstantFolding(UnaryOperator expression)
	{
		final Expression child = expression.child();
		if (child.type().IsNumeric() && expression.kind() == ExpressionKind.Cast)
		{
			switch (expression.type().kind())
			{
			case FloatType:
				if (child.type().kind() == TypeKind.IntType && child.kind() == ExpressionKind.Value)
				{
					final Expression result = new ValueExpression<Double>((double)((ValueExpression<Integer>)child).value(), child.line(), child.pos(), Double.class);
					result.SetType(expression.type());
					return result;
				}
				break;
			default:
				break;
			}
		}
		return expression;
	}

	@SuppressWarnings("unchecked")
	private Expression ApplyConstantFolding(BinaryOperator expression)
	{
		Expression lhs = expression.left();
		Expression rhs = expression.right();

		if (lhs.kind() == ExpressionKind.Cast)
		{
			lhs = ApplyConstantFolding((UnaryOperator)lhs);
			expression.SetLeftChild(lhs);
		}
		if (rhs.kind() == ExpressionKind.Cast)
		{
			rhs = ApplyConstantFolding((UnaryOperator)rhs);
			expression.SetRightChild(rhs);
		}


		if (lhs.kind() == ExpressionKind.Value && rhs.kind() == ExpressionKind.Value)
			if (expression.type().kind() == TypeKind.FloatType)
			{
				final double fval1 = ((ValueExpression<Double>)lhs).value();
				final double fval2 = ((ValueExpression<Double>)rhs).value();
				double result = 0;
				switch (expression.kind())
				{

				case sum:
					result = fval1 + fval2;
					break;
				case minus:
					result = fval1 - fval2;
					break;
				case prod:
					result = fval1 * fval2;
					break;
				case div:
					if (fval2 == 0)
						return Error(expression, "Division not defined");
					result = fval1 / fval2;
					break;
				default:
					// bail out, if we can not handle it
					return expression;
				}
				if (result < ((FloatType)expression.type()).low()
						|| result > ((FloatType)expression.type()).high())
					return Error(expression, "Internal Error: value after constant folding not in float-range!");

				final ValueExpression<Double> resexp = new ValueExpression<Double>(result, expression.line(), expression.pos(), Double.class);
				resexp.SetType(expression.type());
				return resexp;
			}
			else if (expression.type().kind() == TypeKind.IntType)
			{
				final int val1 = ((ValueExpression<Integer>)lhs).value();
				final int val2 = ((ValueExpression<Integer>)rhs).value();
				int result = 0;
				switch (expression.kind())
				{
				case sum:
					result = val1 + val2;
					break;
				case minus:
					result = val1 - val2;
					break;
				case prod:
					result = val1 * val2;
					break;
				case idiv:
					if (val2 == 0)
						return Error(expression, "Division not defined.");
					result = val1 / val2;
					break;
				case mod:
					result = val1 % val2;
					break;
				default:
					// bail out, if we can not handle it
					return expression;
				}

				if (result < ((IntType)expression.type()).rangeLow()
						|| result > ((IntType)expression.type()).rangeHigh())
					return Error(expression, "Internal Error: value after constant folding not in int-range!");

				final ValueExpression<Integer> intres = new ValueExpression<Integer>(result, expression.line(), expression.pos(), Integer.class);
				intres.SetType(expression.type());
				return intres;
			}
			else if (expression.type().kind() == TypeKind.BoolType)
			{
				boolean result = false;
				switch (expression.kind())
				{
				case greater:
					assert(lhs.type().kind() == rhs.type().kind());
					switch (lhs.type().kind())
					{
					case IntType:
						result = ((ValueExpression<Integer>)lhs).value() >
							((ValueExpression<Integer>)rhs).value();
						break;
					case FloatType:
						result = ((ValueExpression<Double>)lhs).value() >
							((ValueExpression<Double>)rhs).value();
						break;
					default:
						return expression;
					}
					break;
				case greaterequal:
					assert(lhs.type().kind() == rhs.type().kind());
					switch (lhs.type().kind())
					{
					case IntType:
						result = ((ValueExpression<Integer>)lhs).value() >=
							((ValueExpression<Integer>)rhs).value();
						break;
					case FloatType:
						result = ((ValueExpression<Double>)lhs).value() >=
							((ValueExpression<Double>)rhs).value();
						break;
					default:
						return expression;
					}
					break;
				case less:
					assert(lhs.type().kind() == rhs.type().kind());
					switch (lhs.type().kind())
					{
					case IntType:
						result = ((ValueExpression<Integer>)lhs).value() <
							((ValueExpression<Integer>)rhs).value();
						break;
					case FloatType:
						result = ((ValueExpression<Double>)lhs).value() <
							((ValueExpression<Double>)rhs).value();
						break;
					default:
						return expression;
					}
					break;
				case lessequal:
					assert(lhs.type().kind() == rhs.type().kind());
					switch (lhs.type().kind())
					{
					case IntType:
						result = ((ValueExpression<Integer>)lhs).value() <=
							((ValueExpression<Integer>)rhs).value();
						break;
					case FloatType:
						result = ((ValueExpression<Double>)lhs).value() <=
							((ValueExpression<Double>)rhs).value();
						break;
					default:
						return expression;
					}
					break;
				case and:
					result = ((ValueExpression<Boolean>)lhs).value() && ((ValueExpression<Boolean>)rhs).value();
					break;
				case equal:
					// we have to be careful here, since equal takes all sorts of types..
					assert(lhs.type().kind() == rhs.type().kind());
					switch (lhs.type().kind())
					{
					case BoolType:
						result = ((ValueExpression<Boolean>)lhs).value() ==
							((ValueExpression<Boolean>)rhs).value();
						break;
					case IntType:
						result = ((ValueExpression<Integer>)lhs).value() ==
							((ValueExpression<Integer>)rhs).value();
						break;
					case FloatType:
						result = ((ValueExpression<Double>)lhs).value() ==
							((ValueExpression<Double>)rhs).value();
						break;
					default:
						return expression;
					}
					break;
				case biimplies:
					result = ((ValueExpression<Boolean>)lhs).value() == ((ValueExpression<Boolean>)rhs).value();
					break;
				case implies:
					result = !((ValueExpression<Boolean>)lhs).value() || ((ValueExpression<Boolean>)rhs).value();
					break;
				case or:
					result = ((ValueExpression<Boolean>)lhs).value() || ((ValueExpression<Boolean>)rhs).value();
					break;
				default:
					return expression;
				}
				final ValueExpression<Boolean> boolres = new ValueExpression<Boolean>(result, expression.line(), expression.pos(), Boolean.class);
				boolres.SetType(expression.type());
				return boolres;
			}

		return expression;
	}


	///
	///  "jump table" (could by avoided by 'dynamic' type as found in c#4)
	///

	@SuppressWarnings("unchecked")
	private Expression ResolveExpression(Expression expression)
	{
		if (expression == null) return null;

		Expression result = expression;

		switch (expression.kind())
		{
		case Value:
			final LeafExpression aValue = (LeafExpression)expression;
			switch (aValue.valueType())
			{
			case bool:
				expression.SetType(new BoolType(null));
				break;
			case chr:
				expression.SetType(new CharType(null));// IntType(0, 255, null));
				break;
			case complex:
			case identifier:
				assert(false);
				break;
			case integer:
				final int val = ((ValueExpression<Integer>)expression).value();
				expression.SetType(new IntType(val, val, null));
				break;
			case qval:
				throw new NotImplementedException();
			case real:
				final double fval = ((ValueExpression<Double>)expression).value();
				expression.SetType(new FloatType(fval, fval, fval, null));
				break;
			case reference:
				final Object aref = ((ValueExpression<?>)expression).value();
				if (aref == null)
					expression.SetType(new NullType());
				else
				{
					assert(false);
					return null;
				}
				break;
			case unset:
				throw new NotImplementedException();
			default:
				break;
			}
			result = expression;
			break;

			/* ternary operators */
		case conditional:
		case foldLR:
		case foldRL:
			result = ResolveExpression((TernaryOperator)expression);
			break;

			/* forall */
		case forall:
			result = ResolveExpression((ForallQuantifier)expression);
			break;

			/* exists */
		case exists:
			result = ResolveExpression((ExistsQuantifier)expression);
			break;

			/* constructors */
		case ListConstr:
			result = ResolveExpression((ListConstructor)expression);
			break;
		case SetConstr:
			result = ResolveExpression((SetConstructor)expression);
			break;
		case MapConstr:
			result = ResolveExpression((MapConstructor)expression);
			break;
		case TupleConstr:
			result = ResolveExpression((TupleConstructor)expression);
			break;
		case ObjectConstr:
			result = expression;
			break;

			/* identifiers */
		case Identifier:
			result = ResolveExpression((IdentifierExpression)expression);
			break;
		case UnresolvedIdentifier:
			result = ResolveExpression((UnresolvedIdentifierExpression)expression);
			break;

			/* evaluate */
		case TupleMapAccess:
			result = ResolveExpression((TupleMapAccessExpression)expression);
			break;
		case Call:
			result = ResolveExpression((CallExpression)expression);
			break;

			/* access some element within a class.. */
		case Access:
			result = ResolveExpression((AccessExpression)expression);
			break;


		case Cast:
			final UnaryOperator cast = (UnaryOperator)expression;

			/*prevent casts of complex datatypes, e.g. lists etc..*/
			if (cast.type().kind() != TypeKind.OoActionSystemType)
				return Error(cast, String.format("Cast operator needs class type as argument. (Expected: OoActionSystemType, Found: %s)", cast.type().kind().name()));

			cast.SetChild(ResolveExpression(cast.child()));
			final Type acover = Type.CoverType(cast.type(), cast.child().type());
			final boolean upcast = Type.TypeEqual(acover, cast.type());           // the cast is safe; Mostly used in list constructors..
			final boolean downcast = Type.TypeEqual(acover, cast.child().type()); // downcast, unsafe.
			if (downcast)
				Info(cast, String.format("Potentially unsafe downcast: %s as %s (cover: %s)",
					cast.child().type().toString(), cast.type().toString(), acover.toString()));
			if (acover == null || !(upcast || downcast))
				return Error(cast, String.format("Invalid cast: %s as %s (cover: %s)",
					cast.child().type().toString(), cast.type().toString(), acover != null ? acover.toString() : "<none>"));

			result = cast;
			break;

			/* general unary operators */
		case Primed:
		case unminus:
		case unplus:
		case not:
		case abs:
		case dom:
		case range:
		case merge:
		case card:
		case dconc:
		case dinter:
		case dunion:
		case elems:
		case head:
		case inds:
		case len:
		case tail:
			result = ResolveExpression((UnaryOperator)expression);
			break;

			/* general binary operators */
		case domresby:
		case domresto:
		case rngresby:
		case rngresto:
		case munion:
		case conc:
		case diff:
		case inter:
		case elemin:
		case notelemin:
		case subset:
		case union:
		case div:
		case greater:
		case greaterequal:
		case idiv:
		case less:
		case lessequal:
		case minus:
		case mod:
		case pow:
		case prod:
		case sum:
		case and:
		case biimplies:
		case implies:
		case or:
		case equal:
		case notequal:
		case seqmod_mapoverride:
			result = ResolveExpression((BinaryOperator)expression);
			break;
		default:
			throw new NotImplementedException();
		}

		return result;
	}


	public Expression ResolveExpressionNewScope(Expression toResolve)
	{
		Expression result = null;

		m_freeVariables.push(new SymbolTable());
		try
		{
			result = ResolveExpression(toResolve);
		}
		finally
		{
			if (result != null)
				result.SetFreeVariables(m_freeVariables.pop());
		}
		return result;
	}


	///
	///  called for every element in the ast
	///

	@Override
	protected void VisitAstElement(IAst subElement, IAst parent)
	{
		if (subElement.nodeType() == AstNodeTypeEnum.expression)
		{
			// calculate a new (resolved) expression
			m_freeVariables.push(new SymbolTable());
			// save toplevel -- used to keep track of method calls.
			m_entryExpression = (Expression)subElement;

			final Expression newExpression = ResolveExpression(m_entryExpression);
			// replace the expression in the parent
			if (newExpression != null)
			{
				newExpression.SetFreeVariables(m_freeVariables.pop());
				ReplaceExpression(parent, (Expression)subElement, newExpression);
			}

		}
		else
			subElement.Accept(this); // saves us the call to base.VisitAstElement
	}


	///
	///  PUBLIC METHODS
	///

	public OoaResolveExpressionsVisitor(ParserState aState)
	{
		super (aState);
		if (aState == null)
			throw new ArgumentException();
	}
}