OoasTools

/**

  *

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

        { }

    }

}