OoasTools

/**

  *

  *                      OOAS Compiler

  *

  *       Copyright 2015, AIT Austrian Institute of Technology.

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

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

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

  * Technology. All rights reserved.

  *

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

  *

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

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

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

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

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

  *

  * Contributors:

  *               Willibald Krenn (AIT)

  *               Stephan Zimmerer (AIT)

  *               Markus Demetz (AIT)

  *               Christoph Czurda (AIT)

  *

  */

package org.momut.ooas.codegen.prolog;

import java.util.ArrayList;

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 /*override*/ 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, UlyssesType 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 resultingType.kind() == TypeKind.QrType || !isNumericBinary(expression) ? "<" : "#<";

		case lessequal:

			return resultingType.kind() == TypeKind.QrType || !isNumericBinary(expression) ? "=<" : "#=<";

		case greater:

			return resultingType.kind() == TypeKind.QrType || !isNumericBinary(expression) ? ">" : "#>";

		case greaterequal:

			return resultingType.kind() == TypeKind.QrType || !isNumericBinary(expression) ? ">=" : "#>=";

		case equal:

			return resultingType.kind() == TypeKind.QrType || !isNumericBinary(expression) ? "==" : "#=";

		case notequal:

			return resultingType.kind() == TypeKind.QrType || !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 /*override*/ <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 /*override*/ void visit(IdentifierExpression identifierExpression)

	{

		if (identifierExpression.identifier().kind() == IdentifierKind.LandmarkIdentifier)

		{

			final LandmarkIdentifier lmid = (LandmarkIdentifier)identifierExpression.identifier();

			final OoaPrologIdentifier pid = createIdentifierVisitor();

			lmid.Accept(pid);

			//m_emitter.Append(pid.ToString());

			m_tmpVars.add(pid.toString());

			return;

		}

		else 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 /*override*/ void visit(TypeExpression typeExpression)

	{

		if (typeExpression.type().kind() != TypeKind.QrType &&

				typeExpression.type().kind() != TypeKind.EnumeratedType)

		{

			m_emitter.Append(GetIdentifierString(typeExpression.type().identifier()));

		}

	}

	@Override

	public /*override*/ 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 /*override*/ 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 /*override*/ 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 /*override*/ void visit(MapConstructor mapConstructor)

	{

		throw new NotImplementedException();

	}

	@Override

	public /*override*/ 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 /*override*/ void visit(QValConstructor qValConstructor)

	{

		final OoaPrologIdentifier pident = createIdentifierVisitor();

		qValConstructor.type().identifier().Accept(pident);

		final StringBuilder qVal = new StringBuilder();

		if (qValConstructor.value() != null || qValConstructor.value().length != 0)

		{

			final OoaPrologExpression landmark1 = createExpressionVisitor();

			qValConstructor.value()[0].Accept(landmark1);

			qVal.append(landmark1.toString());

			if (qValConstructor.value().length > 1)

			{

				final OoaPrologExpression landmark2 = createExpressionVisitor();

				qValConstructor.value()[1].Accept(landmark2);

				qVal.append("..");

				qVal.append(landmark2.toString());

			}

		}

		else

			qVal.append("_");

		String deriv = "_";

		switch (qValConstructor.valueDeriv())

		{

		case Dec:

			deriv = "dec";

			break;

		case Inc:

			deriv = "inc";

			break;

		case Steady:

			deriv = "std";

			break;

		default:

			throw new NotImplementedException();

		}

		final String tmpVar = NewTempVariable();

		m_emitter.AppendLine(String.format("%s = (%s:%s/%s),", tmpVar, pident.toString(), qVal.toString(), deriv));

	}

	@Override

	public /*override*/ void visit(AccessExpression accessExpression)

	{

		if (accessExpression.left().type().kind() != TypeKind.QrType &&

				accessExpression.left().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 /*override*/ 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());

			if (binaryOperator.left().type().kind() == TypeKind.QrType)

				m_emitter.Append("qEval");

			//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 /*override*/ 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 /*override*/ 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 /*override*/ 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 /*override*/ 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 /*override*/ 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 /*override*/ 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();

	}