regel 4 für paare (a <. Theta') (funktioniert zu 99 Prozent noch nicht

richtig)

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

@@ -50,4 +50,5 @@ public interface IFiniteClosure {
 	public Set<Type> smArg(PlaceholderType type);
 	
 	public Optional<Type> getGenericType(String typeName);
+	public Set<Type> getAllTypes(String typeName);
 }

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

@@ -4,6 +4,7 @@ import java.util.Optional;
 import java.util.Set;
 
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
+import de.dhbwstuttgart.typeinference.unify.model.Type;
 import de.dhbwstuttgart.typeinference.unifynew.Unifier;
 
 /**
@@ -12,4 +13,6 @@ import de.dhbwstuttgart.typeinference.unifynew.Unifier;
  */
 public interface IUnify {
 	public Optional<Set<MPair>> unify(Set<MPair> terms);
+	
+	public Optional<Set<MPair>> unify(Type t1, Type t2);
 }

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

@@ -4,6 +4,7 @@ import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Optional;
 import java.util.Set;
+import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
@@ -205,4 +206,11 @@ public class FiniteClosure implements IFiniteClosure {
 		
 		return Optional.empty();
 	}
+	
+	@Override
+	public Set<Type> getAllTypes(String typeName) {
+		if(!strInheritanceGraph.containsKey(typeName))
+			return new HashSet<>();
+		return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new));
+	}
 }

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

@@ -5,7 +5,6 @@ import java.util.LinkedList;
 import java.util.Optional;
 import java.util.Queue;
 import java.util.Set;
-import java.util.Stack;
 import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
@@ -21,6 +20,13 @@ import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
  */
 public class MartelliMontanariUnify implements IUnify {
 
+	@Override
+	public Optional<Set<MPair>> unify(Type t1, Type t2) {
+		Set<MPair> terms = new HashSet<MPair>();
+		terms.add(new MPair(t1, t2, PairOperator.EQUALSDOT));
+		return unify(terms);
+	}
+	
 	@Override
 	public Optional<Set<MPair>> unify(Set<MPair> terms) {
 		Queue<MPair> termsQ = new LinkedList<>(terms);

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

@@ -16,6 +16,7 @@ import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
 import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
+import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
 import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
@@ -223,7 +224,36 @@ public class Unify {
 	
 			// Case 1: (a <. Theta')
 			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
-				// TODO
+				IUnify unify = new MartelliMontanariUnify();
+				
+				Set<Type> possibleCs = fc.getAllTypes(rhsType.getName());
+				Set<Type> possibleThetas = possibleCs.stream()
+						.flatMap(x -> fc.smaller(x).stream())
+						.collect(Collectors.toCollection(HashSet::new));
+				Set<Type> possibleThetaPrimes = possibleThetas.stream()
+						.flatMap(x -> getAllInstantiations(x).stream())
+						.collect(Collectors.toCollection(HashSet::new));
+				
+				Set<Unifier> unifiers = possibleThetaPrimes.stream()
+						.map(x -> unify.unify(x, rhsType))
+						.filter(x -> x.isPresent())
+						.flatMap(x -> x.get().stream())
+						.map(x -> new Unifier(x.getLhsType(), x.getRhsType()))
+						.collect(Collectors.toCollection(HashSet::new));
+				
+				Set<Type> thetas = new HashSet<>();
+				
+				for(Unifier sigma : unifiers)
+					for(Type thetaQuer : possibleThetas)
+						thetas.addAll(fc.smaller(sigma.apply(thetaQuer)));
+				
+				Set<MPair> resultSet = new HashSet<>();
+				thetas.forEach(x -> resultSet.add(new MPair(lhsType, x, PairOperator.EQUALSDOT)));
+				unifiers.forEach(x -> resultSet.add(new MPair(x.getSource(), x.getTarget(), PairOperator.EQUALSDOT)));
+				
+				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
 			}
 			
 			// Case 2: (a <.? ? ext Theta')
@@ -278,4 +308,8 @@ public class Unify {
 		
 		return result;
 	}
+	
+	private Set<Type> getAllInstantiations(Type t) {
+		return new HashSet<>();
+	}
 }

test/unify/UnifyTest.java

@@ -27,13 +27,15 @@ public class UnifyTest extends Unify {
 		// Vector<Integer> <. Vector<A>
 		// Vector<Integer <. Vector<C>
 		// A <. Integer
+		// Number <. A
 		// Double <. B
 		// B <. Object
 		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.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.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT));
-		eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), 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));
 		
 		System.out.println(this.unify(eq, fc));