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;

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

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.identifiers.LandmarkIdentifier;

import org.momut.ooas.ast.types.EnumType;

import org.momut.ooas.ast.types.FunctionType;

import org.momut.ooas.ast.types.TypeKind;

import org.momut.ooas.ast.types.UlyssesType;

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

        }

}