package jcircus.newutil;

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

import jcircus.anns.MuCallAnn;

import net.sourceforge.czt.circus.ast.Action1;
import net.sourceforge.czt.circus.ast.Action2;
import net.sourceforge.czt.circus.ast.ActionPara;
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.BasicProcess;
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.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.InputField;
import net.sourceforge.czt.circus.ast.MuAction;
import net.sourceforge.czt.circus.ast.ParamAction;
import net.sourceforge.czt.circus.ast.ParamProcess;
import net.sourceforge.czt.circus.ast.PrefixingAction;
import net.sourceforge.czt.circus.ast.Process1;
import net.sourceforge.czt.circus.ast.Process2;
import net.sourceforge.czt.circus.ast.VarDeclCommand;
import net.sourceforge.czt.z.ast.AndPred;
import net.sourceforge.czt.z.ast.AxPara;
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.InclDecl;
import net.sourceforge.czt.z.ast.MemPred;
import net.sourceforge.czt.z.ast.NegPred;
import net.sourceforge.czt.z.ast.OrPred;
import net.sourceforge.czt.z.ast.Para;
import net.sourceforge.czt.z.ast.Pred;
import net.sourceforge.czt.z.ast.Spec;
import net.sourceforge.czt.z.ast.TruePred;
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.ZName;
import net.sourceforge.czt.z.ast.ZNameList;
import net.sourceforge.czt.z.ast.ZParaList;
import net.sourceforge.czt.z.ast.ZSchText;

/**Author: Samuel Barrocas (created in 13/06/2013)
 * It works as an auxiliary util for determining if a variable is on the scope of a process...
 *
 * */

public class ScopeUtil {
	private static boolean variableIsInsideExpression (String var, Expr expr, Vector <String> inputFieldVariables) {
		if (inputFieldVariables.contains(var)) {
			return false;
		}
		return ExprUtil.exprContainsName(expr, var);
	}
	private static boolean variableIsInsideZExprList (String var, ZExprList exprlist, Vector <String> inputFieldVariables) {
		int size = exprlist.size();
		boolean aux = false;
		for (int i = 0; i < size; i++) {
			aux = aux || variableIsInsideExpression (var, exprlist.get(i), inputFieldVariables);
		}
		return aux;
	}
	private static boolean variableIsInsideZName (String var, ZName name) {
		if (name.toString().equals(var))
			return true;
		return false;
	}
	private static boolean variableIsInsideZNameList (String var, ZNameList namelist) {
		int size = namelist.size();
		boolean aux = false;
		for (int i = 0; i < size; i++) {
			ZName name = (ZName) namelist.get(i);
			aux = aux || variableIsInsideZName (var, name);
		}
		return aux;
	}
	private static boolean variableIsInsideDecl (String var, Decl decl, Vector <String> inputFieldVariables) {
		if (decl instanceof VarDecl) {
			ZNameList namelist = ((VarDecl)decl).getZNameList();
			Expr expr = ((VarDecl)decl).getExpr();
			return variableIsInsideZNameList (var, namelist) || variableIsInsideExpression (var, expr, inputFieldVariables);
		}
		else if (decl instanceof ConstDecl) {
			Expr expr = ((ConstDecl)decl).getExpr();
			ZName name = ((ConstDecl)decl).getZName();
			return variableIsInsideZName (var, name) || variableIsInsideExpression (var, expr, inputFieldVariables);
		}
		else if (decl instanceof InclDecl) {
			return variableIsInsideExpression (var, ((InclDecl)decl).getExpr(), inputFieldVariables);
		}
		//else if () {} //mais algum??
		else {
			ExceptionUtil.throwException ("ScopeUtil.variableIsInsideDecl method: there is no translation to this Decl declaration...");
			return false;
		}
	}
	private static boolean variableIsInsideZDeclList (String var, ZDeclList decllist, Vector <String> inputFieldVariables) {
		int size = decllist.size();
		boolean aux = false;
		for (int i = 0; i < size; i++) {
			aux = aux || variableIsInsideDecl (var, decllist.get(i), inputFieldVariables);
		}
		return aux;
	}
	private static boolean variableIsInsidePred (String var, Pred pred, Vector <String> inputFieldVariables) {
		if (pred instanceof MemPred) {
			boolean left = variableIsInsideExpression (var, ((MemPred)pred).getLeftExpr(), inputFieldVariables);
			boolean right = variableIsInsideExpression (var, ((MemPred)pred).getRightExpr(), inputFieldVariables);
			return left || right;
		}
		else if (pred instanceof OrPred) {
			Pred left = ((OrPred)pred).getLeftPred();
			Pred right = ((OrPred)pred).getRightPred();
			return 
					variableIsInsidePred (var, left, inputFieldVariables) 
					|| variableIsInsidePred (var, right, inputFieldVariables);
		}
		else if (pred instanceof AndPred) {
			Pred left = ((AndPred)pred).getLeftPred();
			Pred right = ((AndPred)pred).getRightPred();
			return 
					variableIsInsidePred (var, left, inputFieldVariables) 
					|| variableIsInsidePred (var, right, inputFieldVariables);
		}
		else if (pred instanceof TruePred || pred instanceof FalsePred) {
			return false;
		}
		else if (pred instanceof NegPred) {
			return variableIsInsidePred (var, ((NegPred)pred).getPred(), inputFieldVariables);
		}
		else {
			ExceptionUtil.throwException("ScopeUtil.variableIsInsidePred: Does not accept the predicate " + pred.getClass() + ". Why not implementing it for this method? ;)");
			return false;
		}
	}
	public static boolean variableIsInsideAction (String var, CircusAction action, BasicProcess process, Spec spec) {
		return variableIsInsideAction (var, action, process, new Vector <String> (), new Vector <String> (), spec);
	}
	private static boolean variableIsInsideAction (String var, CircusAction action, BasicProcess process, Vector <String> calls, Vector <String> inputFieldVariables, Spec spec) {
		if (action instanceof CircusCommand) {
			return variableIsInsideCommand (var, (CircusCommand)action, process, calls, inputFieldVariables, spec);
		}
		else if (action instanceof Action2) {
			CircusAction left = ((Action2)action).getLeftAction();
			CircusAction right = ((Action2)action).getRightAction();
			return
					variableIsInsideAction (var, left, process, calls, inputFieldVariables, spec)
					|| variableIsInsideAction (var, right, process, calls, inputFieldVariables, spec);
		}
		/*else if (action instanceof Action1) {
			CircusAction getaction = ((Action1)action).getCircusAction();
			return variableIsInsideAction (var, getaction, process, calls);
		}*/
		else if (action instanceof GuardedAction) {
			Pred pred = ((GuardedAction)action).getPred();
			boolean isonpred = variableIsInsidePred (var, pred, inputFieldVariables);
			boolean isonaction = variableIsInsideAction (var, ((GuardedAction)action).getCircusAction(), process, calls, inputFieldVariables, spec);
			return isonpred || isonaction;
		}
		else if (action instanceof ParamAction) {
			CircusAction circusaction = ((ParamAction)action).getCircusAction();
			ZDeclList decls = ((ParamAction)action).getZDeclList();
			return 
					variableIsInsideAction (var, circusaction, process, calls, inputFieldVariables, spec)
					&& !variableIsInsideZDeclList (var, decls, inputFieldVariables)
					;
		}
		else if (action instanceof PrefixingAction) {
			CircusFieldList cfl = ((PrefixingAction)action).getCommunication().getCircusFieldList();
			CircusAction prefixed = ((PrefixingAction)action).getCircusAction ();
			int cflsize = cfl.size();
			boolean aux = false;
			for (int i = 0; i < cflsize; i++) {
				Field field = cfl.get(i);
				if (field instanceof InputField) {
					aux = false;
					ZName name = ((InputField)field).getVariableZName();
					inputFieldVariables.addElement(name.toString());
					//aux = aux || variableIsInsideZName (var, name);
				}
				else if (field instanceof DotField) {
					Expr expr = ((DotField)field).getExpr();
					aux = aux || variableIsInsideExpression (var, expr, inputFieldVariables);
				}
			}
			return aux || variableIsInsideAction (var, prefixed, process, calls, inputFieldVariables, spec);
		}
		else if (action instanceof BasicAction) {
			return false;
		}
		else if (action instanceof MuAction) {
			CircusAction cact = ((MuAction)action).getCircusAction();
			ZName name = ((MuAction)action).getZName();
			Vector <String> vec = new Vector <String> (calls);//.add(name.toString());
			vec.add(name.toString());
			return variableIsInsideAction (var, cact, process, vec, inputFieldVariables, spec);
		}
		else if (action instanceof CallAction) {
			if (calls.contains(((CallAction)action).getZName().toString())) {
				return false;
			}
			if (action.getAnn(MuCallAnn.class) != null) {
				return false;
			}
			Vector <String> newcalls = new Vector <String> ();
			newcalls.addAll(calls);
			newcalls.addElement(((CallAction)action).getZName().toString());
			return variableIsInsideAction (var, CallUtil.getContentOfCallAction((CallAction)action, process, spec), process, newcalls, inputFieldVariables, spec);
			//return false;
		}
		else {
			if (action == null) {
				ExceptionUtil.throwException ("ScopeUtil.variableIsInsideAction: null action!");
			}
			ExceptionUtil.throwException ("ScopeUtil.variableIsInsideAction: Still cannot return for " + action.getClass());
			return false;
		}
	}
	private static boolean variableIsInsideCommand (String var, CircusCommand command, BasicProcess process, Vector <String> calls, Vector <String> inputFieldVariables, Spec spec) {
		if (command instanceof AssignmentCommand) {
			AssignmentPairs asspairs = ((AssignmentCommand)command).getAssignmentPairs();
			return
					variableIsInsideZNameList (var, asspairs.getZLHS())
					|| variableIsInsideZExprList (var, asspairs.getZRHS(), inputFieldVariables);
		}
		else if (command instanceof VarDeclCommand) {
			ZDeclList decllist = ((VarDeclCommand)command).getZDeclList();
			boolean aux = variableIsInsideZDeclList (var, decllist, inputFieldVariables);
			boolean action = variableIsInsideAction (var, ((VarDeclCommand)command).getCircusAction(), process, calls, inputFieldVariables, spec);
			return aux || action;
		}
		else if (command instanceof IfGuardedCommand) {
			CircusActionList actionlist = ((IfGuardedCommand)command).getGuardedActionList();
			int size = actionlist.size();
			boolean aux = false;
			for (int i = 0; i < size; i++) {
				GuardedAction ga = (GuardedAction) actionlist.get(i);
				aux = aux || variableIsInsideAction (var, ga, process, calls, inputFieldVariables, spec);
			}
			return aux;
		}
		else {
			ExceptionUtil.throwException ("ScopeUtil.variableIsInsideCommand was not implemented yet for this command...");
			return false;
		}
	}
	private static boolean variableIsInsideZSchText (String var, ZSchText schtext, Vector <String> inputFieldVariables) {
		ZDeclList decllist = schtext.getZDeclList();
		Pred pred = schtext.getPred();
		boolean isondecllist = variableIsInsideZDeclList (var, decllist, inputFieldVariables);
		boolean isonpred = variableIsInsidePred (var, pred, inputFieldVariables);
		return isondecllist || isonpred;
	}
	private static boolean variableIsInsideAxPara (String var, AxPara para, Vector <String> inputFieldVariables) {
		ZSchText schtext = ((AxPara)para).getZSchText();
		ZNameList namelist = ((AxPara)para).getZNameList();
		boolean isonschtext = variableIsInsideZSchText (var, schtext, inputFieldVariables);
		boolean isonnamelist = variableIsInsideZNameList (var, namelist);
		return isonschtext || isonnamelist;
	}
	public static boolean variableIsInsideProcess (String var, CircusProcess process, Spec spec) {
		if (process instanceof ParamProcess) {
			boolean isondecllist = variableIsInsideZDeclList (var, ((ParamProcess)process).getZDeclList(), new Vector <String> ());
			boolean isonotherprocess = variableIsInsideProcess (var, ((ParamProcess)process).getCircusProcess(), spec);
			return isondecllist || isonotherprocess;
		}
		else if (process instanceof BasicProcess) {
			ZParaList paralist = ((BasicProcess)process).getZParaList();
			int size = paralist.size();
			boolean aux = false;
			for (int i = 0; i < size; i++) {
				Para para = paralist.get(i);
				if (para instanceof AxPara) {
					aux = aux || variableIsInsideAxPara (var, (AxPara)para, new Vector <String> ());
				}
				else if (para instanceof ActionPara) {
					aux = aux || variableIsInsideAction (var, ((ActionPara)para).getCircusAction(), (BasicProcess)process, spec);
				}
			}
			return aux;
		}
		else if (process instanceof Process2) {
			return
					variableIsInsideProcess (var, ((Process2)process).getLeftProcess (), spec)
					|| variableIsInsideProcess (var, ((Process2)process).getRightProcess (), spec);

		}
		else if (process instanceof Process1) {
			return variableIsInsideProcess (var, ((Process1)process).getCircusProcess (), spec);
		}
		else {
			ExceptionUtil.throwException ("ScopeUtil.variableIsInsideProcess: this process was not implemented yet on this method");
			return false;
		}
	}
}