/**
  *
  *                      OOAS Compiler (Deprecated)
  *
  * Copyright 2015, Institute for Software Technology, Graz University of
  * Technology. Portions are copyright 2015 by the AIT Austrian Institute
  * of Technology. All rights reserved.
  *
  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
  *
  * Please notice that this version of the OOAS compiler is considered de-
  * precated. Only the Java version is maintained.
  *
  * Contributors:
  *               Willibald Krenn (TU Graz/AIT)
  *               Stefan Tiran (TU Graz/AIT)
  */

/*
 * Prolog Code Generator
 */

using System;
using System.Collections.Generic;
using System.Text;
using TUG.Mogentes.Codegen;


namespace TUG.Mogentes.Codegen.Prolog
{
    public class OoaPrologExpression : OoaExpressionVisitor
    {
        public class Factory
        {
            public OoaPrologExpression create(OoaPrologIdentifier.Factory idFactory, OoaPrologType.Factory typeFactory) 
            { return create(idFactory, typeFactory, false); }
            public virtual OoaPrologExpression create(OoaPrologIdentifier.Factory idFactory, OoaPrologType.Factory typeFactory, bool lhs)
            { return new OoaPrologExpression(idFactory, typeFactory, this, lhs); }
        }

        protected OoaCodeEmitter m_emitter = new OoaCodeEmitter();
        protected List<string> m_tmpVars = new List<string>();
        private bool m_LhsExpression = false;


        public List<string> tmpVariables { get { return m_tmpVars; } }
        public bool isLhsExpression { get { return m_LhsExpression; } }

        private string GetPrologType(UlyssesType aType)
        {
            OoaPrologType pType = createTypeVisitor();
            aType.Accept(pType);
            return pType.ToString();
        }

        protected string GetIdentifierString(Identifier anIdentifier)
        {
            OoaPrologIdentifier pIdent = createIdentifierVisitor();
            anIdentifier.Accept(pIdent);
            return pIdent.ToString();
        }


        // following call must not happen
        public override void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)
        {
            System.Diagnostics.Debug.Assert(false);
        }

        // call of method that returns a value..
        public override void visit(CallExpression callExpression)
        {
            // we handle only function calls within expressions here (must have non-void return!)
            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 = String.Empty;
            StringBuilder parameter = new StringBuilder();

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

            m_emitter.Append(prologexpr.ToString());
            callstatement = prologexpr.tmpVariables[0];
            int i = 0;
            foreach (var arg in callExpression.arguments)
            {
                if (i != 0)
                    parameter.Append(", ");
                else
                    i++;
                OoaPrologExpression paramexpr = createExpressionVisitor();
                arg.Accept(paramexpr);
                m_emitter.Append(paramexpr.ToString());
                parameter.Append(paramexpr.tmpVariables[0]);
            }
            if (parameter.Length > 0)
                m_emitter.AppendLine(String.Format("{0}({1},{2}),", callstatement, parameter, NewTempVariable()));
            else
                m_emitter.AppendLine(String.Format("{0}({1}),", callstatement, NewTempVariable()));
        }


        // we need to map all other things to Prolog constructs
        private string OperatorString(Expression expression, UlyssesType resultingType)
        {
            switch (expression.kind)
            {
                case ExpressionKind.abs:    // T_ABS:
                case ExpressionKind.card:   // T_CARD:
                case ExpressionKind.dom:    // T_DOM:
                case ExpressionKind.range:  // T_RNG:
                case ExpressionKind.merge:  // T_MERGE:
                case ExpressionKind.elems:  // T_ELEMS:
                case ExpressionKind.head:   // T_HEAD:
                case ExpressionKind.tail:   // T_TAIL:
                case ExpressionKind.conc:   // T_CONC:
                case ExpressionKind.inds:   // T_INDS:
                case ExpressionKind.dinter: // T_DINTER:
                case ExpressionKind.dunion: // T_DUNION:
                case ExpressionKind.domresby:   // T_DOMRESBY:
                case ExpressionKind.domresto:   // T_DOMRESTO:
                case ExpressionKind.rngresby:   // T_RNGRESBY:
                case ExpressionKind.rngresto:   // T_RNGRESTO:
                case ExpressionKind.inter:  // T_INTER:
                case ExpressionKind.union:  // T_UNION:
                case ExpressionKind.diff:   // T_DIFF:
                case ExpressionKind.munion: // T_MUNION:
                case ExpressionKind.seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:
                case ExpressionKind.subset:
                case ExpressionKind.elemin:
                case ExpressionKind.notelemin:
                case ExpressionKind.implies:    // T_IMPLIES:
                case ExpressionKind.biimplies:  // T_BIIMPLIES:
                case ExpressionKind.Primed:
                case ExpressionKind.len:    // T_LEN:
                    throw new NotImplementedException();

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

                case ExpressionKind.Cast:
                    return String.Empty;

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

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

        public override void visit<T>(ValueExpression<T> valueExpression)
        {
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
            string tmpVar = NewTempVariable();
            m_emitter.Append(String.Format("{0} ", tmpVar));


            if (valueExpression.value == null)
                m_emitter.Append("= 'null'");
            else if (valueExpression is ValueExpression<bool>)
                m_emitter.Append((valueExpression as ValueExpression<bool>).value ? " #= true" : " #= fail");
            else if (valueExpression is ValueExpression<char>)
                m_emitter.Append(String.Format("#= '{0}'", valueExpression.ToString()));
            else if (valueExpression is ValueExpression<int>)
                m_emitter.Append(String.Format("#= {0}", valueExpression.ToString()));
            else
                m_emitter.Append(String.Format("= {0}", valueExpression.value.ToString()));

            m_emitter.AppendLine(",");
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
        }

        public override void visit(IdentifierExpression identifierExpression)
        {
            if (identifierExpression.identifier.kind == IdentifierKind.LandmarkIdentifier)
            {
                LandmarkIdentifier lmid = (LandmarkIdentifier)identifierExpression.identifier;
                OoaPrologIdentifier pid = createIdentifierVisitor();
                lmid.Accept(pid);
                //m_emitter.Append(pid.ToString());
                m_tmpVars.Add(pid.ToString());
                return;
            }
            else if (identifierExpression.identifier.kind == IdentifierKind.EnumIdentifier)
            {
                EnumIdentifier enumid = (EnumIdentifier)identifierExpression.identifier;
                EnumType enumType = (EnumType)enumid.type;
                //m_emitter.Append(enumType.listOfEnumSymbols.IndexOf(enumid));
                if (enumType is ValuedEnumType)
                    m_emitter.AppendLine(String.Format("{0} #= {1},", NewTempVariable(), enumid.Value));
                else
                    m_emitter.AppendLine(String.Format("{0} #= {1},", NewTempVariable(), enumType.listOfEnumSymbols.IndexOf(enumid).ToString()));
            }
            else if (identifierExpression.isSelf)
            {
                m_emitter.AppendLine(String.Format("{0} = {1},", NewTempVariable(), GetIdentifierString(identifierExpression.identifier)));
            }
            /*else if (identifierExpression.identifier.kind == IdentifierKind.AttributeIdentifier)
            {
                m_emitter.AppendLine(String.Format("getVal({1},{0},_),", NewTempVariable(), GetIdentifierString(identifierExpression.identifier)));
            }*/
            else
            {
                //m_emitter.Append(GetIdentifierString(identifierExpression.identifier));
                m_tmpVars.Add(GetIdentifierString(identifierExpression.identifier));
            }
        }

        public override void visit(TypeExpression typeExpression)
        {
            if (typeExpression.type.kind != TypeKind.QrType &&
                typeExpression.type.kind != TypeKind.EnumeratedType)
            {
                //m_emitter.Append(GetIdentifierString(typeExpression.type.identifier));
                m_emitter.Append(GetIdentifierString(typeExpression.type.identifier));
            }
        }


        public override void visit(ObjectConstructor objectConstructor)
        {
            if (objectConstructor.instances.Count > 1)
                throw new NotImplementedException();

            m_emitter.AppendLine(String.Format("{0} = '{1}',", NewTempVariable(), objectConstructor.instances[0].Name));

            //m_emitter.Append(String.Format("new {0}(this)", GetIdentifierString(objectConstructor.type.identifier)));
        }

        public override void visit(ListConstructor listConstructor)
        {
            if (listConstructor.hasComprehension)
            {
                OoaPrologExpression compr = createExpressionVisitor();
                listConstructor.comprehension.Accept(compr);
                OoaPrologExpression elem = createExpressionVisitor();
                listConstructor.elements[0].Accept(elem);

                StringBuilder enumvars = new StringBuilder();
                int i = 0;
                foreach (var v in listConstructor.comprehensionVariables.symbolList)
                {
                    OoaPrologIdentifier ident = createIdentifierVisitor();
                    v.Accept(ident);

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

                    enumvars.Append(String.Format("{2} {0}: {1}", ident.ToString(), identType.ToString(), i == 0 ? String.Empty : ","));
                    i++;
                }

                m_emitter.AppendLine("% listcomprehension");
                m_emitter.AppendLine(String.Format("{0} = {{{1}:[{2}]:({3}{4},{5}{6})}}",
                    NewTempVariable(), elem.tmpVariables[0], enumvars.ToString(), compr.ToString(), compr.tmpVariables[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("{0} = []", NewTempVariable()));

                foreach (var expr in listConstructor.elements)
                {
                    m_emitter.Append(", ");

                    OoaPrologExpression pVal = createExpressionVisitor();
                    expr.Accept(pVal);
                    m_emitter.Append(pVal.ToString());
                    System.Diagnostics.Debug.Assert(pVal.tmpVariables.Count == 1);
                    m_emitter.AppendLine(String.Format("ulyssesListConc({0},[{1}],{2})", m_tmpVars[0], pVal.tmpVariables[0], NewTempVariable()));
                    m_tmpVars.RemoveAt(0);
                }
            }
            m_emitter.Append(",");
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
        }

        public override void visit(SetConstructor setConstructor)
        {
            throw new NotImplementedException();
        }

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

        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("{0} = []", NewTempVariable()));

                foreach (var expr in tupleConstructor.values)
                {
                    m_emitter.Append(", ");

                    OoaPrologExpression pVal = createExpressionVisitor();
                    expr.Accept(pVal);
                    m_emitter.Append(pVal.ToString());
                    System.Diagnostics.Debug.Assert(pVal.tmpVariables.Count == 1);
                    m_emitter.AppendLine(String.Format("ulyssesListConc({0},[{1}],{2})", m_tmpVars[0], pVal.tmpVariables[0], NewTempVariable()));
                    m_tmpVars.RemoveAt(0);
                }
                m_emitter.Append(",");
                System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
            }
        }

        public override void visit(QValConstructor qValConstructor)
        {
            OoaPrologIdentifier pident = createIdentifierVisitor();
            qValConstructor.type.identifier.Accept(pident);
            StringBuilder qVal = new StringBuilder();
            if (qValConstructor.value != null || qValConstructor.value.Length != 0)
            {
                OoaPrologExpression landmark1 = createExpressionVisitor();
                qValConstructor.value[0].Accept(landmark1);
                qVal.Append(landmark1.ToString());

                if (qValConstructor.value.Length > 1)
                {
                    OoaPrologExpression landmark2 = createExpressionVisitor();
                    qValConstructor.value[1].Accept(landmark2);
                    qVal.Append("..");
                    qVal.Append(landmark2.ToString());
                }
            }
            else
                qVal.Append("_");

            string deriv = "_";
            switch (qValConstructor.valueDeriv)
            {
                case QValDeriv.Dec:
                    deriv = "dec";
                    break;
                case QValDeriv.Inc:
                    deriv = "inc";
                    break;
                case QValDeriv.Steady:
                    deriv = "std";
                    break;

            }
            string tmpVar = NewTempVariable();
            m_emitter.AppendLine(String.Format("{3} = ({0}:{1}/{2}),", pident.ToString(), qVal.ToString(), deriv, tmpVar));
        }

        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))
            {
                System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
                // enums and qr types are directly (statically) converted to nums...
                VisitSub(accessExpression.left, accessExpression);
                string leftresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);

                VisitSub(accessExpression.right, accessExpression);
                string rightresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);

                m_tmpVars.Add(String.Format("{0}\\{1}", leftresult, rightresult));
            }
            else
                VisitSub(accessExpression.right, accessExpression);
        }

        public override void visit(BinaryOperator binaryOperator)
        {
            OoaCodeEmitter origEmitter = m_emitter;


            // eval stack must be empty
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
            // traverse left
            OoaCodeEmitter leftcode = new OoaCodeEmitter();
            m_emitter = leftcode;
            VisitSub(binaryOperator.left, binaryOperator);
            string leftresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
            // traverse right
            OoaCodeEmitter rightcode = new OoaCodeEmitter();
            m_emitter = rightcode;
            VisitSub(binaryOperator.right, binaryOperator);
            string rightresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
            // eval stack must be empty
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);

            m_emitter = origEmitter;

            // get tmp.var
            string tmpVar = NewTempVariable();

            switch (binaryOperator.kind)
            {
                case ExpressionKind.elemin:
                    m_emitter.Append(leftcode.ToString());
                    m_emitter.Append(rightcode.ToString());
                    m_emitter.AppendLine(String.Format(" {0} = member({1},{2}),",
                        tmpVar, leftresult, rightresult));
                    break;
                case ExpressionKind.and:    // T_AND:
                    m_emitter.Append(leftcode.ToString());
                    m_emitter.Append(rightcode.ToString());
                    m_emitter.AppendLine(String.Format(" {0} = ({1} {2} {3}), ",
                        tmpVar, leftresult, ",", rightresult));
                    break;
                case ExpressionKind.or:     // T_OR:
                    m_emitter.Append(leftcode.ToString());
                    m_emitter.Append(rightcode.ToString());
                    m_emitter.AppendLine(String.Format(" {0} = ({1} {2} {3}), ",
                        tmpVar, leftresult, ";", rightresult));
                    break;

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

                case ExpressionKind.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(" {0} = ({1} {2} {3}), ",
                            tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left.type), rightresult));
                    else
                    {
                        m_emitter.Append(String.Format("{0} = unify({1} = [", tmpVar, aTuple));
                        int cntr = 0;
                        foreach (var x in matcher.values)
                        {
                            if (cntr != 0)
                                m_emitter.Append(", ");
                            else
                                cntr++;

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

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



                case ExpressionKind.conc:
                    m_emitter.Append(leftcode.ToString());
                    m_emitter.Append(rightcode.ToString());
                    m_emitter.AppendLine(String.Format("ulyssesListConc({1},{2},{0}),", tmpVar, leftresult, rightresult));
                    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(" {0} #= ({1} {2} {3}), ",
                            tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left.type), rightresult));
                    else
                        m_emitter.AppendLine(String.Format(" {0} = ({1} {2} {3}), ",
                            tmpVar, leftresult, OperatorString(binaryOperator, binaryOperator.left.type), rightresult));
                    //m_emitter.Append(")");
                    break;
            }
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
        }

        public override void visit(TernaryOperator ternaryOperator)
        {
            if (ternaryOperator.kind == ExpressionKind.conditional)
            {
                VisitSub(ternaryOperator.left, ternaryOperator);
                string leftresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
                VisitSub(ternaryOperator.mid, ternaryOperator);
                string midresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
                VisitSub(ternaryOperator.right, ternaryOperator);
                string rightresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);

                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(" = {0}) );( call(\\+({1})), unify(", varname, leftresult));
                m_emitter.Append(rightresult);
                m_emitter.Append(String.Format(" = {0}) )),", varname));
            }
            else if (ternaryOperator.kind == ExpressionKind.foldRL)
                throw new NotImplementedException();
            else if (ternaryOperator.kind == ExpressionKind.foldLR)
            {
                VisitSub(ternaryOperator.mid, ternaryOperator);
                string midresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
                VisitSub(ternaryOperator.right, ternaryOperator);
                string rightresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);


                int uniqueNumer = GetUniqueNumber();
                m_emitter.Append(String.Format("fun_fold({0},{1},(_Elem_{2}, _In_{2}, Out_{2},(", midresult,
                    rightresult, uniqueNumer));


                // hack the current element and current result values to match the declaration above (change from __result, __elem)
                CallExpression leftcall = (CallExpression)ternaryOperator.left;
                IdentifierExpression elemId = (IdentifierExpression)leftcall.arguments[leftcall.arguments.Count - 1];
                elemId.identifier.SetTokenText(String.Format("Elem_{0}", uniqueNumer));
                IdentifierExpression currentResultId = (IdentifierExpression)leftcall.arguments[leftcall.arguments.Count - 2];
                currentResultId.identifier.SetTokenText(String.Format("In_{0}", uniqueNumer));

                VisitSub(leftcall, ternaryOperator);
                string leftresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
                string tmpresult = NewTempVariable();
                m_emitter.Append(String.Format(" Out_{1} = {2})),{0}),", tmpresult, uniqueNumer, leftresult));
            }



            else
                throw new NotImplementedException();
        }

        public override void visit(TupleMapAccessExpression tupleMapAccessExpression)
        {
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
            VisitSub(tupleMapAccessExpression.child, tupleMapAccessExpression);
            string childresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);

            VisitSub(tupleMapAccessExpression.argument, tupleMapAccessExpression);
            string accessresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);

            string tmpresult = NewTempVariable();

            if (!m_LhsExpression)
            {
                switch (tupleMapAccessExpression.child.type.kind)
                {
                    case TypeKind.TupleType:
                        m_emitter.AppendLine(String.Format("ulyssesTupleAccess({0},{1},{2}),", childresult, accessresult, tmpresult));
                        break;
                    case TypeKind.MapType:
                        m_emitter.AppendLine(String.Format("ulyssesMapAccess({0},{1},{2}),", childresult, accessresult, tmpresult));
                        break;
                    case TypeKind.ListType:
                        m_emitter.AppendLine(String.Format("ulyssesListAccess({0},{1},{2}),", childresult, accessresult, tmpresult));
                        break;
                    default:
                        throw new NotImplementedException();
                }
                System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
            }
            else
            {
                /*>>>>> See comment in ooaTypeCheckVisitor on method CheckPlace! <<<<<<<<<*/
                switch (tupleMapAccessExpression.child.type.kind)
                {
                    case TypeKind.ListType:
                        bool 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;


                        tmpVarCntr++;
                        string newlist = String.Format("RESVAR_{0}", tmpVarCntr);

                        m_emitter.AppendLine(String.Format("ulyssesListWrite({0},{1},{2},{3}),", childresult, accessresult, tmpresult, newlist));

                        if (isAttribute)
                        { m_emitter.AppendLine(String.Format("{0} := {1},", childresult, newlist)); }
                        else
                        { throw new NotImplementedException(); }

                        break;
                    default:
                        throw new NotImplementedException();
                }


            }
        }


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

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

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

                Generator.Append(String.Format("{2} {0}: {1}", ident.ToString(), identType.ToString(), i == 0 ? String.Empty : ","));
                i++;
            }

            m_emitter.AppendLine(String.Format("{0} = forall([{1}],({2}{3})),",
            NewTempVariable(), Generator.ToString(), pExpr.ToString(), pExpr.tmpVariables[0]));
        }



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

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

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

                Generator.Append(String.Format("{2} {0}: {1}", ident.ToString(), identType.ToString(), i == 0 ? String.Empty : ","));
                i++;
            }

            m_emitter.AppendLine(String.Format("{0} = exists([{1}],({2}{3})),",
            NewTempVariable(), Generator.ToString(), pExpr.ToString(), pExpr.tmpVariables[0]));
        }
        public override void visit(UnaryOperator unaryOperator)
        {
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);
            VisitSub(unaryOperator.child, unaryOperator);

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

            string childresult = m_tmpVars[0]; m_tmpVars.RemoveAt(0);
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);

            string tmpresult = NewTempVariable();

            switch (unaryOperator.kind)
            {
                case ExpressionKind.head:
                    m_emitter.AppendLine(String.Format("ulyssesListHead({1},{0}),", tmpresult, childresult));
                    break;

                case ExpressionKind.tail:
                    m_emitter.AppendLine(String.Format("ulyssesListTail({1},{0}),", tmpresult, childresult));
                    break;

                case ExpressionKind.len:    // T_LEN:
                    m_emitter.AppendLine(String.Format("ulyssesListLength({1},{0}),", tmpresult, childresult));
                    break;

                case ExpressionKind.not:

                    if (unaryOperator.type.kind == TypeKind.IntType)
                        m_emitter.Append(String.Format(" {0} #= call(\\+", tmpresult));
                    else
                        m_emitter.Append(String.Format(" {0} = call(\\+", tmpresult));
                    m_emitter.Append("(");
                    m_emitter.Append(childresult);
                    m_emitter.AppendLine(")),");


                    break;

                case ExpressionKind.Cast:
                    // todo
                    break;

                default:
                    if (unaryOperator.type.kind == TypeKind.IntType)
                        m_emitter.Append(String.Format(" {0} #= ({1}", tmpresult, OperatorString(unaryOperator, unaryOperator.child.type)));
                    else
                        m_emitter.Append(String.Format(" {0} = ({1}", tmpresult, OperatorString(unaryOperator, unaryOperator.child.type)));
                    m_emitter.Append("(");
                    m_emitter.Append(childresult);
                    m_emitter.AppendLine(")),");
                    break;
            }
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
        }

        public override string ToString()
        {
            return m_emitter.ToString();
        }

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

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

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

        protected OoaPrologExpression(
            OoaPrologIdentifier.Factory idFactory, 
            OoaPrologType.Factory typeFactory, 
            OoaPrologExpression.Factory expressionFactory,
            bool isLHS)
            : base()
        {
            m_LhsExpression = isLHS;
            m_idFactory = idFactory;
            m_typeFactory = typeFactory;
            m_exprFactory = expressionFactory;
        }


        static int tmpVarCntr = 0;
        public string NewTempVariable()
        {
            tmpVarCntr++;
            string result = String.Format("TMPVAR_{0}", tmpVarCntr);
            m_tmpVars.Add(result);
            return result;
        }

        public int GetUniqueNumber()
        {
            tmpVarCntr++;
            return tmpVarCntr;
        }

    }
}