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

import java.util.ArrayList;

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.identifiers.EnumIdentifier;
import org.momut.ooas.ast.identifiers.Identifier;
import org.momut.ooas.ast.identifiers.IdentifierKind;
import org.momut.ooas.ast.types.EnumType;
import org.momut.ooas.ast.types.FunctionType;
import org.momut.ooas.ast.types.MetaType;
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.codegen.OoasCodeEmitter;
import org.momut.ooas.utils.exceptions.ArgumentException;
import org.momut.ooas.utils.exceptions.NotImplementedException;
import org.momut.ooas.visitors.OoaExpressionVisitor;

public class OoaPrologExpression extends OoaExpressionVisitor
{
	public static class Factory
	{
		public final OoaPrologExpression create(OoaPrologIdentifier.Factory idFactory, OoaPrologType.Factory typeFactory, Scratchbook sb)
		{ return create(idFactory, typeFactory, sb, false); }
		public OoaPrologExpression create(OoaPrologIdentifier.Factory idFactory, OoaPrologType.Factory typeFactory, Scratchbook sb, boolean lhs)
		{ return new OoaPrologExpression(idFactory, typeFactory, sb, this, lhs); }
	}

	protected OoasCodeEmitter m_emitter = new OoasCodeEmitter();
	protected ArrayList<String> m_tmpVars = new ArrayList<String>();
	protected final Scratchbook m_scratchbook;
	private boolean m_LhsExpression = false;


	public ArrayList<String> tmpVariables() { return m_tmpVars; }
	public boolean isLhsExpression() { return m_LhsExpression; }

//	private String GetPrologType(UlyssesType aType)
//	{
//		OoaPrologType pType = createTypeVisitor();
//		aType.Accept(pType);
//		return pType.toString();
//	}

	protected String GetIdentifierString(Identifier anIdentifier)
	{
		final OoaPrologIdentifier pIdent = createIdentifierVisitor();
		anIdentifier.Accept(pIdent);
		return pIdent.toString();
	}


	// following call must not happen
	@Override
	public void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)
	{
		assert(false);
	}

	// call of method that returns a value..
	@Override
	public void visit(CallExpression callExpression)
	{
		// we handle only function calls within expressions here (must have non-void return!)
		final FunctionType funtype = (FunctionType)callExpression.child().type();
		if (funtype.returnType() == null)
			throw new ArgumentException("Internal error: Function call in expression with return-type void!");

		String callstatement = "";
		final StringBuilder parameter = new StringBuilder();

		final OoaPrologExpression prologexpr = createExpressionVisitor();
		callExpression.child().Accept(prologexpr);

		m_emitter.Append(prologexpr.toString());
		callstatement = prologexpr.tmpVariables().get(0);
		int i = 0;
		for (final Expression arg: callExpression.arguments())
		{
			if (i != 0)
				parameter.append(", ");
			else
				i++;
			final OoaPrologExpression paramexpr = createExpressionVisitor();
			arg.Accept(paramexpr);
			m_emitter.Append(paramexpr.toString());
			parameter.append(paramexpr.tmpVariables().get(0));
		}
		if (parameter.length() > 0)
			m_emitter.AppendLine(String.format("%s(%s,%s),", callstatement, parameter, NewTempVariable()));
		else
			m_emitter.AppendLine(String.format("%s(%s),", callstatement, NewTempVariable()));
	}


	// we need to map all other things to Prolog constructs
	private String OperatorString(Expression expression, Type resultingType)
	{
		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 head:   // T_HEAD:
		case tail:   // T_TAIL:
		case conc:   // T_CONC:
		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 diff:   // T_DIFF:
		case munion: // T_MUNION:
		case seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:
		case subset:
		case elemin:
		case notelemin:
		case implies:    // T_IMPLIES:
		case biimplies:  // T_BIIMPLIES:
		case Primed:
		case len:    // T_LEN:
			throw new NotImplementedException();

		case div:    // T_DIV:
			return "/";
		case idiv:   // T_IDIV:
			return "/";
		case mod:    // T_MOD:
			return "mod";
		case prod:   // T_PROD:
			return "*";
		case sum:    // T_SUM:
			return "+";
		case minus:  // T_MINUS:
			return "-";
		case less:
			return !isNumericBinary(expression) ? "<" : "#<";
		case lessequal:
			return !isNumericBinary(expression) ? "=<" : "#=<";
		case greater:
			return !isNumericBinary(expression) ? ">" : "#>";
		case greaterequal:
			return !isNumericBinary(expression) ? ">=" : "#>=";
		case equal:
			return !isNumericBinary(expression) ? "==" : "#=";
		case notequal:
			return !isNumericBinary(expression) ? "\\=" : "#\\=";
		case and:    // T_AND:
			throw new NotImplementedException(); // implemented in binaryoperator
		case or:     // T_OR:
			throw new NotImplementedException(); // implemented in binaryoperator
		case not:
			throw new NotImplementedException(); // implemented in binaryoperator

		case Cast:
			return "";

		default:
			return expression.kind().name(); //Enum.GetName(typeof(ExpressionKind), expression.kind);
		}
	}

	protected boolean isNumericBinary(Expression expression)
	{
		boolean result = false;
		if (expression instanceof BinaryOperator)
		{
			result = ((BinaryOperator)expression).left().type().kind() == TypeKind.IntType &&
					((BinaryOperator)expression).right().type().kind() == TypeKind.IntType;
		}
		else if (expression instanceof UnaryOperator)
		{
			result = ((UnaryOperator)expression).child().type().kind() == TypeKind.IntType;
		}
		else throw new NotImplementedException();
		return result;
	}

	@SuppressWarnings("unchecked")
	@Override
	public <T> void visit(ValueExpression<T> valueExpression)
	{
		assert(m_tmpVars.size() == 0);
		final String tmpVar = NewTempVariable();
		m_emitter.Append(String.format("%s ", tmpVar));


		if (valueExpression.value() == null)
			m_emitter.Append("= 'null'");
		else if (Boolean.class.isAssignableFrom(valueExpression.m_clazz))
			m_emitter.Append(((ValueExpression<Boolean>) valueExpression).value() ? " #= true" : " #= fail");
		else if (Character.class.isAssignableFrom(valueExpression.m_clazz))
			m_emitter.Append(String.format("#= '%s'", valueExpression.toString()));
		else if (Integer.class.isAssignableFrom(valueExpression.m_clazz))
			m_emitter.Append(String.format("#= %s", valueExpression.toString()));
		else
			m_emitter.Append(String.format("= %s", valueExpression.value().toString()));

		m_emitter.AppendLine(",");
		assert(m_tmpVars.size() == 1);
	}

	@Override
	public void visit(IdentifierExpression identifierExpression)
	{
		if (identifierExpression.identifier().kind() == IdentifierKind.EnumIdentifier)
		{
			final EnumIdentifier enumid = (EnumIdentifier)identifierExpression.identifier();
			final EnumType enumType = (EnumType)enumid.type();
			//m_emitter.Append(enumType.listOfEnumSymbols.IndexOf(enumid));
			if (enumType instanceof ValuedEnumType)
				m_emitter.AppendLine(String.format("%s #= %s,", NewTempVariable(), enumid.Value()));
			else
				m_emitter.AppendLine(String.format("%s #= %s,", NewTempVariable(), enumType.listOfEnumSymbols().indexOf(enumid)));
		}
		else if (identifierExpression.isSelf())
		{
			m_emitter.AppendLine(String.format("%s = %s,", NewTempVariable(), GetIdentifierString(identifierExpression.identifier())));
		}
		/*else if (identifierExpression.identifier.kind == IdentifierKind.AttributeIdentifier)
		{
			m_emitter.AppendLine(String.format("getVal(%s,%s,_),", GetIdentifierString(identifierExpression.identifier), NewTempVariable(), ));
		}*/
		else
		{
			m_tmpVars.add(GetIdentifierString(identifierExpression.identifier()));
		}
	}

	@Override
	public void visit(TypeExpression typeExpression)
	{
		if (typeExpression.referredType().kind() != TypeKind.EnumeratedType)
		{
			m_emitter.Append(GetIdentifierString(typeExpression.referredType().identifier()));
		}
	}


	@Override
	public void visit(ObjectConstructor objectConstructor)
	{
		if (objectConstructor.instances().size() > 1)
			throw new NotImplementedException();

		m_emitter.AppendLine(String.format("%s = '%s',", NewTempVariable(), objectConstructor.instances().get(0).Name));

		//m_emitter.Append(String.format("new %s(this)", GetIdentifierString(objectConstructor.type.identifier)));
	}

	@Override
	public void visit(ListConstructor listConstructor)
	{
		if (listConstructor.hasComprehension())
		{
			final OoaPrologExpression compr = createExpressionVisitor();
			listConstructor.comprehension().Accept(compr);
			final OoaPrologExpression elem = createExpressionVisitor();
			listConstructor.elements().get(0).Accept(elem);

			final StringBuilder enumvars = new StringBuilder();
			int i = 0;
			for (final Identifier v: listConstructor.comprehensionVariables().symbolList())
			{
				final OoaPrologIdentifier ident = createIdentifierVisitor();
				v.Accept(ident);

				final OoaPrologType identType = createTypeVisitor();
				v.type().Accept(identType);

				enumvars.append(String.format("%s %s: %s", i == 0 ? "" : ",", ident.toString(), identType.toString()));
				i++;
			}

			m_emitter.AppendLine("% listcomprehension");
			m_emitter.AppendLine(String.format("%s = {%s:[%s]:(%s%s,%s%s)}",
					NewTempVariable(), elem.tmpVariables().get(0), enumvars.toString(), compr.toString(), compr.tmpVariables().get(0),
					elem.toString(), "1=1" /*elem.ToString() == String.Empty ? "1=1" : elem.tmpVariables[0]*/));
		}
		else
		{
			m_emitter.AppendLine("% make list");
			m_emitter.AppendLine(String.format("%s = []", NewTempVariable()));

			for (final Expression expr: listConstructor.elements())
			{
				m_emitter.Append(", ");

				final OoaPrologExpression pVal = createExpressionVisitor();
				expr.Accept(pVal);
				m_emitter.Append(pVal.toString());
				assert(pVal.tmpVariables().size() == 1);
				m_emitter.AppendLine(String.format("ulyssesListConc(%s,[%s],%s)", m_tmpVars.get(0), pVal.tmpVariables().get(0), NewTempVariable()));
				m_tmpVars.remove(0);
			}
		}
		m_emitter.Append(",");
		assert(m_tmpVars.size() == 1);
	}

	@Override
	public void visit(SetConstructor setConstructor)
	{
		m_emitter.AppendLine("% make set");
		// our resulting set.
		m_emitter.AppendLine(String.format("%s = []", NewTempVariable()));

		for (final Expression expr: setConstructor.items())
		{
			m_emitter.Append(", ");

			final OoaPrologExpression pVal = createExpressionVisitor();
			expr.Accept(pVal);
			m_emitter.Append(pVal.toString());
			assert(pVal.tmpVariables().size() == 1);
			m_emitter.AppendLine(String.format("ulyssesListConc(%s,[%s],%s)", m_tmpVars.get(0), pVal.tmpVariables().get(0), NewTempVariable()));
			m_tmpVars.remove(0);
		}
		m_emitter.Append(",");
		assert(m_tmpVars.size() == 1);
	}

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

	@Override
	public void visit(TupleConstructor tupleConstructor)
	{
		if (tupleConstructor.isMatcher())
		{
			// being dealt with in binaryoperator (since we only allow tuple=MyTuple(a,b))
			NewTempVariable();
			return;
		}
		else
		{
			m_emitter.AppendLine("% make tuple");
			m_emitter.AppendLine(String.format("%s = []", NewTempVariable()));

			for (final Expression expr: tupleConstructor.values())
			{
				m_emitter.Append(", ");

				final OoaPrologExpression pVal = createExpressionVisitor();
				expr.Accept(pVal);
				m_emitter.Append(pVal.toString());
				assert(pVal.tmpVariables().size() == 1);
				m_emitter.AppendLine(String.format("ulyssesListConc(%s,[%s],%s)", m_tmpVars.get(0), pVal.tmpVariables().get(0), NewTempVariable()));
				m_tmpVars.remove(0);
			}
			m_emitter.Append(",");
			assert(m_tmpVars.size() == 1);
		}
	}

	@Override
	public void visit(AccessExpression accessExpression)
	{
		if (!(accessExpression.left().type().kind() == TypeKind.MetaType && ((MetaType)accessExpression.left().type()).Type().kind() == TypeKind.EnumeratedType ) &&
		    !(accessExpression.right().kind() == ExpressionKind.Identifier &&
		    ((IdentifierExpression)accessExpression.right()).identifier().kind() == IdentifierKind.AttributeIdentifier))
		{
			assert(m_tmpVars.size() == 0);
			// enums and qr types are directly (statically) converted to nums...
			VisitSub(accessExpression.left(), accessExpression);
			final String leftresult = m_tmpVars.get(0); m_tmpVars.remove(0);

			VisitSub(accessExpression.right(), accessExpression);
			final String rightresult = m_tmpVars.get(0); m_tmpVars.remove(0);

			m_tmpVars.add(String.format("%s\\%s", leftresult, rightresult));
		}
		else
			VisitSub(accessExpression.right(), accessExpression);
	}

	@Override
	public void visit(BinaryOperator binaryOperator)
	{
		final OoasCodeEmitter origEmitter = m_emitter;


		// eval stack must be empty
		assert(m_tmpVars.size() == 0);
		// traverse left
		final OoasCodeEmitter leftcode = new OoasCodeEmitter();
		m_emitter = leftcode;
		VisitSub(binaryOperator.left(), binaryOperator);
		final String leftresult = m_tmpVars.get(0); m_tmpVars.remove(0);
		assert(m_tmpVars.size() == 0);
		// traverse right
		final OoasCodeEmitter rightcode = new OoasCodeEmitter();
		m_emitter = rightcode;
		VisitSub(binaryOperator.right(), binaryOperator);
		final String rightresult = m_tmpVars.get(0); m_tmpVars.remove(0);
		// eval stack must be empty
		assert(m_tmpVars.size() == 0);

		m_emitter = origEmitter;

		// get tmp.var
		final String tmpVar = NewTempVariable();

		switch (binaryOperator.kind())
		{
		case elemin:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			m_emitter.AppendLine(String.format(" %s = member(%s,%s),",
					tmpVar, leftresult, rightresult));
			break;
		case and:    // T_AND:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			m_emitter.AppendLine(String.format(" %s = (%s %s %s), ",
					tmpVar, leftresult, ",", rightresult));
			break;
		case or:     // T_OR:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			m_emitter.AppendLine(String.format(" %s = (%s %s %s), ",
					tmpVar, leftresult, ";", rightresult));
			break;

		case implies:
			m_emitter.Append(leftcode.toString());
			m_emitter.AppendLine(String.format(" %s = (%s -> (%s%s); true), ", // {0} = (({1} -> ({2}{3}); true))
					tmpVar, leftresult, rightcode.toString(), rightresult));
			break;

		case equal:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			/*check if we have tupleconstructors as matchers*/
			TupleConstructor matcher = null;
			String aTuple = null;
			if (binaryOperator.left().kind() == ExpressionKind.TupleConstr &&
					((TupleConstructor)binaryOperator.left()).isMatcher())
			{
				matcher = (TupleConstructor)binaryOperator.left();
				aTuple = rightresult;
			}
			else if (binaryOperator.right().kind() == ExpressionKind.TupleConstr &&
					((TupleConstructor)binaryOperator.right()).isMatcher())
			{
				matcher = (TupleConstructor)binaryOperator.right();
				aTuple = leftresult;
			}

			if (matcher == null)
				m_emitter.AppendLine(String.format(" %s = (%s %s %s), ",
				tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left().type()), rightresult));
			else
			{
				m_emitter.Append(String.format("%s = unify(%s = [", tmpVar, aTuple));
				int cntr = 0;
				for(final Expression x: matcher.values())
				{
					if (cntr != 0)
						m_emitter.Append(", ");
					else
						cntr++;

					if (x.kind() != ExpressionKind.Identifier)
						throw new ArgumentException();

					final IdentifierExpression ident = (IdentifierExpression)x;
					final OoaPrologIdentifier avisitor = createIdentifierVisitor();
					ident.Accept(avisitor);
					m_emitter.Append(avisitor.toString());
				}
				m_emitter.AppendLine("]),");
			}
			break;



		case conc:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			m_emitter.AppendLine(String.format("ulyssesListConc(%s,%s,%s),", leftresult, rightresult, tmpVar));
			break;

		default:
			m_emitter.Append(leftcode.toString());
			m_emitter.Append(rightcode.toString());
			//m_emitter.Append("(");
			if (binaryOperator.type().kind() == TypeKind.IntType)
				m_emitter.AppendLine(String.format(" %s #= (%s %s %s), ",
						tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left().type()), rightresult));
			else
				m_emitter.AppendLine(String.format(" %s = (%s %s %s), ",
						tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left().type()), rightresult));
			//m_emitter.Append(")");
			break;
		}
		assert(m_tmpVars.size() == 1);
	}

	@Override
	public void visit(TernaryOperator ternaryOperator)
	{
		if (ternaryOperator.kind() == ExpressionKind.conditional)
		{
			VisitSub(ternaryOperator.left(), ternaryOperator);
			final String leftresult = m_tmpVars.get(0); m_tmpVars.remove(0);
			VisitSub(ternaryOperator.mid(), ternaryOperator);
			final String midresult = m_tmpVars.get(0); m_tmpVars.remove(0);
			VisitSub(ternaryOperator.right(), ternaryOperator);
			final String rightresult = m_tmpVars.get(0); m_tmpVars.remove(0);

			final String varname = NewTempVariable();

			// (cond, expr #= var; #\ (cond), expr #= var)
			m_emitter.Append("((");
			m_emitter.Append(leftresult);
			m_emitter.Append(", unify(");
			m_emitter.Append(midresult);
			m_emitter.Append(String.format(" = %s) );( call(\\+(%s)), unify(", varname, leftresult));
			m_emitter.Append(rightresult);
			m_emitter.Append(String.format(" = %s) )),", varname));
		}
		else if (ternaryOperator.kind() == ExpressionKind.foldRL)
			throw new NotImplementedException();
		else if (ternaryOperator.kind() == ExpressionKind.foldLR)
		{
			VisitSub(ternaryOperator.mid(), ternaryOperator);
			final String midresult = m_tmpVars.get(0); m_tmpVars.remove(0);
			VisitSub(ternaryOperator.right(), ternaryOperator);
			final String rightresult = m_tmpVars.get(0); m_tmpVars.remove(0);


			// make vars unique
			final int uniqueNumer = GetUniqueNumber();
			final CallExpression leftcall = (CallExpression)ternaryOperator.left();
			final IdentifierExpression elemId = (IdentifierExpression)leftcall.arguments().get(leftcall.arguments().size() - 1);
			elemId.identifier().SetTokenText(String.format("Elem_%s", uniqueNumer));
			final IdentifierExpression currentResultId = (IdentifierExpression)leftcall.arguments().get(leftcall.arguments().size() - 2);
			currentResultId.identifier().SetTokenText(String.format("In_%s", uniqueNumer));

			final String elemVarName = GetIdentifierString(elemId.identifier());
			final String inVarName = GetIdentifierString(currentResultId.identifier());

			m_emitter.Append(String.format("fun_fold(%s,%s,(%s, %s, Out_%s,(",
					midresult, rightresult, elemVarName, inVarName, uniqueNumer));
			VisitSub(leftcall, ternaryOperator);
			final String leftresult = m_tmpVars.get(0); m_tmpVars.remove(0);
			final String tmpresult = NewTempVariable();
			m_emitter.Append(String.format(" Out_%s = %s)),%s),", uniqueNumer, leftresult, tmpresult));
		}

		else
			throw new NotImplementedException();
	}

	@Override
	public void visit(TupleMapAccessExpression tupleMapAccessExpression)
	{
		assert(m_tmpVars.size() == 0);
		VisitSub(tupleMapAccessExpression.child(), tupleMapAccessExpression);
		final String childresult = m_tmpVars.get(0); m_tmpVars.remove(0);

		VisitSub(tupleMapAccessExpression.argument(), tupleMapAccessExpression);
		final String accessresult = m_tmpVars.get(0); m_tmpVars.remove(0);
		assert(m_tmpVars.size() == 0);

		final String tmpresult = NewTempVariable();

		if (!m_LhsExpression)
		{
			switch (tupleMapAccessExpression.child().type().kind())
			{
			case TupleType:
				m_emitter.AppendLine(String.format("ulyssesTupleAccess(%s,%s,%s),", childresult, accessresult, tmpresult));
				break;
			case MapType:
				m_emitter.AppendLine(String.format("ulyssesMapAccess(%s,%s,%s),", childresult, accessresult, tmpresult));
				break;
			case ListType:
				m_emitter.AppendLine(String.format("ulyssesListAccess(%s,%s,%s),", childresult, accessresult, tmpresult));
				break;
			default:
				throw new NotImplementedException();
			}
			assert(m_tmpVars.size() == 1);
		}
		else
		{
			/*>>>>> See comment in ooaTypeCheckVisitor on method CheckPlace! <<<<<<<<<*/
			switch (tupleMapAccessExpression.child().type().kind())
			{
			case ListType:
				boolean isAttribute;
				isAttribute = tupleMapAccessExpression.child().kind() == ExpressionKind.Identifier &&
						((IdentifierExpression)tupleMapAccessExpression.child()).identifier().kind() == IdentifierKind.AttributeIdentifier;

				isAttribute = isAttribute || tupleMapAccessExpression.child().kind() == ExpressionKind.Access
						&& ((AccessExpression)tupleMapAccessExpression.child()).left().kind() == ExpressionKind.Identifier
						&& ((IdentifierExpression)((AccessExpression)tupleMapAccessExpression.child()).left()).isSelf()
						&& ((AccessExpression)tupleMapAccessExpression.child()).right().kind() == ExpressionKind.Identifier
						&& ((IdentifierExpression)((AccessExpression)tupleMapAccessExpression.child()).right()).identifier().kind()
						== IdentifierKind.AttributeIdentifier;


				final String newlist = String.format("RESVAR_%s", m_scratchbook.getNewTmpVarCntrValue());

				m_emitter.AppendLine(String.format("ulyssesListWrite(%s,%s,%s,%s),", childresult, accessresult, tmpresult, newlist));

				if (isAttribute)
				{ m_emitter.AppendLine(String.format("%s := %s,", childresult, newlist)); }
				else
				{ throw new NotImplementedException(); }

				break;
			default:
				throw new NotImplementedException();
			}


		}
	}


	@Override
	public void visit(ForallQuantifier quantifier)
	{
		final OoaPrologExpression pExpr = createExpressionVisitor();
		quantifier.child().Accept(pExpr);

		// TEMPXY = forall(enumerate1([var:type,...]),pred(var..))
		final StringBuilder Generator = new StringBuilder();
		final StringBuilder nullGuard = new StringBuilder();
		int i = 0;
		for (final Identifier v: quantifier.symbols().symbolList())
		{
			final OoaPrologIdentifier ident = createIdentifierVisitor();
			v.Accept(ident);

			final OoaPrologType identType = createTypeVisitor();
			v.type().Accept(identType);

			Generator.append(String.format("%s %s: %s", i == 0 ? "" : ",", ident.toString(), identType.toString()));
			if (v.type().kind() == TypeKind.OoActionSystemType)
				nullGuard.append(String.format("(%s == null) ; ", ident.toString()));
			i++;
		}

		m_emitter.AppendLine(String.format("%s = forall([%s], (%s(%s%s))),",
				NewTempVariable(), Generator.toString(), nullGuard.toString(), pExpr.toString(), pExpr.tmpVariables().get(0)));
	}



	@Override
	public void visit(ExistsQuantifier quantifier)
	{
		final OoaPrologExpression pExpr = createExpressionVisitor();
		quantifier.child().Accept(pExpr);

		// TEMPXY = exists(enumerate1([var:type,...]),pred(var..))
		final StringBuilder Generator = new StringBuilder();
		final StringBuilder nullGuard = new StringBuilder();
		int i = 0;
		for (final Identifier v: quantifier.symbols().symbolList())
		{
			final OoaPrologIdentifier ident = createIdentifierVisitor();
			v.Accept(ident);

			final OoaPrologType identType = createTypeVisitor();
			v.type().Accept(identType);

			Generator.append(String.format("%s %s: %s", i == 0 ? "" : ",", ident.toString(), identType.toString()));
			if (v.type().kind() == TypeKind.OoActionSystemType)
				nullGuard.append(String.format("(%s \\= null), ", ident.toString()));
			i++;
		}

		m_emitter.AppendLine(String.format("%s = exists([%s], (%s(%s%s))),",
				NewTempVariable(), Generator.toString(), nullGuard.toString(), pExpr.toString(), pExpr.tmpVariables().get(0)));
	}
	@Override
	public void visit(UnaryOperator unaryOperator)
	{
		assert(m_tmpVars.size() == 0);
		VisitSub(unaryOperator.child(), unaryOperator);

		if (unaryOperator.kind() == ExpressionKind.Cast)
			return;

		final String childresult = m_tmpVars.get(0); m_tmpVars.remove(0);
		assert(m_tmpVars.size() == 0);

		final String tmpresult = NewTempVariable();

		switch (unaryOperator.kind())
		{
		case head:
			m_emitter.AppendLine(String.format("ulyssesListHead(%s,%s),", childresult, tmpresult));
			break;

		case tail:
			m_emitter.AppendLine(String.format("ulyssesListTail(%s,%s),", childresult, tmpresult));
			break;

		case len:    // T_LEN:
			m_emitter.AppendLine(String.format("ulyssesListLength(%s,%s),", childresult, tmpresult));
			break;

		case not:

			if (unaryOperator.type().kind() == TypeKind.IntType)
				m_emitter.Append(String.format(" %s #= call(\\+", tmpresult));
			else
				m_emitter.Append(String.format(" %s = call(\\+", tmpresult));
			m_emitter.Append("(");
			m_emitter.Append(childresult);
			m_emitter.AppendLine(")),");


			break;

		case Cast:
			// todo
			break;

		default:
			if (unaryOperator.type().kind() == TypeKind.IntType)
				m_emitter.Append(String.format(" %s #= (%s", tmpresult, OperatorString(unaryOperator, unaryOperator.child().type())));
			else
				m_emitter.Append(String.format(" %s = (%s", tmpresult, OperatorString(unaryOperator, unaryOperator.child().type())));
			m_emitter.Append("(");
			m_emitter.Append(childresult);
			m_emitter.AppendLine(")),");
			break;
		}
		assert(m_tmpVars.size() == 1);
	}

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

	protected OoaPrologType createTypeVisitor() { return m_typeFactory.create(m_idFactory, m_scratchbook); }
	protected OoaPrologIdentifier createIdentifierVisitor() { return m_idFactory.create(); }
	protected OoaPrologExpression createExpressionVisitor() { return m_exprFactory.create(m_idFactory, m_typeFactory, m_scratchbook); }

	protected final OoaPrologIdentifier.Factory m_idFactory;
	protected final OoaPrologType.Factory m_typeFactory;
	protected final OoaPrologExpression.Factory m_exprFactory;

	protected OoaPrologExpression(
			OoaPrologIdentifier.Factory idFactory,
			OoaPrologType.Factory typeFactory,
			Scratchbook scratchbook,
			OoaPrologExpression.Factory expressionFactory)
	{
		this(idFactory, typeFactory, scratchbook, expressionFactory, false);
	}

	protected OoaPrologExpression(
			OoaPrologIdentifier.Factory idFactory,
			OoaPrologType.Factory typeFactory,
			Scratchbook scratchbook,
			OoaPrologExpression.Factory expressionFactory,
			boolean isLHS)
	{
		super();
		m_LhsExpression = isLHS;
		m_idFactory = idFactory;
		m_typeFactory = typeFactory;
		m_exprFactory = expressionFactory;
		m_scratchbook = scratchbook;
	}


	public String NewTempVariable()
	{
		final String result = String.format("TMPVAR_%s", m_scratchbook.getNewTmpVarCntrValue());
		m_tmpVars.add(result);
		return result;
	}

	public int GetUniqueNumber()
	{
		return m_scratchbook.getNewTmpVarCntrValue();
	}
}