/**
  *
  *                      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.codegen.cadp;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;

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.ListConstructor;
import org.momut.ooas.ast.expressions.MapConstructor;
import org.momut.ooas.ast.expressions.ObjectConstructor;
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.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.types.FunctionType;
import org.momut.ooas.ast.types.ListType;
import org.momut.ooas.ast.types.MapType;
import org.momut.ooas.ast.types.OoActionSystemInstance;
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.codegen.OoasCodeEmitter;
import org.momut.ooas.parser.SymbolTable;
import org.momut.ooas.visitors.OoaExpressionVisitor;

/// <summary>
/// Knows how to construct a C-CADP expression from an AST-expression
/// (only basic arithmetical operations supported)
/// </summary>
public final class CadpExpression extends OoaExpressionVisitor
{
	private OoasCodeEmitter m_emitter = new OoasCodeEmitter();
	private final CadpActionInfo m_procInfo;
	private final ArrayList<Identifier> m_usedIdentifier = new ArrayList<Identifier>();
	private static OoasCodeEmitter m_helperCode = new OoasCodeEmitter();
	private static OoasCodeEmitter m_resetCode = new OoasCodeEmitter();

	public static HashSet<String> emittedOperations = new HashSet<String>();
	public List<Identifier> usedIdentifiers() { return m_usedIdentifier; }

	private String OperatorString(Expression expression)
	{
		switch (expression.kind())
		{
		case abs:    // T_ABS:
		case card:   // T_CARD:
		case dom:    // T_DOM:
		case range:  // T_RNG:
		case merge:  // T_MERGE:
		case elems:  // T_ELEMS:
		case inds:   // T_INDS:
		case dinter: // T_DINTER:
		case dunion: // T_DUNION:
		case domresby:   // T_DOMRESBY:
		case domresto:   // T_DOMRESTO:
		case rngresby:   // T_RNGRESBY:
		case rngresto:   // T_RNGRESTO:
		case inter:  // T_INTER:
		case union:  // T_UNION:
		case munion: // T_MUNION:
		case seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:
		case subset:
		case biimplies:  // T_BIIMPLIES:
		case Primed:
			throw new UnsupportedOperationException();

		case notelemin:
		case elemin:
		case implies:    // T_IMPLIES:
		case conc:   // T_CONC:
		case head:   // T_HEAD:
		case tail:   // T_TAIL:
		case len:    // T_LEN:
			throw new IllegalArgumentException(); // handled directly in binary operator! (T_CONC instanceof still todo, however)


		case div:    // T_DIV:
			return "/";
		case idiv:   // T_IDIV:
			return "/";
		case mod:    // T_MOD:
			return "%";
		case prod:   // T_PROD:
			return "*";
		case sum:    // T_SUM:
			return "+";
		case minus:  // T_MINUS:
			return "-";
		case less:
			return "<";
		case lessequal:
			return "<=";
		case greater:
			return ">";
		case greaterequal:
			return ">=";
		case equal:
			return "==";
		case notequal:
			return "!=";
		case and:    // T_AND:
			return "&&";
		case or:     // T_OR:
			return "||";
		case not:
			return "!";

		case Cast:
			throw new IllegalArgumentException(); // handled elsewhere
			/*if (expression.type != null)
                    return "("+expression.type().ToString()+")";
                else
                    return "(??Cast??)";*/

		default:
			return expression.kind().toString();
		}
	}
	@Override
	public <T>void visit(ValueExpression<T> valueExpression)
	{
		if (valueExpression.value() == null)
		{
			m_emitter.Append("NULL");
		}
		else if (valueExpression.valueType() == LeafTypeEnum.bool)
		{
			// bad hack..
			final boolean aboolval = (Boolean)valueExpression.value();
			m_emitter.AppendLine(aboolval ? "1" : "0");
		}
		else if (valueExpression.valueType() == LeafTypeEnum.chr)
			m_emitter.Append(String.format("'%1$s'", valueExpression.toString()));
		else
			m_emitter.Append(valueExpression.value().toString());
	}
	@Override
	public  void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)
	{
		throw new IllegalArgumentException();
	}

	@Override
	public  void visit(IdentifierExpression identifierExpression)
	{
		final CadpIdentifier idvis = new CadpIdentifier(m_procInfo.stateVariableString);
		identifierExpression.Accept(idvis);
		m_emitter.Append(idvis.toString());

		if (identifierExpression.identifier().kind() == IdentifierKind.ExpressionVariableIdentifier)
		{
			// we need to define the variable
			// declare free variables
			final ExpressionVariableIdentifier id = (ExpressionVariableIdentifier)identifierExpression.identifier();
			if (!emittedVariabes.contains(id))
			{
				emittedVariabes.add(id);
				final CadpType atype = new CadpType();
				id.type().Accept(atype);
				varDecl.Append(String.format("%1$s %2$s; ", atype.ToString(), idvis.toString()));
			}
		}
		// we memorize all identifiers
		if (!m_usedIdentifier.contains(identifierExpression.identifier()))
			m_usedIdentifier.add(identifierExpression.identifier());
	}

	@Override
	public  void visit(TypeExpression typeExpression)
	{
		m_emitter.Append(typeExpression.referredType().identifier().tokenText());
	}

	@Override
	public  void visit(ListConstructor listConstructor)
	{
		final ListType aListType = (ListType)listConstructor.type();
		if (!listConstructor.hasComprehension())
		{
			CadpType.EmitType(aListType);

			m_emitter.Append(String.format("%1$s%2$s(%3$s", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aListType.identifier()), listConstructor.elements().size()));
			int i;
			for (i = 0; i < aListType.maxNumberOfElements(); i++)
			{
				m_emitter.Append(", ");
				if (i < listConstructor.elements().size())
					listConstructor.elements().get(i).Accept(this);
				else
					m_emitter.Append(String.format("%1$s%2$s(%3$s%2$s())", CadpType.enumString, CadpIdentifier.GetIdentifierString(aListType.innerType().identifier()), CadpType.lowString));
			}
			m_emitter.Append(")");
		}
		else
		{
			final CadpExpression compExpr = new CadpExpression(new CadpActionInfo(null, -1, 0, m_procInfo.toDoListString, m_procInfo.doneListString, "aState"), emittedVariabes);
			if (listConstructor.comprehension() != null)
				listConstructor.comprehension().Accept(compExpr);
			else
				new ValueExpression<Integer>(1, 0, 0, Integer.class).Accept(compExpr);

			final CadpExpression listElementExpr = new CadpExpression(m_procInfo, emittedVariabes);
			listConstructor.elements().get(0).Accept(listElementExpr);

			// get a list of imported variabes
			compExpr.usedIdentifiers().addAll(listElementExpr.usedIdentifiers());
			final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, listConstructor.comprehensionVariables());


			// Idea: reduce importVars by compExpr.VariableDeclarations
			// importVars.RemoveAll( (x) => if (x in compExpr.Vara... ) return true);

			// BEGIN FIXXME
			final List<Identifier> varsToRemove = new ArrayList<Identifier>();

			for (final Identifier id : importVars)
			{
				final CadpType atype = new CadpType();
				id.type().Accept(atype);
				final String typeAndName = (String.format("%1$s %2$s; ", atype.ToString(), id.tokenText()));

				if (compExpr.VariableDeclarations().contains(typeAndName))
					varsToRemove.add(id);
			}
			int tmpcntr = importVars.size() -1;
			for (tmpcntr = importVars.size() -1; tmpcntr>=0; tmpcntr--)
				if (varsToRemove.contains(importVars.get(tmpcntr)))
					importVars.remove(tmpcntr);
			// END FIXXME

			final String functionName = String.format("create_dyn_list_%1$s", OoaCADPVisitor.getUIntHashCode(listConstructor));
			m_emitter.Append(functionName);
			m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
			for (final Identifier x : importVars)
			{
				m_emitter.Append(",");
				m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
			}
			m_emitter.Append(")");

			// emit helper
			final ListType listType = (ListType)listConstructor.type();
			CadpType.EmitType(listType.innerType());
			final OoasCodeEmitter helper = new OoasCodeEmitter();
			final String listtypename = String.format("struct_list_%1$s", CadpType.DumpType(listType.innerType()).replaceAll(" ", "_"));


			final StringBuilder typedefbuilder = new StringBuilder();
			typedefbuilder.append("#ifdef WINDOWSPACK" + System.lineSeparator());
			typedefbuilder.append("#pragma pack(1)" + System.lineSeparator());
			typedefbuilder.append("#endif" + System.lineSeparator());
			typedefbuilder.append(String.format("struct %2$s { struct %2$s *next; %1$s element;} UNIXPACK;", CadpType.DumpType(listType.innerType()), listtypename));
			typedefbuilder.append(System.lineSeparator());
			final String listStruct = typedefbuilder.toString();
			CadpType.AddTypeDefinition(listStruct);

			helper.AppendLine(String.format("struct %1$s* %2$s(CAESAR_TYPE_STATE aState", listtypename, functionName));
			for (final Identifier x : importVars)
			{
				helper.Append(", ");
				helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
			}
			helper.AppendLine("){");

			helper.AppendLine(String.format("struct %1$s* result = NULL;", listtypename));
			helper.AppendLine(String.format("struct %1$s* __currhead = NULL;", listtypename));
			helper.AppendLine(compExpr.VariableDeclarations());

			int loops = 0;
			for (final Identifier enumvar : listConstructor.comprehensionVariables().symbolList())
			{
				helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
				helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
						CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));

				if (compExpr.VariableDeclarations().contains(String.format(" %1$s;", CadpIdentifier.GetIdentifierString(enumvar))))
					helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
							CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
				else
					helper.AppendLine(String.format("%1$s %2$s = %3$s(iterator_%2$s);",
							CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
				loops++;
			}

			helper.AppendLine(String.format("%1$s __newElem;", CadpType.DumpType(listType.innerType())));


			helper.AppendLine(String.format("if ((%1$s) && (CALC_INVALID == 0)) { __newElem = %2$s; ", compExpr.toString(), listElementExpr.toString()));

			helper.AppendLine(String.format("struct %1$s* __listelem =  (struct %1$s*) malloc(sizeof(struct %1$s));", listtypename));
			helper.AppendLine(String.format("if (__listelem == NULL) { fprintf(stderr,\"malloc failure\"); exit(1);}"));
			helper.AppendLine(String.format("memset((char*)__listelem,0,sizeof(struct %1$s));", listtypename));

			helper.AppendLine(String.format(String.format("memcpy(&(__listelem->element),&__newElem, sizeof(%1$s));", CadpType.DumpType(listType.innerType()))));
			helper.AppendLine(String.format("if (result == NULL) result = __listelem; else __currhead->next = __listelem; __currhead = __listelem;"));

			helper.AppendLine("} /*if*/");
			helper.AppendLine("if (CALC_INVALID == 1) CALC_INVALID = 0;");
			while (loops > 0)
			{
				helper.AppendLine("}");
				loops--;
			}
			helper.AppendLine("return result; }");

			m_helperCode.Append(helper.toString());
		}
	}

	@Override
	public  void visit(SetConstructor setConstructor)
	{
		final ListType aSetType = (ListType)setConstructor.type();
		m_emitter.Append(String.format(" /*set constr*/ %1$s%2$s(", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aSetType.identifier())));
		m_emitter.Append(setConstructor.items().size());
		for (final Expression x : setConstructor.items())
		{
			m_emitter.Append(", ");
			x.Accept(this);
		}
		m_emitter.Append(")");
	}

	@Override
	public  void visit(MapConstructor mapConstructor)
	{
		throw new UnsupportedOperationException();
	}

	@Override
	public  void visit(TupleConstructor tupleConstructor)
	{
		final TupleType aTupleType = (TupleType)tupleConstructor.type();

		if (tupleConstructor.isMatcher())
		{
			// being dealt with in binaryoperator (since we only allow tuple=MyTuple(a,b))
			throw new IllegalArgumentException();
		}
		else
		{
			m_emitter.Append(String.format("%1$s%2$s(", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aTupleType.identifier())));
			int i = 0;
			for (final Expression x : tupleConstructor.values())
			{
				if (i != 0)
					m_emitter.Append(", ");
				else
					i++;
				x.Accept(this);
			}
			m_emitter.Append(")");
		}
	}

	@Override
	public void visit(ObjectConstructor objectConstructor)
	{
		final OoActionSystemInstance instance = objectConstructor.GetNextInstance();
		CadpType.EmitType(instance.Type);
		if (objectConstructor.instances().size() == 1)
		{
			m_emitter.Append(String.format("%1$s", instance.Name));
		}
		else
		{
			final String helpername = String.format("obj_constr_%1$s", OoaCADPVisitor.getUIntHashCode(objectConstructor));
			m_emitter.Append(String.format("%1$s()", helpername));

			// emit helper

			final OoasCodeEmitter helper = new OoasCodeEmitter();
			helper.AppendLine(String.format("int %1$s_counter = 0;", helpername));
			m_resetCode.AppendLine(String.format("%1$s_counter = 0;", helpername));
			helper.AppendLine(String.format("%1$s %2$s(){", CadpType.DumpType(objectConstructor.type()), helpername));
			int i = 0;
			for (final OoActionSystemInstance x : objectConstructor.instances())
			{
				CadpType.EmitType(x.Type);
				helper.AppendLine(String.format("if (%1$s_counter == %2$s) {%1$s_counter++; return %3$s;}",
						helpername, i, x.Name));
				i++;
			}
			helper.AppendLine(String.format("fprintf(stderr,\"constructor called too often: %1$s\"); exit(1);", helpername));
			helper.Append("}");
			m_helperCode.AppendLine(helper.toString());
		}
	}


	@Override
	public  void visit(AccessExpression accessExpression)
	{
		// if this instanceof some "<enumType>.<enumValue>" access, then just print the numeric value of <enumValue>
		if (accessExpression.left().kind() == ExpressionKind.Type &&
		    ((TypeExpression)accessExpression.left()).referredType().kind() == TypeKind.EnumeratedType )
		{
			accessExpression.right().Accept(this);
			return;
		}

		// we normally skip the self, except for the case of method
		// accesses (where we need to go over the jumptable
		if (accessExpression.left().kind() == ExpressionKind.Identifier &&
				((IdentifierExpression)accessExpression.left()).isSelf())
		{
			if (accessExpression.right().kind() != ExpressionKind.Identifier ||
					((IdentifierExpression)accessExpression.right()).identifier().kind() != IdentifierKind.MethodIdentifier)
			{
				accessExpression.right().Accept(this);
				return;
			}
		}

		accessExpression.left().Accept(this);
		m_emitter.Append(".");
		// in oder to save memory, we do method access via a jump table
		if (((IdentifierExpression)accessExpression.right()).identifier().kind() == IdentifierKind.MethodIdentifier ||
				((IdentifierExpression)accessExpression.right()).identifier().kind() == IdentifierKind.NamedActionIdentifier)
			m_emitter.Append("methods->");
		accessExpression.right().Accept(this);
	}


	OoasCodeEmitter varDecl = new OoasCodeEmitter();
	HashSet<Identifier> emittedVariabes = new HashSet<Identifier>();

	public void addEmittedVariables(HashSet<Identifier> elementsToAdd)
	{
		emittedVariabes.addAll(elementsToAdd);
	}

	private void EmitMatcher(TupleConstructor tupleConstructor, Expression expression)
	{
		final OoasCodeEmitter tmp = m_emitter;
		// get the expression
		m_emitter = new OoasCodeEmitter();
		expression.Accept(this);
		final OoasCodeEmitter expr = m_emitter;
		m_emitter = tmp;

		// treat cases of MyTuple(a,b..) = <expr>
		final Iterator<Type> elem = ((TupleType)tupleConstructor.type()).innerTypes().iterator();
		int i = 0;
		m_emitter.Append("(");
		while (elem.hasNext())
		{
			final Expression var = tupleConstructor.values().get(i);

			if (i != 0)
				m_emitter.Append(" , ");

			var.Accept(this);
			m_emitter.Append(String.format(" = (%1$s).elem_%2$s ", expr.toString(), i));

			i++;
		}
		m_emitter.Append(", 1==1)");
	}

	private void EmitDefaultBinaryOperator(BinaryOperator binaryOperator)
	{
		m_emitter.Append("(");
		VisitSub(binaryOperator.left(), binaryOperator);
		m_emitter.Append(") ");
		m_emitter.Append(OperatorString(binaryOperator));
		m_emitter.Append(" (");
		VisitSub(binaryOperator.right(), binaryOperator);
		m_emitter.Append(")");
	}

	@Override
	public  void visit(BinaryOperator binaryOperator)
	{
		switch (binaryOperator.kind())
		{
		case equal:
			/*check if we have tupleconstructors as matchers*/
			if (binaryOperator.left().kind() == ExpressionKind.TupleConstr &&
			((TupleConstructor)binaryOperator.left()).isMatcher())
			{
				EmitMatcher((TupleConstructor)binaryOperator.left(), binaryOperator.right());
			}
			else if (binaryOperator.right().kind() == ExpressionKind.TupleConstr &&
					((TupleConstructor)binaryOperator.right()).isMatcher())
			{
				EmitMatcher((TupleConstructor)binaryOperator.right(), binaryOperator.left());
			}/* check whether we must use memcmp */
			else if (!CadpType.IsNumeric(binaryOperator.left().type()))
			{
				m_emitter.Append("0 == ");
				EmitComplexEqual(binaryOperator);
			}
			else
				EmitDefaultBinaryOperator(binaryOperator);
			break;
		case notequal:
			if (!CadpType.IsNumeric(binaryOperator.left().type()))
			{
				m_emitter.Append("0 != ");
				EmitComplexEqual(binaryOperator);
			}
			else
				EmitDefaultBinaryOperator(binaryOperator);
			break;
		case conc:
			final String conc = EmitConcOperation(binaryOperator);
			m_emitter.Append(String.format("%1$s(", conc));
			VisitSub(binaryOperator.left(), binaryOperator);
			m_emitter.Append(",");
			VisitSub(binaryOperator.right(), binaryOperator);
			m_emitter.Append(")");
			break;
		case implies:
			m_emitter.Append("!(");
			VisitSub(binaryOperator.left(), binaryOperator);
			m_emitter.Append(") || (");
			VisitSub(binaryOperator.right(), binaryOperator);
			m_emitter.Append(")");
			break;
		case elemin:
			EmitInOperator(binaryOperator);
			break;
		case notelemin:
			EmitNotInOperator(binaryOperator);
			break;
		case diff:   // T_DIFF:
			final String diff = EmitSetDifference(binaryOperator);
			m_emitter.Append(String.format("%1$s(", diff));
			VisitSub(binaryOperator.left(), binaryOperator);
			m_emitter.Append(",");
			VisitSub(binaryOperator.right(), binaryOperator);
			m_emitter.Append(")");
			break;
		default:
			EmitDefaultBinaryOperator(binaryOperator);
			break;
		}
	}

	private String EmitSetDifference(BinaryOperator binaryOperator)
	{
		final String childBTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.right().type().identifier());
		final String childATypeName = CadpIdentifier.GetIdentifierString(binaryOperator.left().type().identifier());
		final String result = String.format("op_listdiff_%1$s_%2$s", childATypeName, childBTypeName);
		if (emittedOperations.contains(result))
			return result;

		CadpType.EmitType(binaryOperator.type());
		final ListType alist = (ListType)binaryOperator.type();
		final Type innerType = alist.innerType();
		final String resultTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.type().identifier());

		m_helperCode.AppendLine(String.format("%4$s %3$s(%1$s listA, %2$s listB){", childATypeName, childBTypeName, result, resultTypeName));
		m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
		m_helperCode.AppendLine(String.format("int len = 0; int i; int j;"));

		m_helperCode.AppendLine(String.format("for (i = 0; i < listA.length; i++) {"));
		m_helperCode.AppendLine(String.format("for (j = 0; j < listB.length; j++) {"));
		m_helperCode.AppendLine(String.format("if (memcmp(&listA.elements[i],&listB.elements[j],sizeof(%1$s))==0)", CadpType.DumpType(innerType)));
		m_helperCode.AppendLine("goto NotCopy;");
		m_helperCode.AppendLine("}");
		m_helperCode.AppendLine(String.format("memcpy(&result.elements[len],&listA.elements[i],sizeof(%1$s));", CadpType.DumpType(innerType)));
		m_helperCode.AppendLine("len++;");
		m_helperCode.AppendLine("NotCopy:");
		m_helperCode.AppendLine("len = len;");
		m_helperCode.AppendLine("}");
		m_helperCode.AppendLine("result.length = len;");

		// in case our resulttype was set wider..
		m_helperCode.AppendLine(String.format("int counter;"));
		m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", ((ListType)binaryOperator.type()).maxNumberOfElements() - 1));
		m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
				CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));

		m_helperCode.AppendLine("return result; }");

		emittedOperations.add(result);
		return result;
	}

	private void EmitInOperator(BinaryOperator binop)
	{
		m_emitter.Append(String.format("0 != setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		VisitSub(binop.left(), binop);
		m_emitter.Append(",");
		VisitSub(binop.right(), binop);
		m_emitter.Append(")");

		CadpType.EmitType(binop.left().type());
		CadpType.EmitType(binop.right().type());
		final OoasCodeEmitter helper = new OoasCodeEmitter();
		helper.Append(String.format("int setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
		helper.AppendLine("int __counter;");
		helper.AppendLine(String.format("for (__counter = 0; __counter < arg2.length; __counter++)"/*, CadpType.GetMaxVal(binop.right().type)*/));
		helper.AppendLine(String.format("if (memcmp(&arg1,&(arg2.elements[__counter]),sizeof(%1$s))==0) return 1;", CadpType.DumpType(binop.left().type())));
		helper.AppendLine("return 0;}");
		m_helperCode.Append(helper.toString());
	}


	private void EmitNotInOperator(BinaryOperator binop)
	{
		m_emitter.Append(String.format("0 == setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		VisitSub(binop.left(), binop);
		m_emitter.Append(",");
		VisitSub(binop.right(), binop);
		m_emitter.Append(")");

		CadpType.EmitType(binop.left().type());
		CadpType.EmitType(binop.right().type());
		final OoasCodeEmitter helper = new OoasCodeEmitter();
		helper.Append(String.format("int setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
		helper.AppendLine("int __counter;");
		helper.AppendLine(String.format("for (__counter = 0; __counter < arg2.length; __counter++)"/*, CadpType.GetMaxVal(binop.right().type)*/));
		helper.AppendLine(String.format("if (memcmp(&arg1,&(arg2.elements[__counter]),sizeof(%1$s))==0) return 1;", CadpType.DumpType(binop.left().type())));
		helper.AppendLine("return 0;}");
		m_helperCode.Append(helper.toString());
	}



	private void EmitComplexEqual(BinaryOperator binop)
	{
		m_emitter.Append(String.format("complex_equal_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		VisitSub(binop.left(), binop);
		m_emitter.Append(",");
		VisitSub(binop.right(), binop);
		m_emitter.Append(")");

		CadpType.EmitType(binop.left().type());
		CadpType.EmitType(binop.right().type());
		final OoasCodeEmitter helper = new OoasCodeEmitter();
		helper.Append(String.format("int complex_equal_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
		helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
		helper.AppendLine(String.format("return memcmp(&arg1, &arg2, sizeof(%1$s));}", CadpIdentifier.GetIdentifierString(binop.left().type().identifier())));
		m_helperCode.Append(helper.toString());
	}

	private String EmitConcOperation(BinaryOperator binaryOperator)
	{
		final String childBTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.right().type().identifier());
		final String childATypeName = CadpIdentifier.GetIdentifierString(binaryOperator.left().type().identifier());
		final String result = String.format("op_conc_%1$s_%2$s", childATypeName, childBTypeName);
		if (emittedOperations.contains(result))
			return result;

		CadpType.EmitType(binaryOperator.type());
		final ListType alist = (ListType)binaryOperator.type();
		final Type innerType = alist.innerType();
		final String resultTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.type().identifier());

		m_helperCode.AppendLine(String.format("%4$s %3$s(%1$s listA, %2$s listB){", childATypeName, childBTypeName, result, resultTypeName));
		m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
		m_helperCode.AppendLine(String.format("result.length = listA.length + listB.length;"));

		m_helperCode.AppendLine(String.format("if (result.length > %1$s) { printf(\"Concatenation result too long! %2$s\\n\"); abort();}", alist.maxNumberOfElements(), result));
		m_helperCode.AppendLine(String.format("memcpy(&result.elements[0],&listA.elements[0],listA.length * sizeof(%1$s));", CadpType.DumpType(innerType)));
		m_helperCode.AppendLine(String.format("memcpy(&result.elements[listA.length],&listB.elements[0],listB.length * sizeof(%1$s));", CadpType.DumpType(innerType)));
		m_helperCode.AppendLine(String.format("int counter;"));
		m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= (listA.length + listB.length); counter--) {", alist.maxNumberOfElements() - 1));
		m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
				CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));
		m_helperCode.AppendLine("return result; }");

		emittedOperations.add(result);
		return result;
	}

	@Override
	public  void visit(TernaryOperator ternaryOperator)
	{
		if (ternaryOperator.kind() == ExpressionKind.conditional)
		{
			m_emitter.Append("(");
			VisitSub(ternaryOperator.left(), ternaryOperator);
			m_emitter.Append(" ? ");

			VisitSub(ternaryOperator.mid(), ternaryOperator);
			m_emitter.Append(" : ");

			VisitSub(ternaryOperator.right(), ternaryOperator);
			m_emitter.Append(")");
		}
		else if (ternaryOperator.kind() == ExpressionKind.foldLR ||
				ternaryOperator.kind() == ExpressionKind.foldRL)
		{
			final CallExpression leftcall = (CallExpression)ternaryOperator.left();
			final Expression initializer = ternaryOperator.mid();
			final Expression listgetter = ternaryOperator.right();

			m_emitter.Append(String.format("fold_%1$s(%2$s", OoaCADPVisitor.getUIntHashCode(ternaryOperator), m_procInfo.stateVariableString));


			final CadpExpression cadpexpr = new CadpExpression(m_procInfo, emittedVariabes);
			leftcall.child().Accept(cadpexpr);
			final List<String> paramtypes = new ArrayList<String>();
			final List<String> parameters = new ArrayList<String>();
			for (int i = 0; i < leftcall.arguments().size() - 2; i++)
			{
				final Expression arg = leftcall.arguments().get(i);
				final CadpExpression paramexpr = new CadpExpression(m_procInfo, emittedVariabes);
				arg.Accept(paramexpr);
				m_emitter.Append(",");
				m_emitter.Append(paramexpr.toString());
			}

			final FunctionType fun = (FunctionType)leftcall.child().type();
			final FunctionIdentifier funid = (FunctionIdentifier) fun.identifier();
			final Iterator<Type> node = fun.parameter().iterator();
			for (int i = 0; i < fun.parameter().size() - 2; i++)
			{
				final Type nodeValue = node.next();
				paramtypes.add(CadpType.DumpType(nodeValue));
				final CadpIdentifier paramid = new CadpIdentifier(m_procInfo.stateVariableString);
				funid.parameter().get(i).Accept(paramid);
				parameters.add(paramid.toString());
			}

			m_emitter.Append(")");


			CadpType.EmitType(initializer.type());
			CadpType.EmitType(listgetter.type());
			final ListType thelist = (ListType)listgetter.type();
			CadpType.EmitType(thelist.innerType());
			final OoasCodeEmitter helper = new OoasCodeEmitter();
			helper.Append(String.format("%2$s fold_%1$s(CAESAR_TYPE_STATE oldState", OoaCADPVisitor.getUIntHashCode(ternaryOperator), CadpType.DumpType(leftcall.type())));
			if (paramtypes.size() > 0)
			{
				for (int i = 0; i < paramtypes.size(); i++)
				{
					helper.Append(",");
					helper.Append(paramtypes.get(i));
					helper.Append(" ");
					helper.Append(parameters.get(i));
				}
			}
			helper.AppendLine("){");

			helper.AppendLine(String.format("int __iterator;"));
			helper.AppendLine(String.format("%1$s param__result;", CadpType.DumpType(leftcall.type())));
			helper.AppendLine(String.format("%1$s __thelist;", CadpType.DumpType(listgetter.type())));
			helper.AppendLine(String.format("%1$s param__elem;", CadpType.DumpType(thelist.innerType())));

			final CadpActionInfo actionInfo = new CadpActionInfo(m_procInfo.action, -1, 0, m_procInfo.toDoListString, m_procInfo.doneListString, "oldState");

			final CadpExpression initvizcode = new CadpExpression(actionInfo, emittedVariabes);
			initializer.Accept(initvizcode);
			helper.AppendLine(initvizcode.VariableDeclarations());
			helper.AppendLine(String.format("param__result = %1$s;", initvizcode.toString()));

			final CadpExpression listgettercode = new CadpExpression(actionInfo, emittedVariabes);
			listgetter.Accept(listgettercode);
			helper.AppendLine(listgettercode.VariableDeclarations());
			helper.AppendLine(String.format("__thelist = %1$s;", listgettercode.toString()));

			final CadpExpression filtercall = new CadpExpression(actionInfo, emittedVariabes);
			leftcall.Accept(filtercall);
			helper.AppendLine(filtercall.VariableDeclarations());

			if (ternaryOperator.kind() == ExpressionKind.foldLR)
				helper.AppendLine(String.format("for (__iterator = 0; __iterator < __thelist.length; __iterator++) {"));
			else
				helper.AppendLine(String.format("for (__iterator = __thelist.length - 1; __iterator >= 0; __iterator--) {"));

			helper.AppendLine(String.format("param__elem = __thelist.elements[__iterator];"));
			helper.AppendLine(String.format("param__result = %1$s;", filtercall.toString()));


			helper.AppendLine("}");
			helper.AppendLine("return param__result;}");
			m_helperCode.Append(helper.toString());
		}
		else
			throw new UnsupportedOperationException();
	}

	@Override
	public  void visit(TupleMapAccessExpression tupleMapAccessExpression)
	{
		VisitSub(tupleMapAccessExpression.child(), tupleMapAccessExpression);
		if (tupleMapAccessExpression.child().type().kind() == TypeKind.TupleType)
		{
			// the access value needs to be a constant integer
			@SuppressWarnings("unchecked")
			final ValueExpression<Integer> accessValue = (ValueExpression<Integer>)tupleMapAccessExpression.argument();
			m_emitter.Append(String.format(".elem_%1$s", accessValue.value()));
		}
		else if (tupleMapAccessExpression.child().type().kind() == TypeKind.ListType)
		{
			m_emitter.Append(".elements[");
			VisitSub(tupleMapAccessExpression.argument(), tupleMapAccessExpression);
			m_emitter.Append("]");
		}
		else
			throw new UnsupportedOperationException();
	}
	@Override
	public  void visit(CallExpression callExpression)
	{
		/* this only supports calls to functions that return ONE value (deterministically) and do not change the state
		 * in a non-deterministic way
		 * ATTENTION: call-statements are treated in cadpstatement. this code only deals with calls within expressions!!
		 */

		final FunctionType funtype = (FunctionType)callExpression.child().type();
		if (funtype.returnType() == null)
			throw new IllegalArgumentException("Internal error: Function call in expression with return-type void!");

		/* create temp variable for result */
		final String tmpresult = String.format("detcallresult_%1$s", OoaCADPVisitor.getUIntHashCode(callExpression));
		final String tmpaftercallstates = String.format("callresult_%1$s", OoaCADPVisitor.getUIntHashCode(callExpression));

		varDecl.AppendLine(String.format("%1$s %2$s;", CadpType.DumpType(funtype.returnType()), tmpresult));
		varDecl.AppendLine(String.format("struct STATE_LIST * %1$s;", tmpaftercallstates));
		/* create call */
		final CadpExpression cadpexpr = new CadpExpression(m_procInfo, emittedVariabes);
		callExpression.child().Accept(cadpexpr);
		final String callstatement = cadpexpr.toString();
		varDecl.Append(cadpexpr.VariableDeclarations());
		m_usedIdentifier.addAll(cadpexpr.usedIdentifiers());
		final StringBuilder parameter = new StringBuilder(m_procInfo.stateVariableString);
		for (final Expression arg : callExpression.arguments())
		{
			parameter.append(", ");
			final CadpExpression paramexpr = new CadpExpression(m_procInfo, emittedVariabes);
			arg.Accept(paramexpr);
			parameter.append(paramexpr.toString());
		}
		parameter.append(String.format(", &(%1$s)", tmpresult));

		m_emitter.Append("(");
		m_emitter.Append(String.format("%3$s = %1$s(%2$s)", callstatement, parameter, tmpaftercallstates));
		m_emitter.Append(",");
		m_emitter.Append(String.format(" CALC_INVALID = %1$s == NULL ? (fprintf(stderr,\"call to %2$s returns NULL!\\n\"), 1) : (%1$s->next == NULL ? CALC_INVALID : (fprintf(stderr,\"call to %2$s non-deterministic!\\n\"), 1))", tmpaftercallstates, callstatement.replaceAll("\"", "'")));
		if (!funtype.isPureFunction())
		{
			m_emitter.Append(",");
			m_emitter.Append(String.format(" elem = %1$s == NULL ? elem : (list_insert_list(%2$s, %1$s),%1$s)", tmpaftercallstates, m_procInfo.doneListString));
		}
		m_emitter.Append(",");
		m_emitter.Append(String.format("%1$s", tmpresult));
		m_emitter.Append(")");
	}


	private interface IFilter<T> {
		boolean apply (T input); // poor man's anonymous function
	}

	private static <T> void removeAll(List<T> list, IFilter<T> filter) {
		int max;
		for (max = list.size() - 1; max >= 0; max --) {
			if (filter.apply(list.get(max)))
				list.remove(max);
		}
	}

	private List<Identifier> getListOfAccessedIdentifiers(CadpExpression child, final SymbolTable currentScopeSymbols)
	{
		final List<Identifier> importVars = new ArrayList<Identifier>(child.usedIdentifiers());
		if (currentScopeSymbols != null)
			removeAll(importVars, new IFilter<Identifier>(){
				@Override
				public boolean apply(Identifier input) {
					return currentScopeSymbols.symbolList().contains(input);
				}});

		removeAll(importVars, new IFilter<Identifier>(){
			@Override
			public boolean apply(Identifier input) {
				return input.kind() == IdentifierKind.AttributeIdentifier || // we pass the complete state..
				       input.kind() == IdentifierKind.EnumIdentifier ||      // constant
				       input.kind() == IdentifierKind.MethodIdentifier ||
				       input.kind() == IdentifierKind.NamedActionIdentifier;
			}
		});
		return importVars;
	}


	@Override
	public  void visit(ForallQuantifier quantifier)
	{
		final CadpActionInfo info = new CadpActionInfo(null, -1, -1, m_procInfo.toDoListString, m_procInfo.doneListString, "oldstate");
		final CadpExpression compExpr = new CadpExpression(info, emittedVariabes);
		quantifier.child().Accept(compExpr);

		// get a list of imported variabes
		final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, quantifier.symbols());

		final String functionName = String.format("forall_%1$s", OoaCADPVisitor.getUIntHashCode(quantifier));
		m_emitter.Append(String.format("1 == %1$s", functionName));
		m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
		for (final Identifier x : importVars)
		{
			m_emitter.Append(",");
			m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
		}
		m_emitter.Append(")");

		// emit helper
		final OoasCodeEmitter helper = new OoasCodeEmitter();
		helper.AppendLine(String.format("int %1$s(CAESAR_TYPE_STATE %2$s", functionName, "oldstate"));
		for (final Identifier x : importVars)
		{
			helper.Append(", ");
			helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
		}
		helper.AppendLine("){");

		helper.AppendLine(compExpr.VariableDeclarations());

		int loops = 0;
		for (final Identifier enumvar : quantifier.symbols().symbolList())
		{
			CadpType.EmitType(enumvar.type());
			helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
			helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
					CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));
			helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
					CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
			if (enumvar.type().kind() == TypeKind.OoActionSystemType)
			{
				// treat nulls - ignore them
				helper.AppendLine(String.format("if (memcmp(&%1$s, &%2$s, sizeof(%3$s)) == 0) continue;",
						CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetNullConstant((OoActionSystemType)enumvar.type()), CadpType.DumpType(enumvar.type())));
			}
			loops++;
		}

		helper.AppendLine(String.format("if (!("));
		helper.AppendLine(compExpr.toString());
		helper.AppendLine(String.format(") ) return 0;"));


		while (loops > 0)
		{
			helper.AppendLine("}");
			loops--;
		}
		helper.AppendLine("return 1; }");

		m_helperCode.Append(helper.toString());
	}

	@Override
	public  void visit(ExistsQuantifier quantifier)
	{
		final CadpActionInfo info = new CadpActionInfo(null, -1, -1, m_procInfo.toDoListString, m_procInfo.doneListString, "oldstate");
		final CadpExpression compExpr = new CadpExpression(info, emittedVariabes);
		quantifier.child().Accept(compExpr);

		// get a list of imported variabes
		final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, quantifier.symbols());

		final String functionName = String.format("exists_%1$s",  OoaCADPVisitor.getUIntHashCode(quantifier));
		m_emitter.Append(String.format("1 == %1$s", functionName));
		m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
		for (final Identifier x : importVars)
		{
			m_emitter.Append(",");
			m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
		}
		m_emitter.Append(")");

		// emit helper
		final OoasCodeEmitter helper = new OoasCodeEmitter();
		helper.Append(String.format("int %1$s(CAESAR_TYPE_STATE %2$s", functionName, "oldstate"));
		for (final Identifier x : importVars)
		{
			helper.Append(", ");
			helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
		}
		helper.AppendLine("){");

		helper.AppendLine(compExpr.VariableDeclarations());

		int loops = 0;
		for (final Identifier enumvar : quantifier.symbols().symbolList())
		{
			CadpType.EmitType(enumvar.type());
			helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
			helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
					CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));
			helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
					CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
			if (enumvar.type().kind() == TypeKind.OoActionSystemType)
			{
				// treat nulls - ignore them
				helper.AppendLine(String.format("if (memcmp(&%1$s, &%2$s, sizeof(%3$s)) == 0) continue;",
						CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetNullConstant((OoActionSystemType)enumvar.type()), CadpType.DumpType(enumvar.type())));
			}
			loops++;
		}

		helper.AppendLine(String.format("if (("));
		helper.AppendLine(compExpr.toString());
		helper.AppendLine(String.format(") ) return 1;"));


		while (loops > 0)
		{
			helper.AppendLine("}");
			loops--;
		}
		helper.AppendLine("return 0; }");

		m_helperCode.Append(helper.toString());
	}

	private static final class RefBool {
		boolean value = false;
	}

	@Override
	public  void visit(UnaryOperator unaryOperator)
	{
		switch (unaryOperator.kind())
		{
		case tail:
			final String tail = EmitTailOperation(unaryOperator);
			m_emitter.Append(String.format("%1$s(", tail));
			VisitSub(unaryOperator.child(), unaryOperator);
			m_emitter.Append(")");
			break;
		case head:
			m_emitter.Append("(");
			VisitSub(unaryOperator.child(), unaryOperator);
			m_emitter.Append(String.format(").elements[0]"));
			break;
		case len:
			m_emitter.Append("(");
			VisitSub(unaryOperator.child(), unaryOperator);
			m_emitter.Append(String.format(").length"));
			break;
		case Cast:
			m_emitter.Append("/*cast*/");
			final RefBool doSub = new RefBool();
			final String cast = EmitCastOperation(unaryOperator, /*out*/ doSub);
			if (doSub.value)
			{
				m_emitter.Append(String.format("(%1$s(", cast));
				VisitSub(unaryOperator.child(), unaryOperator);
				m_emitter.Append("))");
			}
			break;
		default:
			m_emitter.Append(" ");
			m_emitter.Append(OperatorString(unaryOperator));
			m_emitter.Append("(");
			VisitSub(unaryOperator.child(), unaryOperator);
			m_emitter.Append(")");
			break;
		}
	}

	/* The cast support in this target instanceof limited: We can not cast differently sized types!
	 * Hence list and map lengths must be equal.
	 * */
	private boolean CADPCastEquivalent(Type type1, Type type2)
	{
		if ((type1 == null) || (type2 == null))
			return false;

		final TypeKind tk1 = type1.kind();
		final TypeKind tk2 = type2.kind();

		// if of different kind, then return false..
		if (tk1 != tk2)
			return false;

		// if same kind, make a rigorous check
		switch (tk1)
		{
		case IntType:
			return true; // we don't care about the range, since all ints are 32bit wide, which is the max that can be defined in OOAS
		case BoolType:
			return true;
		case FloatType:
			throw new UnsupportedOperationException(); // float type instanceof not used. other than that, we could return true
		case EnumeratedType:
			return type1 == type2; // reference equals!
		case ListType:
			final ListType listt1 = (ListType)type1;
			final ListType listt2 = (ListType)type2;
			return CADPCastEquivalent(listt1.innerType(), listt2.innerType()) &&
					listt1.maxNumberOfElements() == listt2.maxNumberOfElements();
		case MapType:
			final MapType mapt1 = (MapType)type1;
			final MapType mapt2 = (MapType)type2;
			return CADPCastEquivalent(mapt1.fromType(), mapt2.fromType()) &&
					CADPCastEquivalent(mapt1.toType(), mapt2.toType()) &&
					mapt1.maxNumberOfElements() == mapt2.maxNumberOfElements();
		case TupleType:
			final TupleType tuplet1 = (TupleType)type1;
			final TupleType tuplet2 = (TupleType)type2;
			if (tuplet1.innerTypes().size() != tuplet2.innerTypes().size())
				return false;
			final Iterator<Type> innert1 = tuplet1.innerTypes().iterator();
			final Iterator<Type> innert2 = tuplet2.innerTypes().iterator();
			while (innert1.hasNext())
			{
				final Type innert1Value = innert1.next();
				final Type innert2Value = innert2.next();

				if (!CADPCastEquivalent(innert1Value, innert2Value))
					return false;
			}
			return true;
		case OoActionSystemType:
			return type1 == type2 /*ref. eq.*/ ||
					Type.Covariance((OoActionSystemType)type2, (OoActionSystemType)type1);
		case OpaqueType:
			throw new IllegalArgumentException();
		case Null:
		case Any:
			return true;
		default:
			throw new UnsupportedOperationException();
		}
	}


	private String EmitCastOperation(UnaryOperator unaryOperator, /*out*/ RefBool doSub)
	{
		doSub.value = true;
		if (unaryOperator.child().kind() == ExpressionKind.ListConstr &&
				((ListConstructor)unaryOperator.child()).hasComprehension())
		{
			// we get a malloced list an have to cut it down
			final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
			final String resultTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
			final String result = String.format("op_cast_malloc_%1$s_%2$s", childTypeName, resultTypeName);

			if (emittedOperations.contains(result))
				return result;

			// emit target type
			CadpType.EmitType(unaryOperator.type());

			switch (unaryOperator.type().kind())
			{
			case ListType:
				final ListType toType = (ListType)unaryOperator.type();
				final ListType fromType = (ListType)unaryOperator.child().type();
				final String listStruct = String.format("struct struct_list_%1$s", CadpType.DumpType(fromType.innerType()).replaceAll(" ", "_"));

				if (!(fromType.innerType().kind() == TypeKind.Null || CADPCastEquivalent(fromType.innerType(), toType.innerType())))
					throw new UnsupportedOperationException(String.format("CADP Target does not support this type of cast: '%1$s' to '%2$s'", fromType.innerType().toString(), toType.innerType().toString()));
				m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s *toCast){", listStruct, result, resultTypeName));
				m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
				m_helperCode.AppendLine(String.format("%1$s *tmp = toCast;", listStruct));
				m_helperCode.AppendLine(String.format("int len = 0;"));
				m_helperCode.AppendLine(String.format("result.length = 0;"));

				m_helperCode.AppendLine("while (toCast != NULL)");
				m_helperCode.AppendLine("{");
				m_helperCode.AppendLine(String.format("    if (len < %1$s)", toType.maxNumberOfElements()));
				m_helperCode.AppendLine("    {");
				m_helperCode.AppendLine(String.format("memcpy(&result.elements[len],&(toCast->element),sizeof(%1$s));", CadpType.DumpType(toType.innerType())));
				m_helperCode.AppendLine(String.format("result.length = len+1;"));
				m_helperCode.AppendLine("    }");
				m_helperCode.AppendLine("    else ");
				m_helperCode.AppendLine("        CALC_INVALID = 1;");
				m_helperCode.AppendLine("    len++;");
				m_helperCode.AppendLine("    tmp = toCast->next;");
				m_helperCode.AppendLine("    free(toCast);");
				m_helperCode.AppendLine("    toCast = tmp;");
				m_helperCode.AppendLine("}");
				m_helperCode.AppendLine("    if (CALC_INVALID == 1)");
				m_helperCode.AppendLine(String.format("        printf(\"\\n\\nCalculation invalid: Cast to smaller list in %1$s\\n\\n\");", result));


				m_helperCode.AppendLine(String.format("int counter;"));
				m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", toType.maxNumberOfElements() - 1));
				m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
						CadpType.enumString, CadpIdentifier.GetIdentifierString(toType.innerType().identifier()), CadpType.lowString));
				m_helperCode.AppendLine("return result; }");


				break;
			default:
				// no cast
				return "";
			}
			emittedOperations.add(result);
			return result;


		}
		else
		{
			final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
			final String resultTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
			final String result = String.format("op_cast_%1$s_%2$s", childTypeName, resultTypeName);

			if (emittedOperations.contains(result))
				return result;

			// emit target type
			CadpType.EmitType(unaryOperator.type());

			switch (unaryOperator.type().kind())
			{
			case ListType:
				final ListType toType = (ListType)unaryOperator.type();
				final ListType fromType = (ListType)unaryOperator.child().type();
				if (!(fromType.innerType().kind() == TypeKind.Null || CADPCastEquivalent(fromType.innerType(), toType.innerType())))
					throw new UnsupportedOperationException(String.format("CADP Target does not support this type of cast: '%1$s' to '%2$s'", fromType.innerType().toString(), toType.innerType().toString()));
				m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s toCast){", childTypeName, result, resultTypeName));
				m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
				m_helperCode.AppendLine(String.format("if (toCast.length > %1$s) { printf(\"Cast to smaller list! %2$s\\n\"); ", toType.maxNumberOfElements(), result));
				m_helperCode.AppendLine(String.format("%1$s%2$s(stdout, toCast); fflush(stdout); CALC_INVALID=1; result.length = %3$s;} else", CadpType.printString, childTypeName, toType.maxNumberOfElements()));
				m_helperCode.AppendLine(String.format("result.length = toCast.length;"));
				m_helperCode.AppendLine(String.format("if (result.length > 0)"));
				m_helperCode.AppendLine(String.format("memcpy(result.elements,toCast.elements,result.length * sizeof(%1$s));", CadpType.DumpType(toType.innerType())));
				m_helperCode.AppendLine(String.format("int counter;"));
				m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", toType.maxNumberOfElements() - 1));
				m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
						CadpType.enumString, CadpIdentifier.GetIdentifierString(toType.innerType().identifier()), CadpType.lowString));
				m_helperCode.AppendLine("return result; }");


				break;
			case OoActionSystemType:
				if (unaryOperator.child().kind() == ExpressionKind.Value &&
				(unaryOperator.child() instanceof ValueExpression<?>) &&
				((ValueExpression<?>)unaryOperator.child()).value() == null)
				{
					m_emitter.Append(String.format("NULL_%1$s", CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier())));
					doSub.value = false;
				}
				else
				{
					doSub.value = true;
					final CadpType targetType = new CadpType();
					unaryOperator.type().Accept(targetType);
					final CadpType sourceType = new CadpType();
					unaryOperator.child().type().Accept(sourceType);
					if (!(Type.Covariance((OoActionSystemType)unaryOperator.child().type(), (OoActionSystemType)unaryOperator.type())))
					{
						// cast result type (unaryOperator.type) not a sub-type of unaryOperator.child.type
						return String.format("/* up-cast: %1$s as %2$s */ *(%2$s*)&", sourceType.ToString(), targetType.ToString());
					}
					else
					{
						return String.format(" /* down-cast: %1$s as %2$s */ *(%2$s*)&", sourceType.ToString(), targetType.ToString());
					}

				}
				return "";
			default:
				// no cast
				return "";
			}
			emittedOperations.add(result);
			return result;
		}
	}

	private String EmitTailOperation(UnaryOperator unaryOperator)
	{
		final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
		final String result = String.format("op_tail_%1$s", childTypeName);
		if (emittedOperations.contains(result))
			return result;

		final ListType alist = (ListType)unaryOperator.child().type();
		CadpType.EmitType(unaryOperator.type());
		final String resultType = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
		final ListType resultList = (ListType)unaryOperator.type();

		// -- tail constructor
		m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s toCopy){", childTypeName, result, resultType));
		m_helperCode.AppendLine(String.format("%1$s result;", resultType));
		m_helperCode.AppendLine(String.format("if (toCopy.length == 0) { printf(\"Tail from empty list! %1$s\\n\"); abort();}", childTypeName));
		m_helperCode.AppendLine(String.format("result.length = toCopy.length - 1;"));
		m_helperCode.AppendLine(String.format("if (result.length == 0)"));
		m_helperCode.AppendLine(String.format("memset(&result,0,sizeof(%1$s));", resultType));
		m_helperCode.AppendLine(String.format("else"));
		m_helperCode.AppendLine(String.format("memcpy(&result.elements[0],&toCopy.elements[1],result.length * sizeof(%1$s));", CadpType.DumpType(alist.innerType()), alist.maxNumberOfElements() - 1));

		// in case our resulttype was set wider..
		m_helperCode.AppendLine(String.format("int counter;"));
		m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", resultList.maxNumberOfElements() - 1));
		m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
				CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));


		m_helperCode.AppendLine("return result; }");


		emittedOperations.add(result);
		return result;
	}

	public String VariableDeclarations()
	{
		return varDecl.toString();
	}

	@Override
	public  String toString()
	{
		return m_emitter.toString();
	}

	public static String GetHelperCode()
	{
		final StringBuilder result = new StringBuilder(m_helperCode.toString());
		result.append("void Model_Reset() {");
		result.append(System.lineSeparator());
		result.append(m_resetCode.toString());
		result.append("}");
		result.append(System.lineSeparator());
		return result.toString();
	}

	public CadpExpression(CadpActionInfo aProcInfo)
	{
		if (aProcInfo == null)
			throw new IllegalArgumentException();
		m_procInfo = aProcInfo;
	}


	public CadpExpression(CadpActionInfo aProcInfo, HashSet<Identifier> varDecls)
	{
		if (aProcInfo == null)
			throw new IllegalArgumentException();
		m_procInfo = aProcInfo;
		emittedVariabes.addAll(varDecls);
	}
}