package jcircus.newutil;

import java.util.ArrayList;
import java.util.List;
import java.util.Vector;

import jcircus.anns.MuCallAnn;
import jcircus.parallelism.Consumer;
import net.sourceforge.czt.circus.ast.Action1;
import net.sourceforge.czt.circus.ast.Action2;
import net.sourceforge.czt.circus.ast.AssignmentCommand;
import net.sourceforge.czt.circus.ast.AssignmentPairs;
import net.sourceforge.czt.circus.ast.BasicAction;
import net.sourceforge.czt.circus.ast.CallAction;
import net.sourceforge.czt.circus.ast.CircusAction;
import net.sourceforge.czt.circus.ast.CircusActionList;
import net.sourceforge.czt.circus.ast.CircusCommand;
import net.sourceforge.czt.circus.ast.CircusFieldList;
import net.sourceforge.czt.circus.ast.CircusProcess;
import net.sourceforge.czt.circus.ast.Communication;
import net.sourceforge.czt.circus.ast.DotField;
import net.sourceforge.czt.circus.ast.Field;
import net.sourceforge.czt.circus.ast.GuardedAction;
import net.sourceforge.czt.circus.ast.IfGuardedCommand;
import net.sourceforge.czt.circus.ast.ParamAction;
import net.sourceforge.czt.circus.ast.PrefixingAction;
import net.sourceforge.czt.circus.ast.VarDeclCommand;
import net.sourceforge.czt.circus.util.Factory;
import net.sourceforge.czt.z.ast.AndPred;
import net.sourceforge.czt.z.ast.ApplExpr;
import net.sourceforge.czt.z.ast.ConstDecl;
import net.sourceforge.czt.z.ast.Decl;
import net.sourceforge.czt.z.ast.Expr;
import net.sourceforge.czt.z.ast.FalsePred;
import net.sourceforge.czt.z.ast.MemPred;
import net.sourceforge.czt.z.ast.NegPred;
import net.sourceforge.czt.z.ast.NumExpr;
import net.sourceforge.czt.z.ast.OrPred;
import net.sourceforge.czt.z.ast.Pred;
import net.sourceforge.czt.z.ast.ProdExpr;
import net.sourceforge.czt.z.ast.RefExpr;
import net.sourceforge.czt.z.ast.SetExpr;
import net.sourceforge.czt.z.ast.Spec;
import net.sourceforge.czt.z.ast.TruePred;
import net.sourceforge.czt.z.ast.TupleExpr;
import net.sourceforge.czt.z.ast.VarDecl;
import net.sourceforge.czt.z.ast.ZDeclList;
import net.sourceforge.czt.z.ast.ZExprList;
import net.sourceforge.czt.z.ast.ZNameList;

public class ExprUtil {
	public static int sizeOfExpression (Expr expr) {
		if (expr instanceof RefExpr) {
			String name = ((RefExpr)expr).getZName().toString();
			if (name.equals ("$$SYNCH")) {
				return 0;
			}
			return 1;
		}
		else if (expr instanceof ProdExpr) {
			ZExprList exprlist = ((ProdExpr)expr).getZExprList();
			return exprlist.size();
		}
		else {
			ExceptionUtil.throwImplementationException ("ExprUtil.sizeOfExpression", expr.getClass());
			return 0;
		}
	}
	public static ZExprList fromVectorToRefExpr (Vector <String> names) {
		Factory f = new Factory ();
		ZExprList returnexprs = f.createZExprList();
		int size = names.size();
		for (int i = 0; i < size; i++) {
			returnexprs.add(f.createRefExpr(f.createZName(names.elementAt(i))));
		}
		return returnexprs;
	}
	public static boolean exprContainsName (Expr expr, String name) {
		if (expr instanceof RefExpr) {
			String exprname = ((RefExpr)expr).getZName().toString();
			if (exprname.equals(name)) {
				return true;
			}
			else {
				return false;
			}
		}
		else if (expr instanceof NumExpr) {
			return false; //Isto ocorre porque o nome do parâmetro não pode ser igual a uma expressão numérica
		}
		else if (expr instanceof TupleExpr) {
			boolean aux = false;
			ZExprList tupleexprs = ((TupleExpr)expr).getZExprList();
			int size = tupleexprs.size();
			for (int i = 0; i < size; i++) {
				aux = aux || exprContainsName (tupleexprs.get(i), name);
			}
			return aux;
		}
		else if (expr instanceof SetExpr) {
			boolean aux = false;
			ZExprList exprlist = ((SetExpr)expr).getZExprList();
			int size = exprlist.size();
			for (int i = 0; i < size; i++) {
				Expr expri = exprlist.get(i);
				aux = aux || exprContainsName (expri, name);
			}
			return aux;
		}
		else if (expr instanceof ApplExpr) {
			return exprContainsName (((ApplExpr)expr).getRightExpr(), name);
		}
		else /*if (expr instanceof ApplExpr)*/ {
			ExceptionUtil.throwException("ExprUtil" + ".exprContainsName :: " + "this method does not have a implementation for " + expr.getClass() + ". Why not implementing it now? ;)");
			return false;
		}
	}

	public static Expr updateExpr (String namevar, Expr newExpr, Expr targetExpr) {
		/**
		 * Atualiza o valor de uma variável em uma expressão.
		 * Verifica se uma expressão-alvo (targetExpr) possui uma dada variável (namevar), e se a expressão-alvo tiver a variável, 
		 * Substitui a chamada da variável na expressão-alvo pela nova expressão (newExpr).
		 * Por exemplo, supomos que temos a expressão x + y e queremos substituir x por 5. 
		 * Neste caso, x + y é a expressão-alvo (targetExpr),
		 * x é a variável que queremos que seja substituída (namevar),
		 * e 5 é a nova expressão (newExpr). Neste caso, updateExpr retornará x + 5
		*/
		Factory f = new Factory ();
		FactoryUtil fu = new FactoryUtil ();
		if (targetExpr instanceof RefExpr) {
			String nametargetexpr = ((RefExpr)targetExpr).getName().toString();
			Expr returnnewexpr = fu.createExpr (newExpr);
			Expr returntargetexpr = fu.createExpr (targetExpr);
			if (namevar.equals(nametargetexpr)) {
				return returnnewexpr;
			}
			else {
				return returntargetexpr;
			}
		}
		else if (targetExpr instanceof ApplExpr) {
			ApplExpr appl = (ApplExpr) fu.createExpr ((ApplExpr)targetExpr);
			appl.setRightExpr(updateExpr (namevar, newExpr, ((ApplExpr) targetExpr).getRightExpr()));
			return appl;
		}
		else if (targetExpr instanceof TupleExpr) {
			ZExprList exprList = fu.createZExprList (((TupleExpr)targetExpr).getZExprList());
			for (int i = 0; i < exprList.size(); i++) {
				exprList.set(i, updateExpr (namevar, newExpr, exprList.get(i)));
			}
			TupleExpr tupleexpr = f.createTupleExpr();
			tupleexpr.setExprList(exprList);
			return tupleexpr;
		}
		else if (targetExpr instanceof NumExpr) {
			/**
			 * Uma variável nunca pode ser encontrada numa NumExpr...
			 * */
			return fu.createExpr (targetExpr);
		}
		//else if () {} //OUTROS TIPOS DE EXPRESSÃO?
		else {
			ExceptionUtil.throwImplementationException ("ExprUtil.updateExpr", targetExpr.getClass());
			return fu.createExpr (targetExpr);
		}
	}
	public static Expr updateExpr (List <VarDecl> decls, ZExprList newExprs, Expr targetExpr) {
		Factory f = new Factory ();
		int size1 = decls.size();
		Expr oldexprAux = f.createRefExpr();
		for (int i = 0; i < size1; i++) {
			oldexprAux = ExprUtil.updateExpr (decls.get(i).getName().toString(), newExprs.get(i), targetExpr);
		}
		return oldexprAux;
	}

	protected static boolean areTheSameExpr (Expr expr1, Expr expr2) {
		if (expr1 instanceof RefExpr && expr2 instanceof RefExpr) {
			String name1 = ((RefExpr)expr1).getZName().toString();
			String name2 = ((RefExpr)expr2).getZName().toString();
			if (name1.equals(name2)) {
				return true;
			}
			else {
				return false;
			}
		}
		else {
			return false;
		}
	}

	public static CircusAction updateExpression (List <VarDecl> decls, ZExprList paramExprs, CircusAction action, CircusProcess process, Spec spec) {
		CircusAction action2;
		action2 = ExprUtil.actionWithUpdatedExpression (decls, paramExprs, action, process, spec);
		return action2;
	}
	/*public static CircusAction actionWithUpdatedExpression (ZDeclList decls, CircusAction action) {
		Factory f = new Factory ();
		ZExprList refexprlist = f.createZExprList();
		int size = decls.size();
		int counter = 0;
		for (int i = 0; i < size; i++) {
			Decl decl = decls.get(i);
			if (decl instanceof VarDecl) {
				VarDecl vardecl = (VarDecl)decl;
				ZNameList names = vardecl.getZNameList();
				int namessize = names.size();
				for (int j = 0; j < namessize; j++) {
					refexprlist.add(f.createRefExpr(f.createZName(names.get(j).toString())));
				}
			}
		}
		return actionWithUpdatedExpression (decls, refexprlist, action);
	}*/
	public static Vector <String> pActname2Vector (int n, String actionname) {
		Vector <String> names = new Vector <String> ();
		for (int i = 0; i < n; i++) {
			names.addElement ("p" + actionname + i);
		}
		return names;
	}
	public static ZExprList pActname2ExprList (int n, String actionname) {
		Vector <String> names = pActname2Vector (n, actionname);
		return fromVectorToRefExpr (names);
	}
	//actionWithUpdatedExpression (ZDeclList decls, ZExprList paramExprs, CircusAction action)
	//actionWithUpdatedExpression (decls2beupdated, pActname2ExprList (decls2beupdated.size(), ((CallAction)action).getName().toString()), updatedContent);
	public static CircusAction actionWithUpdatedExpression (List <VarDecl> decls, ZExprList paramExprs, CircusAction action, CircusProcess process, Spec spec) {
		return actionWithUpdatedExpression (decls, paramExprs, action, process, spec, new Vector <String> (), new Vector <String> (), new Consumer (new Vector <String> ()));
	}
	public static CircusAction actionWithUpdatedExpression (ZDeclList decls, ZExprList paramExprs, CircusAction action, CircusProcess process, Spec spec, Vector <String> mus, Vector <String> actionNames, Consumer c) {
		List <VarDecl> listdecls = new ArrayList <VarDecl> ();
		int size = decls.size();
		for (int i = 0; i < size; i++) {
			Decl decl = decls.get(i);
			if (decl instanceof VarDecl)
				listdecls.add((VarDecl)decl);
		}
		return actionWithUpdatedExpression (listdecls, paramExprs, action, process, spec, mus, actionNames, c);
	}
	public static Pred predWithUpdatedExpressions (List <VarDecl> decls, ZExprList paramExprs, Pred pred, CircusProcess process, Spec spec, Vector <String> mus, Vector <String> actionNames, Consumer c) {
		Factory f = new Factory ();
		FactoryUtil fu = new FactoryUtil ();
		if (pred instanceof NegPred) {
			NegPred negpred = f.createNegPred ();
			negpred.setPred(predWithUpdatedExpressions (decls, paramExprs, ((NegPred) pred).getPred(), process, spec, mus, actionNames, c));
			negpred.getAnns().addAll(pred.getAnns());
			return negpred;
		}
		else if (pred instanceof TruePred) {
			return f.createTruePred();
		}
		else if (pred instanceof FalsePred) {
			return f.createFalsePred ();
		}
		else if (pred instanceof AndPred) {
			AndPred andpred = f.createAndPred();
			andpred.setAnd(((AndPred) pred).getAnd());
			andpred.setLeftPred(fu.createPred(((AndPred) pred).getLeftPred()));
			andpred.setRightPred(fu.createPred(((AndPred) pred).getRightPred()));
			return andpred;
		}
		else if (pred instanceof OrPred) {
			OrPred orpred = f.createOrPred();
			orpred.setLeftPred(fu.createPred(((OrPred) pred).getLeftPred()));
			orpred.setRightPred(fu.createPred(((OrPred) pred).getRightPred()));
			return orpred;
		}
		else if (pred instanceof MemPred) {
			MemPred mempred = f.createMemPred();
			mempred.setMixfix(((MemPred) pred).getMixfix());
			
			Expr leftexpr = ((MemPred) pred).getLeftExpr();
			Expr rightexpr = ((MemPred) pred).getRightExpr();

			Expr newleftexpr = fu.createExpr(leftexpr);
			Expr newrightexpr = fu.createExpr (rightexpr);
			
			Vector <String> vectordecls = DeclUtil.declListAsVector(DeclUtil.listVarDeclAsDeclList (decls));
			
			int size = vectordecls.size();

			for (int i = 0; i < size; i++) {
				Expr currentexpr = paramExprs.get(i);
				if (exprContainsName (leftexpr, vectordecls.elementAt(i))) {
					newleftexpr = fu.createExpr(updateExpr (vectordecls.elementAt(i), paramExprs.get(i), leftexpr));
				}
				if (exprContainsName (rightexpr, vectordecls.elementAt(i))) {
					newrightexpr = fu.createExpr(updateExpr (vectordecls.elementAt(i), paramExprs.get(i), rightexpr));
				}
			}
			
			System.out.println ("Old left: " + PrinterUtil.printExpression(leftexpr));
			System.out.println ("Old right: " + PrinterUtil.printExpression(rightexpr));
			System.out.println ("New left: " + PrinterUtil.printExpression(newleftexpr));
			System.out.println ("New right: " + PrinterUtil.printExpression(newrightexpr));
			
			mempred.setLeftExpr (newleftexpr);
			mempred.setRightExpr (newrightexpr);
			
			return mempred;
		}
		else {
			ExceptionUtil.throwImplementationException ("ExprUtil.predWithUpdatedExpression", pred.getClass());
			return f.createTruePred();
		}
	}
	public static CircusAction actionWithUpdatedExpression (List <VarDecl> decls, ZExprList paramExprs, CircusAction action, CircusProcess process, Spec spec, Vector <String> mus, Vector <String> actionNames, Consumer c) {
		Factory f = new Factory ();
		FactoryUtil fu = new FactoryUtil ();
		CircusAction auxaction = ParamUtil.pf.createCircusAction (action);
		if (auxaction instanceof ParamAction) {
			CircusAction action2 = ((ParamAction)auxaction).getCircusAction();
			ParamAction returnaction = f.createParamAction();
			returnaction.setDeclList(((ParamAction) auxaction).getZDeclList());
			returnaction.setCircusAction(actionWithUpdatedExpression (decls, paramExprs, action2, process, spec, mus, actionNames, c));
			return returnaction;
		}
		else if (auxaction instanceof CircusCommand) {
			if (auxaction instanceof AssignmentCommand) {
				AssignmentPairs assPairs = (new Factory ()).createAssignmentPairs(((AssignmentCommand)auxaction).getAssignmentPairs().getLHS(), ((AssignmentCommand)auxaction).getAssignmentPairs().getRHS());
				ZExprList exprList = assPairs.getZRHS();
				ZExprList finalExprList = (new Factory ()).createZExprList();
				int counter = 0;
				for (int i = 0; i < exprList.size(); i++) {
					Decl decl = decls.get(i);
					if (decl instanceof VarDecl) {
						ZNameList namelist = ((VarDecl)decl).getZNameList();
						for (int j = 0; j < namelist.size(); j++) {
							if (exprContainsName (exprList.get(i), namelist.get(j).toString())) {
								System.out.println (PrinterUtil.printExpression (exprList.get(i)));
								finalExprList.add(updateExpr (namelist.get(j).toString(), paramExprs.get(counter), exprList.get(i)));
								System.out.println (PrinterUtil.printExpression (exprList.get (i)));
								System.out.println (PrinterUtil.printExpression (finalExprList.get(counter)));
								System.out.print ("");
							}
							else {
								finalExprList.add(exprList.get(j));
							}
							counter++;
						}
					}
					/*if (exprContainsName (exprList.get(i), decls.get(i).getName().toString())) {
						finalExprList.add(updateExpr (decls.get(i).getName().toString(), paramExprs.get(i), exprList.get(i)));
					}
					else {
						finalExprList.add(exprList.get(i));
					}*/
				}
				assPairs.setRHS(finalExprList/*exprList*/);
				((AssignmentCommand)auxaction).setAssignmentPairs(assPairs);
				return auxaction;
			}
			else if (auxaction instanceof IfGuardedCommand) {
				int size = ((IfGuardedCommand)auxaction).getNumberOfGuards();
				CircusActionList al = ((IfGuardedCommand)auxaction).getGuardedActionList();
				for (int i = 0; i < size; i++) {
					CircusAction act = al.get(i);
					act = actionWithUpdatedExpression (decls, paramExprs, al.get(i), process, spec, mus, actionNames, c);
					al.set(i, act);
				}
				((IfGuardedCommand)auxaction).setActionList(al);
				System.out.print ("");
				return auxaction;
			}
			else if (auxaction instanceof VarDeclCommand) {
				VarDeclCommand vdc = f.createVarDeclCommand();
				vdc.setDeclList(((VarDeclCommand)auxaction).getZDeclList());
				vdc.setCircusAction(actionWithUpdatedExpression (decls, paramExprs, ((VarDeclCommand)auxaction).getCircusAction(), process, spec, mus, actionNames, c));
				return vdc;
			}
			else {
				ExceptionUtil.throwImplementationException("actionWithUpdatedExpression", auxaction.getClass());
				return auxaction;
			}
			//return auxaction;
		}
		else if (auxaction instanceof Action2) {
			Action2 action2 = (Action2)auxaction;
			action2.setLeftAction(actionWithUpdatedExpression (decls, paramExprs, action2.getLeftAction(), process, spec, mus, actionNames, c));
			action2.setRightAction (actionWithUpdatedExpression (decls, paramExprs, action2.getRightAction(), process, spec, mus, actionNames, c));
			return action2;
		}
		else if (auxaction instanceof PrefixingAction) {
			Communication comm = ((PrefixingAction)auxaction).getCommunication();
			CircusFieldList cfl = comm.getCircusFieldList();
			int size = cfl.size();
			int counter = 0;
			for (int i = 0; i < size; i++) {
				Field field = cfl.get(i);
				if (field instanceof DotField) {
					DotField dotfield = (DotField)field;
					Expr target = dotfield.getExpr();
					int declssize = decls.size();
					for (int j = 0; j < declssize; j++) {
						int namelistsize = 0;
						if (decls.get(j) instanceof VarDecl) {
							namelistsize = ((VarDecl)decls.get(j)).getZNameList().size();
							ZNameList namelist = ((VarDecl)decls.get(j)).getZNameList();
							for (int k = 0; k < namelistsize; k++) {
								boolean exprContainsName = exprContainsName (target, ((VarDecl)decls.get(j)).getZNameList().get(k).toString());
								if (exprContainsName (target, ((VarDecl)decls.get(j)).getZNameList().get(k).toString())) {
									dotfield.setExpr(updateExpr (namelist.get(k).toString(), paramExprs.get(counter), target));
									counter++;
								}
							}
						}
						else if (decls.get(j) instanceof ConstDecl) {
							namelistsize = 1;
							if (exprContainsName (target, ((ConstDecl)decls.get(j)).getZName().toString())) {
								dotfield.setExpr(updateExpr (((ConstDecl)decls.get(j)).getZName().toString(), paramExprs.get(counter), target));
								counter++;
							}
						}
						else {
							ExceptionUtil.throwImplementationException("actionWithUpdatedExpression", decls.get(j).getClass());
						}
						/*
						for (int k = 0; k < namelistsize; k++) {
							if (exprContainsName (target, decls.get(j).getName().toString())) {
								dotfield.setExpr(updateExpr (decls.get(i).getName().toString(), paramExprs.get(i), target));
							}
						}
						*/
					}
					field = dotfield;
				}
				cfl.set(i, field);
			}
			comm.setFieldList(cfl);
			((PrefixingAction)auxaction).setCommunication(comm);
			((PrefixingAction)auxaction).setCircusAction(actionWithUpdatedExpression (decls, paramExprs, ((PrefixingAction) auxaction).getCircusAction(), process, spec, mus, actionNames, c));
			return auxaction;
		}
		if (auxaction instanceof GuardedAction) {
			Pred pred = ((GuardedAction)auxaction).getPred();
			Pred updatedpred = predWithUpdatedExpressions (decls, paramExprs, pred, process, spec, mus, actionNames, c);
			Pred newpred = fu.createPred (updatedpred);
			GuardedAction ga = f.createGuardedAction();
			ga.setPred(newpred);
			ga.setCircusAction(actionWithUpdatedExpression (decls, paramExprs, ((GuardedAction)auxaction).getCircusAction(), process, spec, mus, actionNames, c));
			return ga;
		}
		else if (auxaction instanceof Action1) {
			Action1 action1 = (Action1)auxaction;
			action1.setCircusAction(actionWithUpdatedExpression (decls, paramExprs, action1.getCircusAction(), process, spec, mus, actionNames, c));
			return action1;
		}
		else if (auxaction instanceof CallAction) {
			if (auxaction.getAnn(MuCallAnn.class) == null) {
				ZExprList callexprs = ((CallAction)auxaction).getZExprList();
				CircusAction auxcontentaction =
						fu.createCircusAction (CallUtil.getContentOfCallAction((CallAction)auxaction, process, spec));
				if (callexprs.size() > 0 && auxcontentaction != null) {
					ZDeclList auxcontentdecls = ((ParamAction)auxcontentaction).getZDeclList();
					ZExprList newlist = f.createZExprList ();
					Vector <String> commondecls = DeclUtil.commonDecls (DeclUtil.listVarDeclAsDeclList (decls), auxcontentdecls);
					Vector <String> auxcontentdeclsvector = DeclUtil.declListAsVector(auxcontentdecls);
					int size = auxcontentdeclsvector.size();
					int counter = 0;
					for (int i = 0; i < size; i++) {
						if (commondecls.contains(auxcontentdeclsvector.get(i))) {
							Expr expr = updateExpr (auxcontentdeclsvector.get(i), paramExprs.get(i), callexprs.get(i));
							newlist.add(fu.createExpr(expr));
							counter++;
						}
						else {
							newlist.add(fu.createExpr(callexprs.get(i)));
						}
					}
					CallAction ca = f.createCallAction ();
					ca.setName(((CallAction)auxaction).getZName());
					ca.setExprList(newlist);
					return ca;
				}
			}
			return auxaction;
		}
		else if (auxaction instanceof BasicAction) {
			return auxaction;
		}
		else {
			ExceptionUtil.throwImplementationException("ExprUtil.actionWithUpdatedExpression", auxaction.getClass());
			return auxaction;
		}
	}
/***USADO EM CCUPDATER***/
	public static void replaceVarName (String targetVar, String newName, Expr expr) {
		replaceVarName (targetVar, newName, expr, "");
	}
	public static void replaceVarName (String targetVar, String newName, Expr expr, String processname) {
		Factory f = new Factory ();
		if (expr instanceof RefExpr) {
			String exprName = ((RefExpr)expr).getName().toString();
			if (exprName.equals(targetVar)) {
				((RefExpr)expr).setName(f.createZName(newName));
			}
		}
		else if (expr instanceof ApplExpr) {
			Expr left = ((ApplExpr)expr).getLeftExpr();
			Expr right = ((ApplExpr)expr).getRightExpr();
			replaceVarName (targetVar, newName, left, processname);
			replaceVarName (targetVar, newName, right, processname);
		}
		else if (expr instanceof TupleExpr) {
			ZExprList exprlist = ((TupleExpr)expr).getZExprList();
			int size = exprlist.size();
			for (int i = 0; i < size; i++) {
				replaceVarName (targetVar, newName, exprlist.get(i), processname);
			}
		}
		else if (expr instanceof NumExpr) {
			//Nothing to do
		}
		else {
			ExceptionUtil.throwImplementationException("ExprUtil.replaceVarName", expr.getClass());
		}
	}
}