package unify;

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

import junit.framework.Assert;

import org.junit.Test;

import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify;
import de.dhbwstuttgart.typinference.unify.model.MPair;
import de.dhbwstuttgart.typinference.unify.model.Type;
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;

public class StandardUnifyTest {
	
	@Test
	public void testUnify() {
		IUnify unify = new MartelliMontanariUnify();
		TypeFactory tf = new TypeFactory();
		
		/*
		 * Positive Tests
		 */
		
		Type x = tf.getPlaceholderType("x");
		Type y = tf.getPlaceholderType("y");
		Type z = tf.getPlaceholderType("z");
		Type f = tf.getSimpleType("f", x);
		
		// {x =. z, f<x> = y}
		Set<MPair> terms = new HashSet<MPair>();
		terms.add(new MPair(x, z, PairOperator.EQUALSDOT));
		terms.add(new MPair(f, y, PairOperator.EQUALSDOT));
		
		System.out.println(unify.unify(terms).get());
		
		// {f<g<x>,x> = f<y,a>}
		Type g = tf.getSimpleType("g", "x");
		Type f1 = tf.getSimpleType("f", g, x);
		Type a = tf.getExtendsType(tf.getPlaceholderType("a"));
		Type f2 = tf.getSimpleType("f", y, a);
		
		terms = new HashSet<>();
		terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT));
		
		System.out.println(unify.unify(terms).get());
		
		/*
		 * Negative Tests
		 */
		
		// {f(x) =. x}
		f = tf.getSimpleType("f", x);
		terms = new HashSet<>();
		terms.add(new MPair(f, x, PairOperator.EQUALSDOT));
		Assert.assertFalse(unify.unify(terms).isPresent());
		
		// {f(x) =. f(x,y)}
		f1 = tf.getSimpleType("f", "x");
		f2 = tf.getSimpleType("f", "x", "y");
		terms = new HashSet<>();
		terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT));
		Assert.assertFalse(unify.unify(terms).isPresent());
		
		// {f(x) =. g(x)}
		f1 = tf.getSimpleType("f", "x");
		f2 = tf.getSimpleType("g", "x");
		terms = new HashSet<>();
		terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT));
		Assert.assertFalse(unify.unify(terms).isPresent());
	}
}