martelli montanari unifikation

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

@@ -10,5 +10,5 @@ import de.dhbwstuttgart.typinference.unify.model.MPair;
  * @author Florian Steurer
  */
 public interface IUnify {
-	public Unifier unify(Set<MPair> terms);
+	public Set<MPair> unify(Set<MPair> terms);
 }

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

@@ -1,7 +1,12 @@
 package de.dhbwstuttgart.typeinference.unifynew;
 
 import java.util.HashSet;
+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;
 import de.dhbwstuttgart.typinference.unify.model.MPair;
@@ -16,43 +21,85 @@ import de.dhbwstuttgart.typinference.unify.model.TypeParams;
 public class MartelliMontanariUnify implements IUnify {
 
 	@Override
-	public Unifier unify(Set<MPair> terms) {
+	public Set<MPair> unify(Set<MPair> terms) {
-		// TODO Auto-generated method stub
+		Queue<MPair> termsQ = new LinkedList<>(terms);
-		return null;
+		Set<MPair> result = new HashSet<>();
+		
+		
+		while(!termsQ.isEmpty()) {
+			MPair pair = termsQ.poll();
+			
+			if(delete(pair))
+				continue;
+			
+			Optional<Set<MPair>> optSet = decompose(pair);
+			
+			if(optSet == null)
+				return new HashSet<>(); // Unification failed
+			
+			if(optSet.isPresent()) {
+				termsQ.addAll(optSet.get());
+				continue;
+			}
+			
+			Optional<MPair> optPair = swap(pair);
+		
+			if(optPair.isPresent()) {
+				termsQ.add(optPair.get());
+				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));
+				continue;
+			}
+			
+			// TODO occurs check?
+		}
+		
+		return result;
 	}
 	
 	private boolean delete(MPair pair) {
 		return pair.getRhsType().equals(pair.getLhsType());
 	}
 	
-	private Set<MPair> decompose(MPair pair) {
+	private Optional<Set<MPair>> decompose(MPair pair) {
 		Set<MPair> result = new HashSet<>();
 		
 		Type rhs = pair.getRhsType();
 		Type lhs = pair.getLhsType();
 		
-		if(!rhs.getName().equals(lhs.getName()) || rhs.getTypeParams().size() != lhs.getTypeParams().size())
-			return null; // conflict
-			
 		TypeParams rhsTypeParams = rhs.getTypeParams();
 		TypeParams lhsTypeParams = lhs.getTypeParams();
 		
+		if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
+			return Optional.empty();
+		
+		if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size())
+			return null; // conflict
+			
 		for(int i = 0; i < rhsTypeParams.size(); i++)
 			result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
 
-		return result;
+		return Optional.of(result);
 	}
 	
-	private MPair swap(MPair pair) {
+	private Optional<MPair> swap(MPair pair) {
 		Type rhs = pair.getRhsType();
 		Type lhs = pair.getLhsType();
 		
 		if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0)
-			return new MPair(rhs, lhs, PairOperator.EQUALSDOT);
+			return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT));
-		return pair;
+		
+		return Optional.empty();
 	}
 	
-	private Unifier eliminate(MPair pair) {
+	private Optional<Unifier> eliminate(MPair pair) {
 		Type rhs = pair.getRhsType();
 		Type lhs = pair.getLhsType();
 		
@@ -60,9 +107,9 @@ public class MartelliMontanariUnify implements IUnify {
 		
 		for(Type t : rhsTypeParams)
 			if(lhs.equals(t))
-				return new Unifier(); //identity-"unifier"
+				return Optional.empty();
 		
-		return new Unifier(lhs, rhs);
+		return Optional.of(new Unifier(lhs, rhs));
 	}
 	
 	private boolean check(MPair pair) {

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

@@ -346,7 +346,7 @@ public class RuleSet implements IRuleSet{
 		for(int i = 1; i < typeDParams.size(); i++) 
 			unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
 		
-		return Optional.of(new MPair(newLhs.apply(unif), typeDs, PairOperator.SMALLERDOT));
+		return Optional.of(new MPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT));
 	}
 
 	@Override
@@ -392,7 +392,7 @@ public class RuleSet implements IRuleSet{
 		for(int i = 1; i < typeDParams.size(); i++) 
 			unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
 		
-		return Optional.of(new MPair(newLhs.apply(unif), typeExtDs, PairOperator.SMALLERDOTWC));
+		return Optional.of(new MPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC));
 	}
 
 	@Override
@@ -444,7 +444,7 @@ public class RuleSet implements IRuleSet{
 		for(int i = 1; i < typeDParams.size(); i++) 
 			unif.andThen(new Unifier(typeSupDsgenParams.get(i), typeDParams.get(i)));
 		
-		return Optional.of(new MPair(newLhs.apply(unif), newRhs, PairOperator.SMALLERDOTWC));
+		return Optional.of(new MPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC));
 	}
 
 	/**

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

@@ -1,7 +1,10 @@
 package de.dhbwstuttgart.typeinference.unifynew;
 
+import java.util.Set;
 import java.util.function.Function;
+import java.util.stream.Collectors;
 
+import de.dhbwstuttgart.typinference.unify.model.MPair;
 import de.dhbwstuttgart.typinference.unify.model.Type;
 import de.dhbwstuttgart.typinference.unify.model.TypeParams;
 
@@ -26,6 +29,10 @@ public class Unifier implements Function<Type, Type> {
 		return t.apply(this);
 	}
 	
+	public MPair apply(MPair p) {
+		return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp());
+	}
+	
 	public Type getSource() {
 		return source;
 	}