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

namespace TUG.Mogentes
{

    

    public sealed class OoaDeepCloneVisitor : OoaCompleteAstTraversalVisitor
    {
        Dictionary<object, object> mapping;
        Identifier selfreplacement;
        //List<SymbolTable> symboltables = new List<SymbolTable>();


        public bool quantifierState = false;

        /* we do not clone types */
        public override void visit(AnyType anyType)
        { throw new NotImplementedException(); }
        public override void visit(BoolType boolType)
        { throw new NotImplementedException(); }
        public override void visit(CharType charType)
        { throw new NotImplementedException(); }
        public override void visit(EnumType enumType)
        { throw new NotImplementedException(); }
        public override void visit(FloatType floatType)
        { throw new NotImplementedException(); }
        public override void visit(FunctionType functionType)
        { throw new NotImplementedException(); }
        public override void visit(IntType intType)
        { throw new NotImplementedException(); }
        public override void visit(ListType listType)
        { throw new NotImplementedException(); }
        public override void visit(MapType mapType)
        { throw new NotImplementedException(); }
        public override void visit(NullType nullType)
        { throw new NotImplementedException(); }
        public override void visit(OoActionSystemType ooActionSystemType)
        { throw new NotImplementedException(); }
        public override void visit(TupleType tupleType)
        { throw new NotImplementedException(); }
        public override void visit(EnumIdentifier enumIdentifier)
        { throw new NotImplementedException(); }
        public override void visit(LandmarkIdentifier landmarkIdentifier)
        { throw new NotImplementedException(); }
        public override void visit(ExpressionVariableIdentifier expressionVariableIdentifier)
        { throw new NotImplementedException(); }


        public override void visit(LocalVariableIdentifier localVariableIdentifier)
        {
            throw new NotImplementedException();
        }

        public override void visit(MainModule mainModule)
        {
            throw new NotImplementedException();
        }


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

        public override void visit(MethodIdentifier methodIdentifier)
        {
            throw new NotImplementedException();
        }

        public override void visit(NamedActionIdentifier namedActionIdentifier)
        {
            Block newBlock = (Block)SClone(namedActionIdentifier.body);
            namedActionIdentifier.SetBody(newBlock);
            // we do not clone the parameters..
        }

        public override void visit(Module module)
        {
            throw new NotImplementedException();
        }

        public override void visit(NondetIdentifierList nondetIdentifierList)
        {
            throw new NotImplementedException();
        }


        public override void visit(OpaqueType opaqueType)
        {
            throw new NotImplementedException(); // must not happen
        }

        public override void visit(ParameterIdentifier parameterIdentifier)
        {
            throw new NotImplementedException();
        }

        public override void visit(PrioIdentifierList prioIdentifierList)
        {
            throw new NotImplementedException();
        }

        public override void visit(QrType qrType)
        {
            throw new NotImplementedException();
        }



        public override void visit(ObjectConstructor objectConstructor)
        {
            //base.visit(objectConstructor);
        }

        private void UpdateScope(IScope aScope)
        {
            if (aScope.GetParentScope() != null && !mapping.ContainsKey(aScope.GetParentScope()))
                throw new ArgumentException();
            else if (aScope.GetParentScope() != null)
            {
                aScope.SetParentScope((IScope)mapping[aScope.GetParentScope()]);
            }
        }


        private Expression EClone(Expression anExpr)
        {
            Expression result = null;
            if (anExpr != null)
            {
                result = anExpr.Clone();

                if (anExpr is IScope)
                {
                    mapping.Add(anExpr, result);
                    UpdateScope((IScope)result);
                }

                result.Accept(this);
            }
            return result;
        }

        private Statement SClone(Statement aStatement)
        {
            Statement result = null;
            if (aStatement != null)
            {
                result = aStatement.Clone();

                if (aStatement is IScope)
                {
                    mapping.Add(aStatement, result);
                    UpdateScope((IScope)result);
                }

                result.Accept(this);
            }
            return result;
        }

        // clones symbols found in symbol table
        private void SymTabClone(SymbolTable aTable)
        {
            if (aTable != null && aTable.symbolList.Count > 0)
            {
                List<Identifier> newList = new List<Identifier>();
                foreach (var x in aTable.symbolList)
                {
                    if (!mapping.ContainsKey(x))
                    {
                        Identifier newid = x.Clone();
                        newList.Add(newid);
                        mapping.Add(x, newid);
                    }
                    else
                        newList.Add((Identifier)mapping[x]);
                }
                aTable.SetSymbolList(newList);
            }
        }


        private void cloneExpressionList(LinkedListNode<Expression> anElem)
        {
            while (anElem != null)
            {
                anElem.Value = EClone(anElem.Value);
                anElem = anElem.Next;
            }
        }


        /*no need to clone leafs (they are already cloned and a shallow copy is sufficient*/
        public override void visit(AbortStatement abortStatement)
        { }
        public override void visit<T>(ValueExpression<T> valueExpression)
        { }


        /*clone a block*/
        public void cloneBlock(Block aBlock)
        {
            SymTabClone(aBlock.symbols);
            LinkedListNode<Statement> stmnt = aBlock.statements.First;
            while (stmnt != null)
            {
                stmnt.Value = SClone(stmnt.Value);
                stmnt = stmnt.Next;
            }
        }
        public override void visit(NondetBlock nondetBlock)
        {
            cloneBlock(nondetBlock);
        }
        public override void visit(SeqBlock seqBlock)
        {
            seqBlock.SetFilter(EClone(seqBlock.filter));
            cloneBlock(seqBlock);
        }
        public override void visit(PrioBlock prioBlock)
        {
            cloneBlock(prioBlock);
        }

        public override void visit(AccessExpression accessExpression)
        {
            visit((BinaryOperator)accessExpression);
        }
        public override void visit(BinaryOperator binaryOperator)
        {
            Expression left = EClone(binaryOperator.left);
            Expression right = EClone(binaryOperator.right);
            binaryOperator.SetLeftChild(left);
            binaryOperator.SetRightChild(right);
        }

        public override void visit(Assignment assignment)
        {
            SymTabClone(assignment.symbols);
            cloneExpressionList(assignment.places.First);
            cloneExpressionList(assignment.values.First);
            assignment.SetNondetExpression(EClone(assignment.nondetExpression));
            UpdateScope(assignment);
        }
        public override void visit(AttributeIdentifier attributeIdentifier)
        {
            Expression initializer = EClone(attributeIdentifier.initializer);
            attributeIdentifier.SetInitializer(initializer);
        }
        public override void visit(Call call)
        {
            Expression cExpr = EClone(call.callExpression);
            call.SetCallExpression(cExpr);
        }

        public override void visit(CallExpression callExpression)
        {
            List<Expression> newargs = new List<Expression>();
            foreach (var x in callExpression.arguments)
            {
                newargs.Add(EClone(x));
            }
            callExpression.SetArguments(newargs);

            visit((UnaryOperator)callExpression);
        }

        public void CloneQuantifier(Quantifier qf)
        {
            SymTabClone(qf.symbols);
            bool oldQunatifierState = quantifierState;
            quantifierState = true;
            visit((UnaryOperator)qf);
            quantifierState = oldQunatifierState;
        }
        public override void visit(ExistsQuantifier quantifier)
        {
            CloneQuantifier(quantifier);
        }
        public override void visit(ForallQuantifier quantifier)
        {
            CloneQuantifier(quantifier);
        }




        public override void visit(GuardedCommand guardedCommand)
        {
            Block newblock = (Block)SClone(guardedCommand.body);
            Expression newguard = EClone(guardedCommand.guard);
            guardedCommand.SetBody(newblock);
            guardedCommand.SetGuard(newguard);
        }

        public override void visit(IdentifierExpression identifierExpression)
        {
            
            if (identifierExpression.isSelf)
            {
                /*if (quantifierState) //FIXXME
                {
                    if (!selfreplacement.tokenText.StartsWith("attr"))
                    {
                        String oldTokenText = selfreplacement.tokenText;
                        selfreplacement.SetTokenText("attr____model_root_" + selfreplacement.tokenText);
                        identifierExpression.SetIdentifier(selfreplacement);
                        selfreplacement.SetTokenText(oldTokenText);
                    }
                }
                else
                */
                identifierExpression.SetIdentifier(selfreplacement);
                
               
            }
            else if (mapping.ContainsKey(identifierExpression.identifier) 
                && identifierExpression.identifier.kind != IdentifierKind.MethodIdentifier)

            /* we do NOT replace method calls here, since they are prefixed by self if it's a
             * method in the current object or by some field/method access if it's another 
             * object.
             */ 
                identifierExpression.SetIdentifier((Identifier)mapping[identifierExpression.identifier]);
            
        }

        public override void visit(KillStatement killStatement)
        {
            if (mapping.ContainsKey(killStatement.someOne))
                killStatement.SetIdentifier((Identifier)mapping[killStatement.someOne]);
        }


        public override void visit(ListConstructor listConstructor)
        {
            SymTabClone(listConstructor.comprehensionVariables);

            List<Expression> newelems = new List<Expression>();
            foreach (var x in listConstructor.elements)
                newelems.Add(EClone(x));

            listConstructor.SetElements(newelems);
            listConstructor.SetComprehension(EClone(listConstructor.comprehension));
        }

        public override void visit(QualitativeConstraintStatement qalitativeConstraintStatement)
        {
            if (qalitativeConstraintStatement.variable0 != null && mapping.ContainsKey(qalitativeConstraintStatement.variable0))
                qalitativeConstraintStatement.SetVariable0((Identifier)mapping[qalitativeConstraintStatement.variable0]);
            if (qalitativeConstraintStatement.variable1 != null && mapping.ContainsKey(qalitativeConstraintStatement.variable1))
                qalitativeConstraintStatement.SetVariable1((Identifier)mapping[qalitativeConstraintStatement.variable1]);
            if (qalitativeConstraintStatement.variable2 != null && mapping.ContainsKey(qalitativeConstraintStatement.variable2))
                qalitativeConstraintStatement.SetVariable2((Identifier)mapping[qalitativeConstraintStatement.variable2]);
        }


        public override void visit(QValConstructor qValConstructor)
        {
            List<Expression> values = new List<Expression>(qValConstructor.value);
            for (int i = 0; i < values.Count; i++)
                qValConstructor.value[i] = EClone(values[i]);
        }

        public override void visit(SeqIdentifierList seqIdentifierList)
        {
            throw new NotImplementedException();
        }


        public override void visit(SetConstructor setConstructor)
        {
            SymTabClone(setConstructor.comprehensionVariables);
            List<Expression> newelems = new List<Expression>();
            foreach (var x in setConstructor.items)
                newelems.Add(EClone(x));

            setConstructor.SetItems(newelems);
            setConstructor.SetComprehension(EClone(setConstructor.comprehension));
        }


        public override void visit(SkipStatement skipStatement)
        { }

        public override void visit(TernaryOperator ternaryOperator)
        {
            ternaryOperator.SetLeftChild(EClone(ternaryOperator.left));
            ternaryOperator.SetMidChild(EClone(ternaryOperator.mid));
            ternaryOperator.SetRightChild(EClone(ternaryOperator.right));
        }

        public override void visit(TupleConstructor tupleConstructor)
        {
            List<Expression> values = new List<Expression>();
            foreach (var x in tupleConstructor.values)
                values.Add(EClone(x));
            tupleConstructor.SetTupleValues(values);
        }

        public override void visit(TupleMapAccessExpression tupleMapAccessExpression)
        {
            tupleMapAccessExpression.SetArgument(EClone(tupleMapAccessExpression.argument));
            visit((UnaryOperator)tupleMapAccessExpression);
        }

        public override void visit(TypeExpression typeExpression)
        { /*we do not clone types*/ }


        public override void visit(TypeIdentifier typeIdentifier)
        {
            throw new NotImplementedException();
        }

        public override void visit(UnaryOperator unaryOperator)
        {
            Expression child = EClone(unaryOperator.child);
            unaryOperator.SetChild(child);
        }


        public override void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)
        {
            throw new NotImplementedException(); // must not occur
        }

        public override void visit(UnspecIdentifierList unspecIdentifierList)
        {
            throw new NotImplementedException();
        }

        public OoaDeepCloneVisitor(Dictionary<object, object> initMapping, Identifier selfreplace)
            : base(null)
        {
            mapping = new Dictionary<object, object>(initMapping);
            selfreplacement = selfreplace;
        }
    }
    
}