/*******************************************************************************
 * Copyright (c) 2004-2008 Akos Horvath, Gergely Varro and Daniel Varro
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *    Akos Horvath, Gergely Varro - initial API and implementation
 *******************************************************************************/

 package org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.callgraph;

import org.eclipse.emf.common.util.EList;
import org.eclipse.viatra2.gtasm.interpreter.exception.ViatraTransformationException;
import org.eclipse.viatra2.gtasm.interpreter.executionEnvironment.IExecutionEnvironment;
import org.eclipse.viatra2.gtasm.interpreter.impl.executionEnvironment.ExecutionEnvironment;
import org.eclipse.viatra2.gtasm.patternmatcher.exceptions.PatternMatcherCompileTimeException;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.core.PatternBuilder;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.EdgeType;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.PatternMatcher;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.PatternMatcherErrorStrings;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.VariableID;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.algorithms.ISearchGraph;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.callgraph.FlattenedPattern.Pair;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.operation.CheckOperation;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.operation.NACCheckOperation;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.searchgraph.SearchGraphEdge;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.searchgraph.SearchGraphNode;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.internal.searchgraph.traceability.EdgeTraceabilityElement;
import org.eclipse.viatra2.gtasm.patternmatcher.impl.patternmatcher.term.ITermHandler;
import org.eclipse.viatra2.gtasm.patternmatcher.patterns.IPatternMatcher;
import org.eclipse.viatra2.gtasm.patternmatcher.patterns.PatternMatcherProvider;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.core.RuntimeAnnotation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.Variable;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.GTPatternCall;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.Term;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.VariableReference;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.ContainmentConstraint;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.GTPattern;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.GTPatternBody;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.NonInjectivityConstraint;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.PatternVariable;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.PatternVariableAssignment;
import org.eclipse.viatra2.gtasmmodel.vpm.editmodel.ModelElement;
import org.eclipse.viatra2.core.IModelManager;
import org.eclipse.viatra2.logger.Logger;


import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;



public class BodyNode extends EvenLevelNode implements IFlattenedPatternElement {
   private GTPatternBody body;
    protected OddLevelNode[] children;
    
    BodyNode(PatternMatcher patternMatcher, 
    		PatternNode parent, GTPatternBody body) throws PatternMatcherCompileTimeException {
        super(parent);
        this.body = body;
        this.children = new OddLevelNode[body.getCalledPatterns().size()];

        List<GTPatternCall> patternCalls = body.getCalledPatterns();
        for (int i = 0; i < patternCalls.size(); i++) {
            GTPatternCall patternCall = patternCalls.get(i);
            PatternNode loopClosingNode = causesRecursion(patternCall.getCalledPattern());
            if (loopClosingNode == null) {
                if(isIncrementallyMatched(patternCall.getCalledPattern()))
                {	
            		IExecutionEnvironment executionEnvironment = new ExecutionEnvironment(patternMatcher.getModelManager().getRoot().getModelSpace().getFramework());
            		try {
            			IPatternMatcher patternMatcherInc = null;
            			patternMatcherInc =  PatternMatcherProvider.getInstance().getPatternMatcher(executionEnvironment, patternCall.getCalledPattern());
            			PatternNode child = new PatternNodeIncremental(new PatternMatcherWrapper(patternMatcherInc,
            					patternMatcher.getLogger(),patternMatcher.getModelManager(),
            					patternMatcher.getTermHandler())
            			, this, patternCall);
                    	children[i] = new PatternReferenceNode(this,patternCall,child);
            		} catch (ViatraTransformationException e) {
            			// It is a Major bug if an exception is caught here. Means that an already incrementally matched pattern does not have a valid PatternMatcher!
            			String[] context = {patternCall.getCalledPattern().getName(),e.getMessage()};
            			throw new PatternMatcherCompileTimeException(
            					PatternMatcherErrorStrings.INTERNAL_INCREMENTALLY_MATCED_PATTERN_HAS_NO_PATTERNMATCHER
            					,context
            					,patternCall);
            		}
                
                }
                else
                {
            	PatternNode child = new PatternNode(patternMatcher, this, patternCall);
                children[i] = child.isRoot() 
                		? new PatternReferenceNode(this, patternCall, child) : child;
                }
            } else {
                children[i] = new PatternReferenceNode(this, patternCall, loopClosingNode);
            }
        }
    }
    
    /** Returns true if the input called pattern is incrementally matched
     * @param calledPattern The called pattern to be checked
     * @return Boolean true if incrementally checked
     * @throws PatternMatcherCompileTimeException
     */
    private boolean isIncrementallyMatched(GTPattern calledPattern) throws PatternMatcherCompileTimeException{
    	
    	EList<RuntimeAnnotation> rtAnnotationsMachine = calledPattern.getNamespace().getRuntimeAnnotations();
		boolean isMachineIncremental = false;
    	if (rtAnnotationsMachine != null && rtAnnotationsMachine.size() > 0) {
			for (RuntimeAnnotation an: rtAnnotationsMachine) {
				if ("@incremental".equals(an.getAnnotationName().toLowerCase())) 
					{
					isMachineIncremental = true;
					}			
				 else if ("@localsearch".equals(an.getAnnotationName()
						.toLowerCase()))
				 	{
					 isMachineIncremental = false;
				 	}
				}
    	}
		
    	EList<RuntimeAnnotation> rtAnnotationsPattern = calledPattern.getRuntimeAnnotations();
    	
    	if (rtAnnotationsPattern != null && rtAnnotationsPattern.size() > 0) {
			for (RuntimeAnnotation an: rtAnnotationsPattern) {
				if ("@incremental".equals(an.getAnnotationName().toLowerCase()))
					return true;
				
				if ("@localsearch".equals(an.getAnnotationName()
							.toLowerCase()))
					return false;
			}
		}
		return isMachineIncremental; //machine default is used
	}

	protected PatternNode causesRecursion(GTPattern patternToTest) {
        return parent.causesRecursion(patternToTest);
    }
    
    @Override
    protected boolean traverse(PatternVariantIterator token) {
        int size = children.length;
        assert index == 0 || index == size - 1;
        while (index >= 0 && index < size) {
            if (children[index].traverse(token)) {
                index++;
            } else {
                children[index].index = 0;
                index--;
            }
        }
        boolean result = (index == size);
        index--;
        return result;
    }
    
    public GTPatternBody getBody() {
        return body;
    }

    public VariableID getVariableID(String name) {
    	return new VariableID(parent.getPattern(), currentLocation, name);
    }
    
    public VariableID getVariableID(Variable variable) {
    	return new VariableID(parent.getPattern(), currentLocation, variable.getName());
    }
    
    public VariableID getVariableID(ModelElement element) {
        return new VariableID(parent.getPattern(), currentLocation, element.getName());
    }
    
    private BodyNode getCallerBody() {
    	return (BodyNode) parent.getParent();
    }
    
    public void addLocalVariables(FlattenedPattern pattern) {
        // Handling of local variables
        for (Iterator<PatternVariable> iter = body.getLocalVariables().iterator(); iter.hasNext();) {
            PatternVariable variable = iter.next();
            pattern.addVariable(getVariableID(variable));
        }
    }

    public void addFormalParameters(FlattenedPattern pattern) 
        throws PatternMatcherCompileTimeException {
        if (parent.isRoot()) {
            assert body.getHeader() == parent.getPattern();
        	GTPattern firstPattern = body.getHeader();
            List<PatternVariable> formalParameters = firstPattern.getSymParameters();
            int numberOfFormalParameters = formalParameters.size();
            for (Integer i = 0; i < numberOfFormalParameters; i++) {
                // TODO gervarro: name convention for local pattern declarations is missing
                pattern.addVariable(getVariableID(formalParameters.get(i)));
            }
            assert firstPattern.getSymParameters().size() == pattern.getFrameSize();
        } else {
            // Handling of pattern calls in FlattenedPatterns (i.e., parameter passing)
            Integer numberOfActualParameters = parent.getActualParameters().size();
            if (numberOfActualParameters == parent.getPattern().getSymParameters().size()) {
                for (int j = 0; j < numberOfActualParameters; j++) {
                    Term actualTerm = parent.getActualParameters().get(j);
                    PatternVariable formalParameter = (PatternVariable) parent.getPattern().getSymParameters().get(j);
                    if (actualTerm instanceof VariableReference) {
                        VariableReference varRef = (VariableReference) actualTerm;
                        PatternVariable actualParameter = (PatternVariable) varRef.getVariable();
                        Integer index = pattern.getIndex(getCallerBody().getVariableID(actualParameter));
                        pattern.setIndex(getVariableID(formalParameter), index);
                    } else {
                        // Based on the latest directive of Dani, terms are not allowed in inner pattern calls
                        String[] context = {""+j, parent.getPattern().getName()};
                    	throw new PatternMatcherCompileTimeException(
                    			PatternMatcherErrorStrings.NO_TERM_IN_PATTERN_CALLS
                    			,context
                    			,actualTerm);
                        /*
                        // Term evaluation
                        Integer index = pattern.addVariable(getVariableID(formalParameter));
                        TermHandler handler = pattern.getTermHandler();
                        AbstractTermCheckOperation operation = 
                            handler.getTermEvaluationOperation(parent.pattern, currentLocation, actualTerm, index);
                        pattern.addPreSearchPlanOperation(operation);
                        */
                    }
                }
            } else {
            	String[] context = {parent.getPattern().getName()};
                throw new PatternMatcherCompileTimeException(
                		PatternMatcherErrorStrings.INTERNAL_FORMAL_AND_ACTUAL_PARAMETER_MISMATCH
                		,context
                		,parent.getPattern());
            }
        }
    }

    public Collection<Pair> processVariableAssignments(FlattenedPattern pattern) 
        throws PatternMatcherCompileTimeException {
    	ArrayList<Pair> pairs = null;
    	List<PatternVariableAssignment> assigments = body.getVariableAssignments();
        if (assigments != null) {
        	pairs = new ArrayList<Pair>();
            for (int i = 0; i < assigments.size(); i++) {
                VariableID leftID = getVariableID(assigments.get(i).getLeftValue().getVariable());
                VariableID rightID = getVariableID(assigments.get(i).getRightValue().getVariable());
               
                int left = pattern.getIndex(leftID);
                int right = pattern.getIndex(rightID);
                
                //The variable assignment operation is handled here
                SearchGraphNode leftNode = pattern.getSearchGraph().getSearchNodes().get(left);
                SearchGraphNode rightNode = pattern.getSearchGraph().getSearchNodes().get(right);

                if(leftNode == null)
            	{
            	String[] context = {leftID.getFancyName()};
                throw new PatternMatcherCompileTimeException(
                		PatternMatcherErrorStrings.VARIABLE_VARIABLEASSIGMENT_MISSING
                		,context
                		,assigments.get(i));
            	}
            
                if(rightNode == null)
            	{//Errofull part
            	String[] context = {rightID.getFancyName()};
                throw new PatternMatcherCompileTimeException(
                		PatternMatcherErrorStrings.VARIABLE_VARIABLEASSIGMENT_MISSING
                		,context
                		,assigments.get(i));
            	}        
                
                pairs.add(pattern.addInjectivityExclusionPair(left, right));
                //pattern.removeInjectivityInclusionPair(left,right); 

                
                SearchGraphEdge edge = new SearchGraphEdge();
                SearchGraphEdge invedge = new SearchGraphEdge();

                edge.setVPMEdgeType(EdgeType.VARIABLE_ASSIGNMENT);
                edge.setOldWeight(ISearchGraph.VARIABLEASSIGNMENT_WEIGHT);
                edge.setWeight(ISearchGraph.VARIABLEASSIGNMENT_WEIGHT);
                edge.setSourceNode(leftNode);
                edge.setTargetNode(rightNode);
                edge.setSource(true);

                edge.setName(leftNode.getName() +" variable assignment " + rightNode.getName());

                invedge.setVPMEdgeType(EdgeType.VARIABLE_ASSIGNMENT);
                invedge.setOldWeight(ISearchGraph.VARIABLEASSIGNMENT_WEIGHT);
                invedge.setWeight(ISearchGraph.VARIABLEASSIGNMENT_WEIGHT);
                invedge.setSourceNode(rightNode);
                invedge.setTargetNode(leftNode);
                invedge.setSource(false);
                invedge.setName(rightNode.getName() +" INVERSE variable assignment " + leftNode.getName());
                invedge.setInverseEdge(invedge);

                rightNode.addSource(edge);
                leftNode.addSource(invedge);
                
                //traceability
                
                EdgeTraceabilityElement edgeTraceability = new EdgeTraceabilityElement(edge,assigments.get(i));
        		pattern.getSearchGraph().addTraceabilityElement(edge, edgeTraceability);
        	    
        	    //source inverse
        	    EdgeTraceabilityElement inverseEdgeTraceability = new EdgeTraceabilityElement(invedge,assigments.get(i));
        	    pattern.getSearchGraph().addTraceabilityElement(invedge, inverseEdgeTraceability);
            }
        }
      return pairs;
    }
    
    public Collection<Pair> processInjectivityAssignments(FlattenedPattern pattern) 
    throws PatternMatcherCompileTimeException {
    ArrayList<Pair> pairs= null;
    List<NonInjectivityConstraint> constraints = body.getNonInjectivityConstraints();
    if (constraints != null) {
    	pairs = new ArrayList<Pair>();
        for (int i = 0; i < constraints.size(); i++) {
            VariableID leftID = getVariableID(constraints.get(i).getLeftValue().getVariable());
            VariableID rightID = getVariableID(constraints.get(i).getRightValue().getVariable());
            int left = pattern.getIndex(leftID);
            int right = pattern.getIndex(rightID);
            pairs.add(pattern.addInjectivityInclusionPair(left, right));
       //     pattern.removeInjectivityExclusionPair(left, right); //have to remove from the Exclusion list as it is explicitly defined with the Injectivity assignment
        }
    }
    
    return pairs; 
    }
    
    public void generateElementInjectivityConstraints(FlattenedPattern flattenedPattern,
    		Collection<Pair> localAdditionalExclusionInjectivityPairs,
			Collection<Pair> localAdditionalInclusionInjectivityPairs) throws PatternMatcherCompileTimeException {
		
    	 HashSet<Integer> bodyPatternIndexes = new HashSet<Integer>();
    	 boolean isDistinctMatching = parent.getPattern().isDistinctMatching();
    	 
    	 //local variables
    	 for (Iterator<PatternVariable> iter = body.getLocalVariables().iterator(); iter.hasNext();) {
             PatternVariable variable = iter.next();
             Integer localVariableIndex = flattenedPattern.getIndex(getVariableID(variable));
             bodyPatternIndexes.add(localVariableIndex);
         }
    	 
    	 //symbolic parameters are already attached to their actual invocation parameters
    	 for (Iterator<PatternVariable> iter = parent.getPattern().getSymParameters().iterator(); iter.hasNext();) {
             PatternVariable formalParemeter = iter.next();
             Integer formalParameterIndex = flattenedPattern.getIndex(getVariableID(formalParemeter));
             if(!bodyPatternIndexes.add(formalParameterIndex))
            	 {
            	 String[] context = {formalParameterIndex.toString(),parent.getPattern().getName()};
            	 throw new PatternMatcherCompileTimeException( 
            			 PatternMatcherErrorStrings.INTERNAL_BODYNODE_INJECTIVITYCONSTRAINT_ALREADYUSED
            			 ,context
            			 ,body);
            	 }
         }
    	 
    	 for(Integer i: bodyPatternIndexes)
    		 for(Integer j: bodyPatternIndexes)
    		 	if(i < j)
    		 		{if(isDistinctMatching)
    		 			{
    		 			if(localAdditionalExclusionInjectivityPairs != null 
    		 					&& !localAdditionalExclusionInjectivityPairs.contains(new Pair(i,j)))
    		 			flattenedPattern.addInjectivityInclusionPair(i, j);
    		 			
    		 			}
    		 		else 
    		 			{
    		 			if(localAdditionalInclusionInjectivityPairs != null
    		 					&& !localAdditionalInclusionInjectivityPairs.contains(new Pair(i,j)))
    		 			flattenedPattern.addInjectivityExclusionPair(i, j);
    		 			
    		 			}
    		 		}
    	 
    	/* if(localAdditionalExclusionInjectivityPairs != null)
    		 for(Pair p: localAdditionalExclusionInjectivityPairs)
    			 flattenedPattern.removeInjectivityInclusionPair(p.getLeft(), p.getRight());
    	 
    	 if(localAdditionalInclusionInjectivityPairs != null)
    		 for(Pair p: localAdditionalInclusionInjectivityPairs)
    			 flattenedPattern.removeInjectivityExclusionPair(p.getLeft(), p.getRight());
    	*/
    	 
    	 
    	 /*for (int j = 0; j < parent.pattern.getSymParameters().size(); j++) {
                 Term actualTerm = parent.actualParameters.get(j);
                 if (actualTerm instanceof VariableReference) {
                     VariableReference varRef = (VariableReference) actualTerm;
                     PatternVariable actualParameter = (PatternVariable) varRef.getVariable();
                     Integer index = flattenedPattern.getIndex(getCallerBody().getVariableID(actualParameter));
                 }
    	 }*/
		
	}
    
    public void processCheckExpressions(FlattenedPattern pattern, Logger logger) {
        List<Term> checkExpressions = body.getCheckExpressions();
        if (checkExpressions != null) {
            ITermHandler handler = pattern.getTermHandler();
            if (handler != null) {
                for (int i = 0; i < checkExpressions.size(); i++) {
                    CheckOperation operation = 
                        handler.getTermCheckOperation(parent.getPattern(), currentLocation, checkExpressions.get(i));
                    pattern.addPostSearchPlanOperation(operation);
                }
            } else {
                logger.warning(PatternMatcherErrorStrings.NO_TERM_HANDLER);
            }
        }
    }

    public void processNegativeApplicationConditions(FlattenedPattern pattern, Logger logger, IModelManager manager) 
        throws PatternMatcherCompileTimeException {
        List<GTPatternCall> negativeCalls = body.getNegativePatterns();
        GTPattern header = body.getHeader();
        if (negativeCalls != null && negativeCalls.size() > 0) {
            for (int i = 0; i < negativeCalls.size(); i++) {
                GTPatternCall call = negativeCalls.get(i);
                PatternBuilder builder = new PatternBuilder(logger, manager, pattern.getTermHandler());
                IPatternMatcher matcher = builder.construct(call.getCalledPattern());
                List<Term> actualTerms = call.getActualParameters();
                Collection<Variable> passingVariables = new ArrayList<Variable>();
                
                int[] actualParameterMapping = new int[actualTerms.size()];
                for (int j = 0; j < actualTerms.size(); j++) {
                    Term term = actualTerms.get(j);
                    if (term instanceof VariableReference) {
                        VariableReference varRef = (VariableReference) term;
                        actualParameterMapping[j] = 
                            pattern.getIndex(getVariableID(varRef.getVariable()));
                        
                        if(header.getSymParameters().contains(varRef.getVariable())) //it is a variable that goes into the NAC call
                        	passingVariables.add(varRef.getVariable());
                    
                    } else {
                    	String[] context = {""+j,call.getCalledPattern().getName()};
                        throw new PatternMatcherCompileTimeException(
                                PatternMatcherErrorStrings.NO_TERM_IN_NAC_CALLS
                                ,context
                                ,call);
                    }
                }
                
                NACCheckOperation operation = new NACCheckOperation(matcher, actualParameterMapping,call,
                			passingVariables);
                pattern.addPostSearchPlanOperation(operation);
            }
        }
    }
    
    public void buildSearchGraph(FlattenedPattern result) throws PatternMatcherCompileTimeException{
		try{
    		result.getSearchGraph().add(this,result);
		}catch (PatternMatcherCompileTimeException e) {
			throw e.addNewStackElement(this.body);
		}
	}

    public String toString() {
        return getClass().getSimpleName() + " " + parent.getPattern().getName() + "_" + currentLocation;
    }

    public CheckOperation getTermEvaluationOperation(ITermHandler handler, ContainmentConstraint conCons, int resultSlot) {
    	return handler.getTermEvaluationOperation(parent.getPattern(), currentLocation, conCons, resultSlot);
    }
	
}