package models.algebra;

import generators.JavaImplementationVisitor;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.List;
import java.util.Map.Entry;

public class Term extends Expression {
	protected Symbol symbol = null;
	protected List<Expression> children = new ArrayList<>();
	protected Type type = null;
	
	public Term(Symbol symbol) {
		super();
		this.symbol = symbol;
	}
	
	public Term(Symbol symbol, List<Expression> children) {
		super();
		this.symbol = symbol;
		this.children = children;
	}
	
	public Term(Symbol symbol, Expression[] children) {
		super();
		this.symbol = symbol;
		this.children = new ArrayList<>(Arrays.asList(children));
	}
	
	public Symbol getSymbol() {
		return symbol;
	}
	
	public int getArity() {
		return symbol.getArity();
	}
	
	public void setType(Type type) {
		this.type = type;
	}
	
	public Type getType() {
		if (type == null) {
			if (symbol.getSignature() == null) return null;
			return symbol.getSignature()[0];
		}
		return type;
	}
	
	public boolean addChild(Expression child) {
		if (getArity() != -1 && children.size() >= getArity()) return false;
		children.add(child);
		return true;
	}
	
	public boolean setChild(int n, Expression child) {
		if (getArity() != -1 && n >= getArity()) return false;
		children.set(n, child);
		return true;
	}
	
	public void addChild(Expression child, boolean bForced) {
		if (!bForced && getArity() != -1 && children.size() >= getArity()) return;
		children.add(child);
	}
	
	public void addChild(int n, Expression child, boolean bForced) {
		if (!bForced && getArity() != -1 && children.size() >= getArity()) return;
		children.add(n, child);
	}
	
	public Expression getChild(int n) {
		return children.get(n);
	}
	
	public List<Expression> getChildren() {
		return children;
	}
	
	public <T extends Expression> HashMap<Position, T> getSubTerms(Class<T> clazz) {
		HashMap<Position, T> subTerms = new HashMap<>();
		Class thisClass = this.getClass();
		while (thisClass != null) {
			if (clazz == thisClass) {
				subTerms.put(new Position(), (T) this);
				break;
			}
			thisClass = thisClass.getSuperclass();
		}
		for (int i = 0; i < children.size(); i++) {
			if (children.get(i) != null) {
				HashMap<Position, T> terms = children.get(i).getSubTerms(clazz);
				for (Entry<Position, T> term : terms.entrySet()) {
					Position pos = term.getKey();
					pos.addHeadOrder(i);
					subTerms.put(pos, term.getValue());
				}
			}
		}
		return subTerms;
	}
	
	public Expression getSubTerm(Position pos) {
		if (pos.isEmpty()) return this;
		pos = (Position) pos.clone();
		int i = pos.removeHeadOrder();
		if (i >= children.size()) return null;
		if (children.get(i) == null) return null;
		return children.get(i).getSubTerm(pos);
	}
	
	public Term substitute(Variable variable, Expression value) {
		Term newTerm = (Term) this.clone();
		HashMap<Position, Variable> variables = getVariables();
		for (Entry<Position, Variable> varEnt : variables.entrySet()) {
			if (varEnt.getValue().equals(variable)) {
				newTerm.replaceSubTerm(varEnt.getKey(), value);
			}
		}
		return newTerm;
	}
	
	public void replaceSubTerm(Position pos, Expression newSubTerm) {
		if (pos.isEmpty()) return;
		pos = (Position) pos.clone();
		int i = pos.removeHeadOrder();
		if (pos.isEmpty()) {
			children.set(i, newSubTerm);
		} else {
			if (!(children.get(i) instanceof Term)) return;
			((Term) children.get(i)).replaceSubTerm(pos, newSubTerm);
		}
	}
	
	@Override
	public Expression unify(Expression another) {
		if (another instanceof Variable) return (Expression) this.clone();
		if (this instanceof Constant) return (Expression) this.clone();
		if (another instanceof Constant) return (Expression) another.clone();
		if (another instanceof Term) {
			Term anotherTerm = (Term) another;
			if (!symbol.equals(anotherTerm.symbol)) return null;
			if (children.size() != anotherTerm.children.size()) return null;
			Term unifiedTerm = new Term(symbol);
			for (int i = 0; i < children.size(); i++) {
				if (children.get(i) != null) {
					unifiedTerm.addChild(children.get(i).unify(anotherTerm.children.get(i)));
				} else {
					unifiedTerm.addChild(anotherTerm.children.get(i));
				}
			}
			return unifiedTerm;
		} else {
			return null;
		}
	}
	
	public Expression reduce() {
		if (symbol.isLambda()) {
			// Lambda beta-reduction
			LambdaAbstraction newSymbol = ((LambdaAbstraction) symbol);
			Term newTerm = newSymbol.getTerm();
			List<Variable> newVariables = newSymbol.getVariables();
			List<Expression> newChildren = children;
			while (newVariables.size() > 0 && newChildren.size() > 0) {
				newTerm = newTerm.substitute(newVariables.get(0), newChildren.get(0));
				newVariables = newVariables.subList(1, newVariables.size());
				newChildren = newChildren.subList(1, newChildren.size());
				newSymbol = new LambdaAbstraction(newVariables, newTerm);
			}
			if (newSymbol.arity == 0 && newChildren.size() == 0) {
				return newTerm;
			} else {
				return new Term(newSymbol, newChildren);
			}
		} else if (symbol.isCalculatable()) {
			List<Expression> newChildren = new ArrayList<>();
			for (Expression child : children) {
				if (child instanceof Term) {
					child = ((Term) child).reduce();
				}
				newChildren.add(child);
			}
			Expression newTerm = symbol.calculate(newChildren);
			if (newTerm == null) return this;
			return newTerm;
		} else {
			// Calculate inverse map
			List<Expression> newChildren = new ArrayList<>();
			boolean bReduced = false;
			for (Expression child : children) {
				if (child instanceof Term && !(child instanceof Constant)) {
					Expression newChild = ((Term) (child)).reduce();
					if (newChild != child) {
						bReduced = true;
						child = newChild;
					}
				}
				newChildren.add(child);
			}
			if (symbol.arity == 1 && newChildren.size() == 1) {
				Expression child = newChildren.get(0);
				if (child instanceof Term && !(child instanceof Constant)) {
					Symbol childSymbol = ((Term) child).getSymbol();
					if (childSymbol.getInverses() != null) {
						for (int i = 0; i < childSymbol.getInverses().length; i++) {
							if (symbol.equals(childSymbol.getInverses()[i])) {
								return ((Term) child).getChild(i);
							}
						}
					}
				}
			}
			if (!bReduced) return this;
			Term newTerm = (Term) this.clone();
			newTerm.children = newChildren;
			return newTerm;
		}
	}
	
	@Override
	public Expression getInverseMap(Expression outputValue, Position targetPos) {
		if (targetPos.isEmpty()) return outputValue;
		targetPos = (Position) targetPos.clone();
		int i = targetPos.removeHeadOrder();
		Symbol[] inverseSymbols = symbol.getInverses();
		if (inverseSymbols == null || i >= inverseSymbols.length || inverseSymbols[i] == null) return null;
		Term inverseMap = new Term(inverseSymbols[i]);
		inverseMap.addChild(outputValue);
		for (int n = 0; n < inverseSymbols[i].getArity(); n++) {
			if (n != i) {
				inverseMap.addChild(children.get(n));
			}
		}
		return children.get(i).getInverseMap(inverseMap, targetPos);
	}
	
	@Override
	public boolean contains(Expression exp) {
		if (equals(exp)) return true;
		for (Expression e : children) {
			if (e.contains(exp)) return true;
		}
		return false;
	}
	
	@Override
	public boolean equals(Object another) {
		if (!(another instanceof Term)) return false;
		if (this == another) return true;
		Term anotherTerm = (Term) another;
		if (!symbol.equals(anotherTerm.symbol)) return false;
		if (children.size() != anotherTerm.children.size()) return false;
		if (type != anotherTerm.type) return false;
		for (int i = 0; i < children.size(); i++) {
			Expression e = children.get(i);
			Expression e2 = anotherTerm.children.get(i);
			if (!e.equals(e2)) return false;
		}
		return true;
	}
	
	@Override
	public int hashCode() {
		return symbol.hashCode();
	}
	
	
	@Override
	public Object clone() {
		Term newTerm = new Term(symbol);
		for (Expression e : children) {
			if (e != null) {
				newTerm.addChild((Expression) e.clone());
			} else {
				newTerm.addChild(null);
			}
		}
		newTerm.type = type;
		return newTerm;
	}
	
	public String toString() {
		if (getArity() == 2 && symbol.isInfix()) {
			return "(" + children.get(0) + symbol.toString() + children.get(1) + ")";
		}
		if ((getArity() >= 1 || getArity() == -1) && symbol.isMethod()) {
			String exp = children.get(0).toString() + "." + symbol.toString() + "(";
			String delimiter = "";
			for (int i = 1; i < children.size(); i++) {
				Expression e = children.get(i);
				exp += (delimiter + e.toString());
				delimiter = ",";
			}
			return exp + ")";
		} else {
			String exp = symbol.toString() + "(";
			String delimiter = "";
			for (Expression e : children) {
				if (e != null) {
					exp += (delimiter + e.toString());
				} else {
					exp += (delimiter + "null");
				}
				delimiter = ",";
			}
			return exp + ")";
		}
	}
	
	public String toImplementation(String[] sideEffects) {
		return accept(new JavaImplementationVisitor(), sideEffects).toString();
	}
	
	@Override
	public code.ast.Expression accept(IExpressionVisitor visitor, String[] sideEffects) {
		return visitor.visit(this, sideEffects);
	}
}