package de.dhbwstuttgart.typeinference.unify.model;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map.Entry;
import java.util.Set;
import java.util.function.Function;

/**
 * A set of substitutions (s -> t) that is an applicable function to types and pairs.
 * @author Florian Steurer
 */
public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<PlaceholderType, UnifyType>> {
	
	/**
	 * The set of substitutions that unify a type-term
	 */
	private HashMap<PlaceholderType, UnifyType> substitutions = new HashMap<>();

	/**
	 * Creates a new instance with a single substitution (source -> target).
	 * @param The type that is replaced
	 * @param The type that replaces
	 */
	public Unifier(PlaceholderType source, UnifyType target) {
		substitutions.put(source, target);
	}
	
	/**
	 * Identity function as an "unifier".
	 */
	protected Unifier() {

	}
	
	/**
	 * Creates an unifier that is the identity function (thus has no substitutions).
	 */
	public static Unifier identity() {
		return new Unifier();
	}
	
	/**
	 * Adds a substitution to the unifier from (source -> target)
	 * @param The type that is replaced
	 * @param The type that replaces
	 */
	public void add(PlaceholderType source, UnifyType target) {
		Unifier tempU = new Unifier(source, target);
		// Every new substitution must be applied to previously added substitutions
		// otherwise the unifier needs to be applied multiple times to unify two terms
		for(PlaceholderType pt : substitutions.keySet())
			substitutions.put(pt, substitutions.get(pt).apply(tempU));
		substitutions.put(source, target);
	}

	@Override
	public UnifyType apply(UnifyType t) {
		return t.apply(this);
	}
	
	/**
	 * Applies the unifier to the two terms of the pair.
	 * @return A new pair where the left and right-hand side are applied
	 */
	public UnifyPair apply(UnifyPair p) {
		UnifyType newLhs = this.apply(p.getLhsType());
		UnifyType newRhs = this.apply(p.getRhsType());
		return new UnifyPair(newLhs, newRhs, p.getPairOp());
	}
	
	/**
	 * Applies the unifier to the two terms of the pair.
	 * works only for single subsitution
	 * @return A new pair where the left and right-hand side are applied
	 */
	public UnifyPair apply(UnifyPair thisAsPair, UnifyPair p) {
		UnifyType newLhs = this.apply(p.getLhsType());
		UnifyType newRhs = this.apply(p.getRhsType());
		//Varianceweitergabe wird nicht benoetigt.
		//PlaceholderType lhsph = (PlaceholderType)thisAsPair.getLhsType();
		//if (lhsph.getVariance() != 0) {
		//	if (p.getLhsType().equals(lhsph)) {
		//		if (p.getRhsType() instanceof PlaceholderType) {
		//			((PlaceholderType)p.getRhsType()).setVariance(lhsph.getVariance());
		//		}
		//	}
		//	if (p.getRhsType().equals(lhsph)) {
		//		if (p.getLhsType() instanceof PlaceholderType) {
		//			((PlaceholderType)p.getLhsType()).setVariance(lhsph.getVariance());
		//		}
		//	}
		//}
		if (!(p.getLhsType().equals(newLhs)) || !(p.getRhsType().equals(newRhs))) {//Die Anwendung von this hat was veraendert PL 2018-04-01
			Set<UnifyPair> suniUnifyPair = new HashSet<>();
			suniUnifyPair.addAll(thisAsPair.getAllSubstitutions());
			suniUnifyPair.add(thisAsPair);
			if (p.getLhsType() instanceof PlaceholderType //&& newLhs instanceof PlaceholderType entfernt PL 2018-04-13
					&& p.getPairOp() == PairOperator.EQUALSDOT) {
				suniUnifyPair.add(p); //p koennte auch subsitution sein
			}
			return new UnifyPair(newLhs, newRhs, p.getPairOp(), suniUnifyPair, p);
		}
		return new UnifyPair(newLhs, newRhs, p.getPairOp(), p.getSubstitution(), p.getBasePair(), p.getfBounded());
	}
	
	/**
	 * Applies the unifier to the left terms of the pair.
	 * @return A new pair where the left and right-hand side are applied
	 */
	public UnifyPair applyleft(UnifyPair p) {
		return new UnifyPair(this.apply(p.getLhsType()), p.getRhsType(), p.getPairOp());
	}
	
	/**
	 * True if the typevariable t will be substituted if the unifier is applied.
	 * false otherwise.
	 */
	public boolean hasSubstitute(PlaceholderType t) {
		return substitutions.containsKey(t);
	}
	
	/**
	 * Returns the type that will replace the typevariable t if the unifier is applied.
	 */
	public UnifyType getSubstitute(PlaceholderType t) {
		return substitutions.get(t);
	}

	/**
	 * The number of substitutions in the unifier. If zero, this is the identity function.
	 */
	public int size() {
		return substitutions.size();
	}
	
	/**
	 * Garantuees that if there is a substitutions (a -> b) in this unifier,
	 * a is not an element of the targetParams. Substitutions that do not
	 * satisfy this condition, are swapped.
	 */
	public void swapPlaceholderSubstitutions(Iterable<UnifyType> targetParams) {
		for(UnifyType tph : targetParams) {
			if(!(tph instanceof PlaceholderType))
				continue;
			// Swap a substitutions (a -> b) if a is an element of the target params.
			if(substitutions.containsKey(tph)) {		
				if((substitutions.get(tph) instanceof PlaceholderType)) {
					PlaceholderType newLhs = (PlaceholderType) substitutions.get(tph);
					substitutions.remove(tph);
					substitutions.put(newLhs, tph);
				}
			}
		}
	}
	
	public void swapPlaceholderSubstitutionsReverse(Iterable<UnifyType> sourceParams) {
		for(UnifyType tph : sourceParams) {
			if(!(tph instanceof PlaceholderType))
				continue;
			if(substitutions.containsValue(tph)) {
				UnifyType key = substitutions.values().stream().filter(x -> x.equals(tph)).findAny().get();
				if(key instanceof PlaceholderType) {
					PlaceholderType newLhs = (PlaceholderType) tph;
					substitutions.remove(key);
					substitutions.put(newLhs, key);
				}
			}
		}
	}

	@Override
	public String toString() {
		String result = "{ ";
		for(Entry<PlaceholderType, UnifyType> entry : substitutions.entrySet())
			result += "(" + entry.getKey() + " -> " + entry.getValue() + "), ";
		if(!substitutions.isEmpty())
			result = result.substring(0, result.length()-2);
		result += " }";
		return result;
	}

	@Override
	public Iterator<Entry<PlaceholderType, UnifyType>> iterator() {
		return substitutions.entrySet().iterator();
	}
}

