standard martelli montanari unifiy fixed

src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java

@@ -1,18 +1,23 @@
 package de.dhbwstuttgart.typeinference.unify.interfaces;
 
+import java.util.Arrays;
 import java.util.Optional;
 import java.util.Set;
+import java.util.stream.Collectors;
 
-import de.dhbwstuttgart.typeinference.unify.model.MPair;
 import de.dhbwstuttgart.typeinference.unify.model.Type;
 import de.dhbwstuttgart.typeinference.unifynew.Unifier;
 
 /**
- * Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari, Ruzicka-Privara or Suciu)
+ * Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari)
  * @author Florian Steurer
  */
 public interface IUnify {
-	public Optional<Set<MPair>> unify(Set<MPair> terms);
 	
-	public Optional<Set<MPair>> unify(Type t1, Type t2);
+	public Optional<Unifier> unify(Set<Type> terms);
+	
+	default public Optional<Unifier> unify(Type... terms) {
+		return unify(Arrays.stream(terms).collect(Collectors.toSet()));
+	}
+
 }

src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java

@@ -36,9 +36,8 @@ public final class PlaceholderType extends Type{
 
 	@Override
 	public Type apply(Unifier unif) {
-		if(this.equals(unif.getSource()))
+		if(unif.hasSubstitute(this))
-			return unif.getTarget();
+			return unif.getSubstitute(this);
-		
 		return this;
 	}
 }

src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java

@@ -44,9 +44,6 @@ public final class SimpleType extends Type {
 
 	@Override
 	public Type apply(Unifier unif) {
-		if(this.equals(unif.getSource()))
-			return unif.getTarget();
-		
 		return new SimpleType(typeName, typeParams.apply(unif));
 	}
 }

src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java

@@ -52,6 +52,13 @@ public final class TypeParams implements Iterable<Type>{
 	public Type get(int i) {
 		return typeParams[i];
 	}
+	
+	public TypeParams set(Type t, int idx) {
+		Type[] newparams = Arrays.copyOf(typeParams, typeParams.length);
+		newparams[idx] = t;
+		return new TypeParams(newparams);
+	}
+	
 
 	@Override
 	public Iterator<Type> iterator() {

src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java

@@ -14,7 +14,6 @@ public class Mapping {
 	
 	public Mapping(Set<de.dhbwstuttgart.syntaxtree.type.Type> types) {
 		for(de.dhbwstuttgart.syntaxtree.type.Type t : types) {
-			// TODO	
 		}
 	}
 	

src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java

@@ -1,18 +1,20 @@
 package de.dhbwstuttgart.typeinference.unifynew;
 
+import java.util.AbstractMap;
+import java.util.ArrayList;
 import java.util.HashSet;
-import java.util.LinkedList;
+import java.util.Iterator;
+import java.util.Map.Entry;
 import java.util.Optional;
-import java.util.Queue;
 import java.util.Set;
 import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
+import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
 import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
 import de.dhbwstuttgart.typeinference.unify.model.Type;
 import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
-import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
 
 /**
  * Implementation of the Martelli-Montanari unification algorithm.
@@ -21,23 +23,29 @@ import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
 public class MartelliMontanariUnify implements IUnify {
 
 	@Override
-	public Optional<Set<MPair>> unify(Type t1, Type t2) {
+	public Optional<Unifier> unify(Set<Type> terms) {
-		Set<MPair> terms = new HashSet<MPair>();
+		if(terms.size() < 2)
-		terms.add(new MPair(t1, t2, PairOperator.EQUALSDOT));
+			return Optional.of(Unifier.IDENTITY);
-		return unify(terms);
-	}
-	
-	@Override
-	public Optional<Set<MPair>> unify(Set<MPair> terms) {
-		Queue<MPair> termsQ = new LinkedList<>(terms);
-		Set<MPair> result = new HashSet<>();
 		
+		ArrayList<MPair> termsQ = new ArrayList<MPair>();
+		Iterator<Type> iter = terms.iterator();
+		Type prev = iter.next();
+		while(iter.hasNext()) {
+			Type next = iter.next();
+			termsQ.add(new MPair(prev, next, PairOperator.EQUALS));
+			prev = next;
+		}
 		
-		while(!termsQ.isEmpty()) {
+		Unifier mgu = Unifier.IDENTITY;
-			MPair pair = termsQ.poll();
+		
+		int idx = 0;
+		while(idx < termsQ.size()) {
+			MPair pair = termsQ.get(idx);
 			
-			if(delete(pair))
+			if(delete(pair)) {
+				termsQ.remove(idx);
 				continue;
+			}
 			
 			Optional<Set<MPair>> optSet = decompose(pair);
 			
@@ -46,6 +54,7 @@ public class MartelliMontanariUnify implements IUnify {
 			
 			if(optSet.isPresent()) {
 				termsQ.addAll(optSet.get());
+				idx = idx+1 == termsQ.size() ? 0 : idx+1;
 				continue;
 			}
 			
@@ -53,25 +62,27 @@ public class MartelliMontanariUnify implements IUnify {
 		
 			if(optPair.isPresent()) {
 				termsQ.add(optPair.get());
+				idx = idx+1 == termsQ.size() ? 0 : idx+1;
 				continue;
 			}
 			
-			Optional<Unifier> optUni = eliminate(pair);
-			
-			if(optUni.isPresent()) {
-				Unifier uni = optUni.get();
-				termsQ = termsQ.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new));
-				result = result.stream().map(uni::apply).collect(Collectors.toCollection(HashSet::new));
-				result.add(pair);
-				continue;
-			}
-			
-			// TODO occurs check notwendig?
 			if(!check(pair)) // Occurs-Check
 				return Optional.empty();
+			
+			Optional<Entry<PlaceholderType, Type>> optUni = eliminate(pair);
+			
+			if(optUni.isPresent()) {
+				Entry<PlaceholderType, Type> substitution = optUni.get();
+				mgu.Add(substitution.getKey(), substitution.getValue());
+				termsQ = termsQ.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new));
+				idx = idx+1 == termsQ.size() ? 0 : idx+1;
+				continue;
+			}
+			
+			idx++;
 		}
 		
-		return Optional.of(result);
+		return Optional.of(mgu);
 	}
 	
 	private boolean delete(MPair pair) {
@@ -103,28 +114,12 @@ public class MartelliMontanariUnify implements IUnify {
 		Type rhs = pair.getRhsType();
 		Type lhs = pair.getLhsType();
 		
-		if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0)
-			return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT));
-		
 		if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType))
 			return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT));
 		
 		return Optional.empty();
 	}
 	
-	private Optional<Unifier> eliminate(MPair pair) {
-		Type rhs = pair.getRhsType();
-		Type lhs = pair.getLhsType();
-		
-		TypeParams rhsTypeParams = rhs.getTypeParams();
-		
-		for(Type t : rhsTypeParams)
-			if(lhs.equals(t))
-				return Optional.empty();
-		
-		return Optional.of(new Unifier(lhs, rhs));
-	}
-	
 	private boolean check(MPair pair) {
 		Type rhs = pair.getRhsType();
 		Type lhs = pair.getLhsType();
@@ -137,4 +132,16 @@ public class MartelliMontanariUnify implements IUnify {
 		
 		return true;
 	}
+	
+	private Optional<Entry<PlaceholderType, Type>> eliminate(MPair pair) {
+		Type rhs = pair.getRhsType();
+		Type lhs = pair.getLhsType();
+		
+		// TODO only apply when lhs is element of vars(termsQ)?
+		
+		if(!(lhs instanceof PlaceholderType))
+			return Optional.empty();
+
+		return Optional.of(new AbstractMap.SimpleImmutableEntry<PlaceholderType, Type>((PlaceholderType) lhs, rhs));
+	}
 }

src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java

@@ -346,9 +346,9 @@ public class RuleSet implements IRuleSet{
 		TypeParams typeDParams = typeD.getTypeParams();
 		TypeParams typeDgenParams = typeDgen.getTypeParams();
 		
-		Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0));
+		Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
 		for(int i = 1; i < typeDParams.size(); i++) 
-			unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
+			unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)));
 		
 		return Optional.of(new MPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT));
 	}
@@ -392,9 +392,9 @@ public class RuleSet implements IRuleSet{
 		TypeParams typeDParams = typeD.getTypeParams();
 		TypeParams typeDgenParams = typeDgen.getTypeParams();
 		
-		Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0));
+		Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
 		for(int i = 1; i < typeDParams.size(); i++) 
-			unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
+			unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)));
 		
 		return Optional.of(new MPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC));
 	}
@@ -444,9 +444,9 @@ public class RuleSet implements IRuleSet{
 		TypeParams typeDParams = typeSupD.getTypeParams();
 		TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams();
 		
-		Unifier unif = new Unifier(typeSupDsgenParams.get(0), typeDParams.get(0));
+		Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0));
 		for(int i = 1; i < typeDParams.size(); i++) 
-			unif.andThen(new Unifier(typeSupDsgenParams.get(i), typeDParams.get(i)));
+			unif.andThen(new Unifier((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i)));
 		
 		return Optional.of(new MPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC));
 	}
@@ -547,7 +547,7 @@ public class RuleSet implements IRuleSet{
 					&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType)
 					&& typeMap.get(lhsType) > 1  // The type occurs in more pairs in the set than just the recent pair.
 					&& !occurs(lhsType, rhsType)) {
-				Unifier uni = new Unifier(lhsType,  rhsType);
+				Unifier uni = new Unifier((PlaceholderType) lhsType,  rhsType);
 				result = result.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new));
 				applied = true;
 			}

src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java

@@ -1,20 +1,20 @@
 package de.dhbwstuttgart.typeinference.unifynew;
 
-import java.util.Set;
+import java.util.HashMap;
+import java.util.Map.Entry;
 import java.util.function.Function;
-import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
+import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
 import de.dhbwstuttgart.typeinference.unify.model.Type;
-import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
 
 public class Unifier implements Function<Type, Type> {
-	private Type source;
+	private HashMap<PlaceholderType, Type> substitutions = new HashMap<>();
-	private Type target;
 	
-	public Unifier(Type source, Type target) {
+	public static Unifier IDENTITY = new Unifier();
-		this.source = source;
+	
-		this.target = target;
+	public Unifier(PlaceholderType source, Type target) {
+		substitutions.put(source, target);
 	}
 	
 	/**
@@ -23,6 +23,10 @@ public class Unifier implements Function<Type, Type> {
 	public Unifier() {
 
 	}
+	
+	public void Add(PlaceholderType source, Type target) {
+		substitutions.put(source, target);
+	}
 
 	@Override
 	public Type apply(Type t) {
@@ -33,17 +37,23 @@ public class Unifier implements Function<Type, Type> {
 		return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp());
 	}
 	
-	public Type getSource() {
+	public boolean hasSubstitute(PlaceholderType t) {
-		return source;
+		return substitutions.containsKey(t);
 	}
 	
-	public Type getTarget() {
+	public Type getSubstitute(Type t) {
-		return target;
+		return substitutions.get(t);
 	}
-	
+
 	@Override
 	public String toString() {
-		return source.toString() + " -> " + target.toString();
+		String result = "{ ";
+		for(Entry<PlaceholderType, Type> entry : substitutions.entrySet())
+			result += "(" + entry.getKey() + " -> " + entry.getValue() + "), ";
+		if(!substitutions.isEmpty())
+			result = result.substring(0, result.length()-2);
+		result += " }";
+		return result;
 	}
 }
 

src/de/dhbwstuttgart/typeinference/unifynew/Unify.java

@@ -23,6 +23,7 @@ import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
 import de.dhbwstuttgart.typeinference.unify.model.SuperType;
 import de.dhbwstuttgart.typeinference.unify.model.Type;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
+import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
 
 
 /**
@@ -231,10 +232,12 @@ public class Unify {
 						.flatMap(x -> fc.smaller(x).stream())
 						.collect(Collectors.toCollection(HashSet::new));
 				Set<Type> possibleThetaPrimes = possibleThetas.stream()
-						.flatMap(x -> getAllInstantiations(x).stream())
+						.flatMap(x -> getAllInstantiations(x, fc).stream())
 						.collect(Collectors.toCollection(HashSet::new));
 				
-				Set<Unifier> unifiers = possibleThetaPrimes.stream()
+				// TODO
+				
+				/*Set<Unifier> unifiers = possibleThetaPrimes.stream()
 						.map(x -> unify.unify(x, rhsType))
 						.filter(x -> x.isPresent())
 						.flatMap(x -> x.get().stream())
@@ -254,6 +257,8 @@ public class Unify {
 				result.add(resultSet);
 				// TODO Speedup - Potenzial durch auschließen unmöglicher kombinationen (z.B. wenn in theta' eine Variable festgelegt ist)
 				// TODO speedup durch pipelining mit streams
+				// TODO speedup teure berechnungen mit proxy rauszögern
+				 */
 			}
 			
 			// Case 2: (a <.? ? ext Theta')
@@ -309,7 +314,12 @@ public class Unify {
 		return result;
 	}
 	
-	private Set<Type> getAllInstantiations(Type t) {
+	private Set<Type> getAllInstantiations(Type t, IFiniteClosure fc) {
-		return new HashSet<>();
+		Set<Type> result = new HashSet<>();
+		result.add(t);
+		return result;
+		
+		// TODO
 	}
+
 }

test/unify/StandardUnifyTest.java

@@ -26,26 +26,24 @@ public class StandardUnifyTest {
 		
 		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}
+		// {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(f, y).get());
 		
-		System.out.println(unify.unify(terms).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,a>}
+		// {f<g<x>,x> = f<y, ? extends 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(f1, f2).get());
-		System.out.println(unify.unify(terms).get());
 		
 		/*
 		 * Negative Tests
@@ -53,22 +51,16 @@ public class StandardUnifyTest {
 		
 		// {f(x) =. x}
 		f = tf.getSimpleType("f", x);
-		terms = new HashSet<>();
+		Assert.assertFalse(unify.unify(f, x).isPresent());
-		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<>();
+		Assert.assertFalse(unify.unify(f1, f2).isPresent());
-		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<>();
+		Assert.assertFalse(unify.unify(f1, f2).isPresent());
-		terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT));
-		Assert.assertFalse(unify.unify(terms).isPresent());
 	}
 }

test/unify/UnifyTest.java

@@ -33,7 +33,7 @@ public class UnifyTest extends Unify {
 		eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT));
 		eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("Integer"), PairOperator.SMALLERDOT));
-		eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT));
+		//eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT));
 		//eq.add(new MPair(tf.getPlaceholderType("B"), tf.getSimpleType("Object"), PairOperator.EQUALSDOT));