package models.dataConstraintModel;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Map.Entry;
import java.util.Set;

import models.algebra.Constant;
import models.algebra.Expression;
import models.algebra.InvalidMessage;
import models.algebra.Position;
import models.algebra.Term;
import models.algebra.ValueUndefined;
import models.algebra.Variable;
import models.dataFlowModel.ResolvingMultipleDefinitionIsFutureWork;

public class StateTransition {
	private Expression curStateExpression = null;
	private Expression nextStateExpression = null;
	private Expression messageExpression = null;
	
	public Expression getCurStateExpression() {
		return curStateExpression;
	}
	
	public void setCurStateExpression(Expression curStateExpression) {
		this.curStateExpression = curStateExpression;
	}
	
	public Expression getNextStateExpression() {
		return nextStateExpression;
	}
	
	public void setNextStateExpression(Expression nextStateExpression) {
		this.nextStateExpression = nextStateExpression;
	}

	public Expression getMessageExpression() {
		return messageExpression;
	}

	public void setMessageExpression(Expression messageExpression) {
		this.messageExpression = messageExpression;
	}
	
	public boolean isRightUnary() {
		for (Variable var: curStateExpression.getVariables().values()) {
			if (nextStateExpression.contains(var)) return false;
		}
		return true;
	}
	
	public boolean isRightPartial() {
		for (Variable var: curStateExpression.getVariables().values()) {
			if (messageExpression.contains(var)) return true;
		}
		if (isRightUnary()) return false;
		for (Variable var: messageExpression.getVariables().values()) {
			if (nextStateExpression.contains(var)) return true;
		}
		return false;
	}

	public Expression deriveMessageConstraintFor(Expression curStateValue, Expression nextStateValue, Set<Position> substitutedPositions) throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork {
		HashMap<Variable, ArrayList<Expression>> bindings = new HashMap<>();
		
		Expression curStateTerm = getCurStateExpression();
		HashMap<Position, Variable> curStateVars = curStateTerm.getVariables();		
		for (Entry<Position, Variable> curStateVarEnt: curStateVars.entrySet()) {
			Variable var = curStateVarEnt.getValue();
			Position varPos = curStateVarEnt.getKey();
			Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos);
			if (valueCalc != null) {
				if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) {
					valueCalc = ((Term) valueCalc).reduce();
				}
				ArrayList<Expression> values = bindings.get(var);
				if (values == null) {
					values = new ArrayList<Expression>();
					bindings.put(var, values);
				}
				values.add(valueCalc);
			}
		}
		
		Expression nextStateTerm = (Expression) getNextStateExpression().clone();
		for (Variable var: bindings.keySet()) {
			HashMap<Position, Variable> vars2 = nextStateTerm.getVariables();
			for (Variable var2: vars2.values()) {
				if (var.equals(var2) && bindings.get(var).size() == 1) {
					if (nextStateTerm instanceof Term) {
						nextStateTerm = ((Term) nextStateTerm).substitute(var, bindings.get(var).get(0));
					} else if (nextStateTerm instanceof Variable && nextStateTerm.equals(var)) {
						nextStateTerm = bindings.get(var).get(0);
					}
				}
			}
		}
		
		HashMap<Position, Variable> nextStateVars = nextStateTerm.getVariables();
		for (Entry<Position, Variable> nextStateVarEnt: nextStateVars.entrySet()) {
			Variable var = nextStateVarEnt.getValue();
			Position varPos = nextStateVarEnt.getKey();
			Expression valueCalc = nextStateTerm.getInverseMap(nextStateValue, varPos);
			if (valueCalc != null) {
				if (valueCalc instanceof Term) {
					valueCalc = ((Term) valueCalc).reduce();
				}
				ArrayList<Expression> values = bindings.get(var);
				if (values == null) {
					values = new ArrayList<Expression>();
					bindings.put(var, values);
				}
				values.add(valueCalc);
			}
		}
		
		Expression messageTerm = getMessageExpression();
		return substituteValues(messageTerm, bindings, substitutedPositions);
	}

	public Expression deriveMessageConstraintFor(Expression curStateValue, Set<Position> substitutedPositions) throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork {
		HashMap<Variable, ArrayList<Expression>> bindings = new HashMap<>();
		
		Expression curStateTerm = getCurStateExpression();
		HashMap<Position, Variable> curStateVars = curStateTerm.getVariables();		
		for (Entry<Position, Variable> curStateVarEnt: curStateVars.entrySet()) {
			Variable var = curStateVarEnt.getValue();
			Position varPos = curStateVarEnt.getKey();
			Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos);
			if (valueCalc != null) {
				if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) {
					valueCalc = ((Term) valueCalc).reduce();
				}
				ArrayList<Expression> values = bindings.get(var);
				if (values == null) {
					values = new ArrayList<Expression>();
					bindings.put(var, values);
				}
				values.add(valueCalc);
			}
		}
		
		Expression messageTerm = getMessageExpression();
		return substituteValues(messageTerm, bindings, substitutedPositions);
	}

	private Expression substituteValues(Expression messageTerm, HashMap<Variable, ArrayList<Expression>> bindings, Set<Position> substitutedPositions)
			throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork {
		if (!(messageTerm instanceof Term) && !(messageTerm instanceof Variable)) throw new InvalidMessage();
		HashMap<Position, Variable> messageVars = messageTerm.getVariables();
		for (Entry<Position, Variable> varEnt: messageVars.entrySet()) {
			Variable var = varEnt.getValue();
			if (bindings.get(var) != null) {
				if (bindings.get(var).size() > 1) throw new ResolvingMultipleDefinitionIsFutureWork();
				if (messageTerm instanceof Term) {
					substitutedPositions.add(varEnt.getKey());
					messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next());
				} else if (messageTerm instanceof Variable) {
					if (messageTerm.equals(var)) {
						substitutedPositions.add(new Position());
						return bindings.get(var).iterator().next();
					}
				}
			}
		}
		return messageTerm;
	}

	public Expression deriveNextStateExpressionFor(Expression curStateValue, Term concreteMessage) 
			throws ResolvingMultipleDefinitionIsFutureWork, ValueUndefined {
		HashMap<Variable, Expression> bindings = new HashMap<>();

		Expression curStateTerm = getCurStateExpression();
		HashMap<Position, Variable> curStateVars = curStateTerm.getVariables();
		for (Entry<Position, Variable> curStateVarEnt: curStateVars.entrySet()) {
			Variable var = curStateVarEnt.getValue();
			Position varPos = curStateVarEnt.getKey();
			Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos);
			if (valueCalc != null) {
				if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) {
					valueCalc = ((Term) valueCalc).reduce();
				}
				if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork();
				bindings.put(var, valueCalc);
			}
		}
		
		Expression messageTerm = getMessageExpression();
		HashMap<Position, Variable> messageVars = messageTerm.getVariables();
		if (concreteMessage != null) {
			for (Entry<Position, Variable> messageVarEnt: messageVars.entrySet()) {
				Variable var = messageVarEnt.getValue();
				Position varPos = messageVarEnt.getKey();
				Expression valueCalc = concreteMessage.getSubTerm(varPos);
				if (valueCalc != null) {
					if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork();
					bindings.put(var, valueCalc);
				}
			}
		}
		
		Expression nextStateTerm = getNextStateExpression();
		if (nextStateTerm instanceof Variable) {
			nextStateTerm = bindings.get((Variable) nextStateTerm);
			if (nextStateTerm == null) throw new ValueUndefined();
		} else {
			for (Variable var: bindings.keySet()) {
				nextStateTerm = ((Term) nextStateTerm).substitute(var, bindings.get(var));
			}
		}
		if (nextStateTerm instanceof Term && !(nextStateTerm instanceof Constant)) {
			nextStateTerm = ((Term) nextStateTerm).reduce();
		}
		return nextStateTerm;
	}
}