package unify;

import java.util.HashSet;
import java.util.Set;

import junit.framework.Assert;

import org.junit.Test;

import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;

public class StandardUnifyTest {
	
	@Test
	public void testUnify() {
		IUnify unify = new MartelliMontanariUnify();
		TypeFactory tf = new TypeFactory();
		
		/*
		 * Positive Tests
		 */
		
		UnifyType x = tf.getPlaceholderType("x");
		UnifyType y = tf.getPlaceholderType("y");
		UnifyType f = tf.getSimpleType("f", x);
		
		// {f<x> = y}
		Set<UnifyPair> terms = new HashSet<UnifyPair>();

		System.out.println(unify.unify(f, y).get());
		
		// TODO ist das ergebnis { (x -> ? extends a), (y -> g<x>) } in der richtigen form oder
		// muss es { (x -> ? extends a), (y -> g<? extends a>) } sein?
		// {f<g<x>,x> = f<y, ? extends a>}
		UnifyType g = tf.getSimpleType("g", "x");
		UnifyType f1 = tf.getSimpleType("f", g, x);
		UnifyType a = tf.getExtendsType(tf.getPlaceholderType("a"));
		UnifyType f2 = tf.getSimpleType("f", y, a);
		
		terms = new HashSet<>();

		System.out.println(unify.unify(f1, f2).get());
		
		/*
		 * Negative Tests
		 */
		
		// {f(x) =. x}
		f = tf.getSimpleType("f", x);
		Assert.assertFalse(unify.unify(f, x).isPresent());
		
		// {f(x) =. f(x,y)}
		f1 = tf.getSimpleType("f", "x");
		f2 = tf.getSimpleType("f", "x", "y");
		Assert.assertFalse(unify.unify(f1, f2).isPresent());
		
		// {f(x) =. g(x)}
		f1 = tf.getSimpleType("f", "x");
		f2 = tf.getSimpleType("g", "x");
		Assert.assertFalse(unify.unify(f1, f2).isPresent());
	}
}