package de.dhbwstuttgart.typeinference.unify;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Optional;
import java.util.Set;
import java.util.stream.Collectors;

import de.dhbwstuttgart.typeinference.unify.interfaces.IMatch;
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
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;

/**
 * Implementation of match derived from unification algorithm.
 * @author Martin Pluemicke
 */
public class Match implements IMatch {

	@Override
	//A<X> =. A<Integer> ==> True
	//A<Integer> =. A<X> ==> False
	public Optional<Unifier> match(ArrayList<UnifyPair> termsList) {
		
		// Start with the identity unifier. Substitutions will be added later.
		Unifier mgu = Unifier.identity();
		
		// Apply rules while possible
		int idx = 0;
		while(idx < termsList.size()) {
			UnifyPair pair = termsList.get(idx);
			UnifyType rhsType = pair.getRhsType();
			UnifyType lhsType = pair.getLhsType();
			TypeParams rhsTypeParams = rhsType.getTypeParams();
			TypeParams lhsTypeParams = lhsType.getTypeParams();
			
			// REDUCE - Rule
			if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
				Set<UnifyPair> result = new HashSet<>();
				
				// f<...> = g<...> with f != g are not unifiable
				if(!rhsType.getName().equals(lhsType.getName()))
					return Optional.empty(); // conflict
				// f<t1,...,tn> = f<s1,...,sm> are not unifiable
				if(rhsTypeParams.size() != lhsTypeParams.size())
					return Optional.empty(); // conflict
				// f = g is not unifiable (cannot be f = f because erase rule would have been applied)
				//if(rhsTypeParams.size() == 0)
					//return Optional.empty();
					
				// Unpack the arguments
				for(int i = 0; i < rhsTypeParams.size(); i++)
					result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
				
				termsList.remove(idx);
				termsList.addAll(result);
				continue;
			}
			
			// DELETE - Rule
			if(pair.getRhsType().equals(pair.getLhsType())) {
				termsList.remove(idx);
				continue; 
			}

			// SWAP - Rule
			if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
				return Optional.empty(); // conflict
			}
			
			// OCCURS-CHECK
			//deleted
			
			// SUBST - Rule
			if(lhsType instanceof PlaceholderType) {
				mgu.add((PlaceholderType) lhsType, rhsType);
				termsList = termsList.stream().map(mgu::applyleft).collect(Collectors.toCollection(ArrayList::new));
				idx = idx+1 == termsList.size() ? 0 : idx+1;
				continue;
			}
			
			idx++;
		}
		
		return Optional.of(mgu);
	}
}
