package de.dhbwstuttgart.typeinference.unify;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;
import java.util.Stack;
import java.util.function.Function;
import java.util.stream.Collectors;

import de.dhbwstuttgart.exceptions.DebugException;
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
import de.dhbwstuttgart.typeinference.unify.model.WildcardType;
import de.dhbwstuttgart.typeinference.unify.distributeVariance;

import java.io.FileWriter;
import java.io.IOException;
import java.io.Writer;

/**
 * Implementation of the type inference rules.
 * @author Florian Steurer
 *
 */
public class RuleSet implements IRuleSet{
	
	Writer logFile;
	
	public RuleSet() {
		super();
	}
	
	RuleSet(Writer logFile) {
		this.logFile = logFile;
	}
	
	@Override
	public Optional<UnifyPair> reduceUp(UnifyPair pair) {
		// Check if reduce up is applicable 
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType rhsType = pair.getRhsType();
		if(!(rhsType instanceof SuperType))
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType))
			return Optional.empty();
		
		// Rule is applicable, unpack the SuperType 
		return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> reduceLow(UnifyPair pair) {
		// Check if rule is applicable
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		if(!(lhsType instanceof ExtendsType))
			return Optional.empty();
		
		UnifyType rhsType = pair.getRhsType();
		if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType))
			return Optional.empty();

		// Rule is applicable, unpack the ExtendsType
		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> reduceUpLow(UnifyPair pair) {
		// Check if rule is applicable
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		if(!(lhsType instanceof ExtendsType))
			return Optional.empty();
		
		UnifyType rhsType = pair.getRhsType();
		if(!(rhsType instanceof SuperType))
			return Optional.empty();
		
		// Rule is applicable, unpack both sides
		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();

		UnifyType x = pair.getLhsType();
		UnifyType sTypeX;
		
		if(x instanceof ReferenceType)
			sTypeX = x;
		else if(x instanceof ExtendsType)
			sTypeX = ((ExtendsType) x).getExtendedType();
		else 
			return Optional.empty();

		UnifyType extY = pair.getRhsType();

		if(!(extY instanceof ExtendsType))
			return Optional.empty();

		if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size())
			return Optional.empty();
		
		UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
		
		if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
			return Optional.empty();
		
		if(x instanceof ExtendsType)
			xFromFc = new ExtendsType(xFromFc);
		
		UnifyType extYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
		
		if(extYFromFc == null || extYFromFc.getTypeParams() != xFromFc.getTypeParams())
			return Optional.empty();

		TypeParams extYParams = extY.getTypeParams();
		TypeParams xParams = x.getTypeParams();
		
		int[] pi = pi(xParams, extYParams);
		
		if(pi.length == 0)
			return Optional.empty();
		
		Set<UnifyPair> result = new HashSet<>();
		
		for(int rhsIdx = 0; rhsIdx < extYParams.size(); rhsIdx++)
			result.add(new UnifyPair(xParams.get(pi[rhsIdx]), extYParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
		
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType x = pair.getLhsType();
		UnifyType sTypeX;
		
		if(x instanceof ReferenceType)
			sTypeX = x;
		else if(x instanceof SuperType)
			sTypeX = ((SuperType) x).getSuperedType();
		else
			return Optional.empty();
		
		UnifyType supY = pair.getRhsType();
		
		if(!(supY instanceof SuperType))
			return Optional.empty();

		if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size())
			return Optional.empty();
		
		UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
		
		if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
			return Optional.empty();
		
		if(x instanceof SuperType)
			xFromFc = new SuperType(xFromFc);
		
		UnifyType supYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
		
		if(supYFromFc == null || supYFromFc.getTypeParams() != xFromFc.getTypeParams())
			return Optional.empty();
		
		TypeParams supYParams = supY.getTypeParams();
		TypeParams xParams = x.getTypeParams();
		Set<UnifyPair> result = new HashSet<>();
		
		int[] pi = pi(xParams, supYParams);
		
		if(pi.length == 0)
			return Optional.empty();
		
		for(int rhsIdx = 0; rhsIdx < supYParams.size(); rhsIdx++)
			result.add(new UnifyPair(supYParams.get(rhsIdx), xParams.get(pi[rhsIdx]), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
		
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> reduceEq(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		if(lhsType instanceof PlaceholderType || lhsType.getTypeParams().empty())
			return Optional.empty();
		
		UnifyType rhsType = pair.getRhsType();
		
		if(!rhsType.getName().equals(lhsType.getName()))
			return Optional.empty();
		
		if(rhsType instanceof PlaceholderType || lhsType instanceof PlaceholderType || rhsType.getTypeParams().empty())
			return Optional.empty();
		
		if(rhsType.getTypeParams().size() != lhsType.getTypeParams().size())
			return Optional.empty();
		
		// Keine Permutation wie im Paper nötig
		Set<UnifyPair> result = new HashSet<>();
		TypeParams lhsTypeParams = lhsType.getTypeParams();
		TypeParams rhsTypeParams = rhsType.getTypeParams();
		
		for(int i = 0; i < lhsTypeParams.size(); i++)
			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> reduce1(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType c = pair.getLhsType();
		if(!(c instanceof ReferenceType))
			return Optional.empty();
		
		UnifyType d = pair.getRhsType();
		if(!(d instanceof ReferenceType))
			return Optional.empty();
		
		ReferenceType lhsSType = (ReferenceType) c;
		ReferenceType rhsSType = (ReferenceType) d;
		
		//try {
		//	logFile.write("PAIR Rules: " + pair + "\n");
		//	logFile.flush();
		//}
		//catch (IOException e) { }
		
		if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size())
			return Optional.empty();
		
		UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null);
		//2018-02-23: liefert Vector<Vector<Integer>>: Das kann nicht sein.
		
		//NOCHMAL UEBERPRUEFEN
		//PL 18-02-09 Eingfuegt Anfang
		//C und D koennen auch gleich sein.
		if (c.getName().equals(d.getName())) {
			Set<UnifyPair> result = new HashSet<>();
			TypeParams rhsTypeParams = d.getTypeParams();
			TypeParams lhsTypeParams = c.getTypeParams();
			for(int rhsIdx = 0; rhsIdx < c.getTypeParams().size(); rhsIdx++)
				result.add(new UnifyPair(lhsTypeParams.get(rhsIdx), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
		
			return Optional.of(result);
		}
		//PL 18-02-09 Eingfuegt ENDE
		
		//try {
		//	logFile.write("cFromFc: " + cFromFc);
		//	logFile.flush();
		//}
		//catch (IOException e) { }
		
		if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders())
			return Optional.empty();
		
		UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null);
		
		//try {
		//	logFile.write("cFromFc: " + cFromFc);
		//	logFile.flush();
		//}
		//catch (IOException e) { }
		
		if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size())
			return Optional.empty();
		//System.out.println("cFromFc: " + cFromFc);
		//System.out.println("dFromFc: " + dFromFc);
		int[] pi = pi(cFromFc.getTypeParams(), dFromFc.getTypeParams());
		
		if(pi.length == 0)
			return Optional.empty();
		
		TypeParams rhsTypeParams = d.getTypeParams();
		TypeParams lhsTypeParams = c.getTypeParams();
		Set<UnifyPair> result = new HashSet<>();
		
		for(int rhsIdx = 0; rhsIdx < rhsTypeParams.size(); rhsIdx++)
			result.add(new UnifyPair(lhsTypeParams.get(pi[rhsIdx]), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
		
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> reduce2(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.EQUALSDOT)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		ReferenceType lhsSType;
		UnifyType rhsType = pair.getRhsType();
		ReferenceType rhsSType;
		
		if ((lhsType instanceof ReferenceType) && (rhsType instanceof ReferenceType)) {
			lhsSType = (ReferenceType) lhsType;
			rhsSType = (ReferenceType) rhsType;
		}
		else if (((lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType)) 
				|| ((lhsType instanceof SuperType) && (rhsType instanceof SuperType))) {
			UnifyType lhsSTypeRaw = ((WildcardType) lhsType).getWildcardedType();
			UnifyType rhsSTypeRaw = ((WildcardType) rhsType).getWildcardedType();
			if ((lhsSTypeRaw instanceof ReferenceType) && (rhsSTypeRaw instanceof ReferenceType)) {
				lhsSType = (ReferenceType) lhsSTypeRaw;
				rhsSType = (ReferenceType) rhsSTypeRaw;
			}
			else
				return Optional.empty();
		}
		else
			return Optional.empty();
		
		if(lhsSType.getTypeParams().empty())
			return Optional.empty();

		/* PL 2018-01-22 in obere Teil integriert
		UnifyType rhsType = pair.getRhsType();
		ReferenceType rhsSType;
		
		if(rhsType instanceof ReferenceType)
			rhsSType = (ReferenceType) rhsType;
		else if(rhsType instanceof WildcardType)  {
			UnifyType rhsSTypeRaw = ((WildcardType) rhsType).getWildcardedType();
			if(rhsSTypeRaw instanceof ReferenceType)
				rhsSType = (ReferenceType) rhsSTypeRaw;
			else
				return Optional.empty();
		}
		else
			return Optional.empty();
		*/
		
		if(!rhsSType.getName().equals(lhsSType.getName()))
			return Optional.empty();
		
		if(!(lhsSType.getTypeParams().size()==rhsSType.getTypeParams().size()))throw new DebugException("Fehler in Unifizierung"+ " " + lhsSType.toString() + " " + rhsSType.toString());
		//if(rhsSType.getTypeParams().size() != lhsSType.getTypeParams().size())
		//	return Optional.empty();
		
		Set<UnifyPair> result = new HashSet<>();
		
		TypeParams rhsTypeParams = rhsSType.getTypeParams();
		TypeParams lhsTypeParams = lhsSType.getTypeParams();
		for(int i = 0; i < rhsTypeParams.size(); i++)
			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		
		return Optional.of(result);
	}

	@Override
	public boolean erase1(UnifyPair pair, IFiniteClosure fc) {
		if((pair.getPairOp() != PairOperator.SMALLERDOT) && (pair.getPairOp() != PairOperator.SMALLERNEQDOT))
			return false;
		
		if (pair.getPairOp() == PairOperator.SMALLERNEQDOT) {
			UnifyType lhs = pair.getLhsType();
			UnifyType rhs = pair.getRhsType();
			if (lhs instanceof WildcardType) {
				lhs = ((WildcardType)lhs).getWildcardedType();
			}
			if (rhs instanceof WildcardType) {
				rhs = ((WildcardType)rhs).getWildcardedType();
			}
		
			if	(lhs.equals(rhs)){
				return false;
			}
		}
		
		UnifyType lhsType = pair.getLhsType();
		if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType))
			return false;
		
		UnifyType rhsType = pair.getRhsType();
		if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType))
			return false;
		
		return fc.greater(lhsType, new HashSet<>()).contains(rhsType);
	}

	@Override
	public boolean erase2(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return false;
		
		UnifyType lhsType = pair.getLhsType();		
		UnifyType rhsType = pair.getRhsType();
		
		return fc.grArg(lhsType, new HashSet<>()).contains(rhsType);
	}

	@Override
	public boolean erase3(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.EQUALSDOT)
			return false;
		
		return pair.getLhsType().equals(pair.getRhsType());
	}

	@Override
	public Optional<UnifyPair> swap(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.EQUALSDOT)
			return Optional.empty();
		
		if(pair.getLhsType() instanceof PlaceholderType)
			return Optional.empty();
		
		if(!(pair.getRhsType() instanceof PlaceholderType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(pair.getRhsType(), pair.getLhsType(), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> adapt(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType typeD = pair.getLhsType();
		if(!(typeD instanceof ReferenceType))
			return Optional.empty();
		
		UnifyType typeDs = pair.getRhsType();
		if(!(typeDs instanceof ReferenceType))
			return Optional.empty();
		
		/*if(typeD.getTypeParams().size() == 0 || typeDs.getTypeParams().size() == 0)
			return Optional.empty();*/
		
		if(typeD.getName().equals(typeDs.getName()))
			return Optional.empty();
		

		Optional<UnifyType> opt = fc.getLeftHandedType(typeD.getName());
		if(!opt.isPresent())
			return Optional.empty();
		
		// The generic Version of Type D (D<a1, a2, a3, ... >)
		UnifyType typeDgen = opt.get();
	
		// Actually greater+ because the types are ensured to have different names
		Set<UnifyType> greater = fc.getAncestors(typeDgen);
		opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();

		if(!opt.isPresent())
			return Optional.empty();
		
		UnifyType newLhs = opt.get();
		
		TypeParams typeDParams = typeD.getTypeParams();
		TypeParams typeDgenParams = typeDgen.getTypeParams();
		
		//System.out.println("Pair: " +pair);
		//System.out.println("typeD: " +typeD);
		//System.out.println("typeDParams: " +typeDParams);
		//System.out.println("typeDgen: " +typeD);
		//System.out.println("typeDgenParams: " +typeDgenParams);
		Unifier unif = Unifier.identity();
		for(int i = 0; i < typeDParams.size(); i++) { 
			//System.out.println("ADAPT" +typeDgenParams);
			if (typeDgenParams.get(i) instanceof PlaceholderType) 
			unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
			else System.out.println("ERROR");
		}
		return Optional.of(new UnifyPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> adaptExt(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType typeD = pair.getLhsType();
		if(!(typeD instanceof ReferenceType) && !(typeD instanceof ExtendsType))
			return Optional.empty();
		
		UnifyType typeExtDs = pair.getRhsType();
		if(!(typeExtDs instanceof ExtendsType))
			return Optional.empty();
		
		if(typeD.getTypeParams().size() == 0 || typeExtDs.getTypeParams().size() == 0)
			return Optional.empty();
		
		UnifyType typeDgen;
		if(typeD instanceof ReferenceType)
			typeDgen = fc.getLeftHandedType(typeD.getName()).orElse(null);
		else {
			Optional<UnifyType> opt = fc.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName());
			typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null;
		}

		if(typeDgen == null)
			return Optional.empty();
		
		Set<UnifyType> grArg = fc.grArg(typeDgen, new HashSet<>());
		
		Optional<UnifyType> opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny();

		if(!opt.isPresent())
			return Optional.empty();
		
		UnifyType newLhs = ((ExtendsType) opt.get()).getExtendedType();
		
		TypeParams typeDParams = typeD.getTypeParams();
		TypeParams typeDgenParams = typeDgen.getTypeParams();
		
		Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
		for(int i = 1; i < typeDParams.size(); i++) 
			unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
		
		return Optional.of(new UnifyPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> adaptSup(UnifyPair pair, IFiniteClosure fc) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType typeDs = pair.getLhsType();
		if(!(typeDs instanceof ReferenceType) && !(typeDs instanceof SuperType))
			return Optional.empty();
		
		UnifyType typeSupD = pair.getRhsType();
		if(!(typeSupD instanceof SuperType))
			return Optional.empty();
		
		if(typeDs.getTypeParams().size() == 0 || typeSupD.getTypeParams().size() == 0)
			return Optional.empty();
		
		
		Optional<UnifyType> opt = fc.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName());
		
		if(!opt.isPresent()) 
			return Optional.empty();
		
		UnifyType typeDgen = opt.get();
		UnifyType typeSupDgen = new SuperType(typeDgen);

		// Use of smArg instead of grArg because
		// a in grArg(b) => b in smArg(a)
		Set<UnifyType> smArg = fc.smArg(typeSupDgen, new HashSet<>());
		opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();

		if(!opt.isPresent())
			return Optional.empty();
		
		// New RHS
		UnifyType newRhs = null;
		if(typeDs instanceof ReferenceType)
			newRhs = new ExtendsType(typeDs);
		else
			newRhs = new ExtendsType(((SuperType) typeDs).getSuperedType());
		
		// New LHS
		UnifyType newLhs = opt.get();
		TypeParams typeDParams = typeSupD.getTypeParams();
		TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams();
		
		Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0));
		for(int i = 1; i < typeDParams.size(); i++) 
			unif.add((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i));
		
		return Optional.of(new UnifyPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
	}

	/**
	 * Finds the permutation pi of the type arguments of two types based on the finite closure
	 * @param cArgs The type which arguments are permuted
	 * @param dArgs The other type
	 * @return An array containing the values of pi for every type argument of C or an empty array if the search failed.
	 */
	private int[] pi(TypeParams cArgs, TypeParams dArgs) {
		if(!(cArgs.size()==dArgs.size()))throw new DebugException("Fehler in Unifizierung");
	
		int[] permutation = new int[dArgs.size()];
		
		boolean succ = true;
		for (int dArgIdx = 0; dArgIdx < dArgs.size() && succ; dArgIdx++) {
			UnifyType dArg = dArgs.get(dArgIdx);
			succ = false;
			for (int pi = 0; pi < cArgs.size(); pi++)
				if (cArgs.get(pi).getName().equals(dArg.getName())) {
					permutation[dArgIdx] = pi;
					succ = true;
					break;
				}
		}

		return succ ? permutation : new int[0];
	}

	public Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs) {
		return subst(pairs, new ArrayList<>());
	}
	
	@Override
	public Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs, List<Set<Set<UnifyPair>>> oderConstraints) {
		HashMap<UnifyType, Integer> typeMap = new HashMap<>();
		
		Stack<UnifyType> occuringTypes = new Stack<>();
		
		for(UnifyPair pair : pairs) {
			occuringTypes.push(pair.getLhsType());
			occuringTypes.push(pair.getRhsType());
		}
		
		while(!occuringTypes.isEmpty()) {
			UnifyType t1 = occuringTypes.pop();
			if(!typeMap.containsKey(t1))
				typeMap.put(t1, 0);
			typeMap.put(t1, typeMap.get(t1)+1);
			
			if(t1 instanceof ExtendsType)
				occuringTypes.push(((ExtendsType) t1).getExtendedType());
			if(t1 instanceof SuperType)
				occuringTypes.push(((SuperType) t1).getSuperedType());
			else
				t1.getTypeParams().forEach(x -> occuringTypes.push(x));	
		}
		
		Queue<UnifyPair> result1 = new LinkedList<UnifyPair>(pairs);
		ArrayList<UnifyPair> result = new ArrayList<UnifyPair>();
		boolean applied = false;
		
		while(!result1.isEmpty()) {
			UnifyPair pair = result1.poll();
			PlaceholderType lhsType = null;
			UnifyType rhsType;
			
			if(pair.getPairOp() == PairOperator.EQUALSDOT
					&& pair.getLhsType() instanceof PlaceholderType)
				lhsType = (PlaceholderType) pair.getLhsType();
				rhsType = pair.getRhsType(); //PL eingefuegt 2017-09-29 statt !((rhsType = pair.getRhsType()) instanceof PlaceholderType)
			if(lhsType != null 
					//&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType) //PL geloescht am 2017-09-29 Begründung: auch Typvariablen muessen ersetzt werden.
					&& typeMap.get(lhsType) > 1  // The type occurs in more pairs in the set than just the recent pair.
					&& !rhsType.getTypeParams().occurs(lhsType) 
					&& !((rhsType instanceof WildcardType) && ((WildcardType)rhsType).getWildcardedType().equals(lhsType))) //PL eigefuegt 2018-02-18
			{
				Unifier uni = new Unifier(lhsType,  rhsType);
				result = result.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(ArrayList::new));
				result1 = result1.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(LinkedList::new));
				
				Function<? super Set<UnifyPair>,? extends HashSet<UnifyPair>> applyUni = b -> b.stream().map(
						x -> uni.apply(pair,x)).collect(Collectors.toCollection(HashSet::new));
				List<Set<Set<UnifyPair>>> oderConstraintsRet = new ArrayList<>();
				for(Set<Set<UnifyPair>> oc : oderConstraints) {
					//Set<Set<UnifyPair>> ocRet = new HashSet<>();
					//for(Set<UnifyPair> cs : oc) {
						Set<Set<UnifyPair>> csRet = oc.stream().map(applyUni).collect(Collectors.toCollection(HashSet::new));
						oderConstraintsRet.add(csRet);
					//}
				}
				oderConstraints.replaceAll(oc -> oc.stream().map(applyUni).collect(Collectors.toCollection(HashSet::new)));
				/*
						oderConstraints = oderConstraints.stream().map(
						a -> a.stream().map(applyUni
								//b -> b.stream().map(
								//		x -> uni.apply(pair,x)).collect(Collectors.toCollection(HashSet::new) )
								).collect(Collectors.toCollection(HashSet::new))
						).collect(Collectors.toList(ArrayList::new));
				}
				*/
				applied = true;
			}
			result.add(pair);
		}
		
		return applied ? Optional.of(new HashSet<>(result)) : Optional.empty();
	}

	@Override
	public Optional<UnifyPair> reduceWildcardLow(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof ExtendsType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); 
	}

	@Override
	public Optional<UnifyPair> reduceWildcardLowRight(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof ExtendsType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> reduceWildcardUp(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof SuperType) || !(rhsType instanceof SuperType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), ((SuperType) lhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<UnifyPair> reduceWildcardUpRight(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof SuperType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), lhsType, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
	}

	/* PL 2018-03-06 auskommentiert sind mutmaßlich falsch
	 * vgl. JAVA_BSP/Wildcard6.java
	@Override
	public Optional<UnifyPair> reduceWildcardLowUp(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof SuperType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((SuperType) rhsType).getSuperedType(), PairOperator.EQUALSDOT));
	}

	@Override
	public Optional<UnifyPair> reduceWildcardUpLow(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof SuperType) || !(rhsType instanceof ExtendsType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(((SuperType) lhsType).getSuperedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT));
	}

	
	@Override
	public Optional<UnifyPair> reduceWildcardLeft(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType rhsType = pair.getRhsType();
		if(!(rhsType instanceof ReferenceType))
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		
		if(lhsType instanceof WildcardType)
			return Optional.of(new UnifyPair(((WildcardType) lhsType).getWildcardedType(), rhsType, PairOperator.EQUALSDOT));
		
		return Optional.empty();
	}
	*/
	@Override
	public Optional<Set<UnifyPair>> reduceFunN(UnifyPair pair) {
		if((pair.getPairOp() != PairOperator.SMALLERDOT)  
		  && (pair.getPairOp() != PairOperator.EQUALSDOT))     //PL 2017-10-03 hinzugefuegt  
		                                                       //da Regel auch fuer EQUALSDOT anwendbar 
			                                                   //TODO: fuer allen anderen Relationen noch pruefen
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		
		if(!(lhsType instanceof FunNType) || !(rhsType instanceof FunNType))
			return Optional.empty();

		FunNType funNLhsType = (FunNType) lhsType;
		FunNType funNRhsType = (FunNType) rhsType;
		
		if(funNLhsType.getN() != funNRhsType.getN())
			return Optional.empty();
		
		Set<UnifyPair> result = new HashSet<UnifyPair>();
		if (pair.getPairOp() == PairOperator.SMALLERDOT) { 
			result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
			for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
				result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
			}
		}
		else {// pair.getPairOp() == PairOperator.EQUALDOT
			result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
			for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
				result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
			}
		}
		result.stream().forEach(x -> { UnifyType l = x.getLhsType();
        								   if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } 
        								   UnifyType r = x.getRhsType();
        								   if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
								     } );
		try {
			logFile.write("FUNgreater: " + pair + "\n");
				logFile.write("FUNred: " + result + "\n");
				logFile.flush();
			}
		catch (IOException e) {
			System.out.println("logFile-Error");
		}
		return Optional.of(result);
	}
	
	
	@Override
	public Optional<Set<UnifyPair>> greaterFunN(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		
		if(!(lhsType instanceof FunNType) || !(rhsType instanceof PlaceholderType))
			return Optional.empty();

		FunNType funNLhsType = (FunNType) lhsType;

		Set<UnifyPair> result = new HashSet<UnifyPair>();
		
		Integer variance = ((PlaceholderType)rhsType).getVariance();
		Integer inversVariance = distributeVariance.inverseVariance(variance);
		
		UnifyType[] freshPlaceholders = new UnifyType[funNLhsType.getTypeParams().size()];
		for(int i = 0; i < freshPlaceholders.length-1; i++) {
			freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
			((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance);
		}
		freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder();
		((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance);
		result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), freshPlaceholders[funNLhsType.getTypeParams().size()-1], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
		
		for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
			result.add(new UnifyPair(freshPlaceholders[i], funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
		}
		
		result.add(new UnifyPair(rhsType, funNLhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		
		result.stream().forEach(x -> { UnifyType l = x.getLhsType();
									   if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } 
									   UnifyType r = x.getRhsType();
									   if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
									 } );
		try {
			logFile.write("FUNgreater: " + pair + "\n");
			logFile.write("FUNgreater: " + result + "\n");
			logFile.flush();
		}
	catch (IOException e) {
		System.out.println("lofFile-Error");
	}
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> smallerFunN(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOT)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		
		if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof FunNType))
			return Optional.empty();

		FunNType funNRhsType = (FunNType) rhsType;

		Set<UnifyPair> result = new HashSet<UnifyPair>();
		
		Integer variance = ((PlaceholderType)lhsType).getVariance();
		Integer inversVariance = distributeVariance.inverseVariance(variance);
		
		UnifyType[] freshPlaceholders = new UnifyType[funNRhsType.getTypeParams().size()];
		for(int i = 0; i < freshPlaceholders.length-1; i++) {
			freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
			((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance);
		}
		freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder();
		((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance);
		
		result.add(new UnifyPair(freshPlaceholders[funNRhsType.getTypeParams().size()-1], funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
		
		for(int i = 0; i < funNRhsType.getTypeParams().size()-1; i++) {
			result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), freshPlaceholders[i], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
		}
		
		result.add(new UnifyPair(lhsType, funNRhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		
		result.stream().forEach(x -> { UnifyType l = x.getLhsType();
		   							   if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } 
		   							   UnifyType r = x.getRhsType();
		   							   if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
									 } );
		try {
			logFile.write("FUNgreater: " + pair + "\n");
			logFile.write("FUNsmaller: " + result + "\n");
			logFile.flush();
		}
	catch (IOException e) {
		System.out.println("lofFile-Error");
	}
		return Optional.of(result);
	}

	@Override
	public Optional<UnifyPair> reduceTph(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof ReferenceType))
			return Optional.empty();
		
		return Optional.of(new UnifyPair(lhsType, rhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
	}

	@Override
	public Optional<Set<UnifyPair>> reduceTphExt(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof PlaceholderType))
			return Optional.empty();
		
		UnifyType extendedType = ((ExtendsType)lhsType).getExtendedType();
		
		if (extendedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? extends a <.? a
		
		boolean isGen = extendedType instanceof PlaceholderType && !((PlaceholderType) extendedType).isGenerated();
		
		Set<UnifyPair> result = new HashSet<>();
		if(isGen)
			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		else {
			UnifyType freshTph = PlaceholderType.freshPlaceholder();
			result.add(new UnifyPair(rhsType, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
			result.add(new UnifyPair(extendedType, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
		}
		
		return Optional.of(result);
	}

	@Override
	public Optional<Set<UnifyPair>> reduceTphSup(UnifyPair pair) {
		if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
			return Optional.empty();
		
		UnifyType lhsType = pair.getLhsType();
		UnifyType rhsType = pair.getRhsType();
		if(!(lhsType instanceof SuperType) || !(rhsType instanceof PlaceholderType))
			return Optional.empty();
		
		UnifyType superedType = ((SuperType)lhsType).getSuperedType();
		
		if (superedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? super a <.? a
		
		boolean isGen = superedType instanceof PlaceholderType && !((PlaceholderType) superedType).isGenerated();
		
		Set<UnifyPair> result = new HashSet<>();
		if(isGen)
			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
		else {
			UnifyType freshTph = PlaceholderType.freshPlaceholder();
			result.add(new UnifyPair(rhsType, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
			Set<UnifyType> fBounded = pair.getfBounded();
			fBounded.add(lhsType);
			result.add(new UnifyPair(freshTph, superedType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair(), fBounded));
		}
		
		return Optional.of(result);
	}
}
