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

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

namespace TUG.Mogentes.Codegen.PrologSymbolic
{
    public class OoaPrologSymbolicExpression : OoaPrologExpression
    {
        new public class Factory : OoaPrologExpression.Factory
        {
            public override OoaPrologExpression create(OoaPrologIdentifier.Factory idFactory, OoaPrologType.Factory typeFactory, bool lhs)
            { return new OoaPrologSymbolicExpression(idFactory, typeFactory, this, lhs); }
        }
        
        /*Also treats bools and enums as ints..*/
        new protected bool isNumericBinary(Expression expression)
        {
            bool result = false;
            if (expression is BinaryOperator)
            {
                TypeKind leftKind = ((BinaryOperator)expression).left.type.kind;
                TypeKind rightKind = ((BinaryOperator)expression).right.type.kind;
                result = (leftKind == TypeKind.IntType || leftKind == TypeKind.BoolType || leftKind == TypeKind.EnumeratedType) &&
                     (rightKind == TypeKind.IntType || rightKind == TypeKind.BoolType || rightKind == TypeKind.EnumeratedType);
            }
            else if (expression is UnaryOperator)
            {
                TypeKind childKind = ((UnaryOperator)expression).child.type.kind;
                result = childKind == TypeKind.IntType || childKind == TypeKind.BoolType || childKind == TypeKind.EnumeratedType;
            }
            else throw new NotImplementedException();
            return result;
        }

        // 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 ? "==" : "#=";
                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);
            }
        }

        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" : " = false");
            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(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} = ( #\\", tmpresult));
                    m_emitter.Append("(");
                    m_emitter.Append(childresult);
                    m_emitter.AppendLine(")),");
                    break;

                case ExpressionKind.Cast:
                    // todo
                    break;

                default:
// do not use #= for assignments in the symbolic backend
//                    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 void visit(BinaryOperator binaryOperator)
        {
            // eval stack must be empty
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 0);

            OoaCodeEmitter origEmitter = m_emitter;
            OoaCodeEmitter leftcode = new OoaCodeEmitter();
            OoaCodeEmitter rightcode = new OoaCodeEmitter();


            // traverse left
            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
            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);

            // restore original emitter and get tmp.var
            m_emitter = origEmitter;
            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");

// do not use #= for assignments in the symbolic backend
//                    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));
                    break;
            }
            System.Diagnostics.Debug.Assert(m_tmpVars.Count == 1);
        }



        protected OoaPrologSymbolicExpression(
            OoaPrologIdentifier.Factory idFactory, 
            OoaPrologType.Factory typeFactory, 
            OoaPrologExpression.Factory expressionFactory,
            bool lhs)
            : base(idFactory, typeFactory, expressionFactory, lhs)
        { }

    }
}