From 8eecda2a8ff557a34b17064005b799b2bb770594 Mon Sep 17 00:00:00 2001
From: Florian Steurer <florian.steurer95@gmail.com>
Date: Sat, 26 Dec 2015 16:52:18 +0100
Subject: [PATCH] subst rule

---
 .../typeinference/unifynew/RuleSet.java       | 42 +++++++++++++++++--
 .../typeinference/unifynew/Unify.java         | 12 +++++-
 2 files changed, 50 insertions(+), 4 deletions(-)

diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java
index 1f5cd265..6352aa07 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java
+++ b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java
@@ -2,9 +2,12 @@ package de.dhbwstuttgart.typeinference.unifynew;
 
 import java.util.ArrayList;
 import java.util.HashSet;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Optional;
+import java.util.Queue;
 import java.util.Set;
+import java.util.stream.Collectors;
 
 import junit.framework.Assert;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
@@ -516,9 +519,42 @@ public class RuleSet implements IRuleSet{
 	}
 
 	@Override
-	public Set<MPair> subst(Set<MPair> pair) {
-		// TODO Auto-generated method stub
-		return null;
+	public Set<MPair> subst(Set<MPair> pairs) {
+		HashSet<Type> allTypes = new HashSet<>();
+		pairs.forEach(x -> { allTypes.add(x.getLhsType()); allTypes.add(x.getRhsType()); });
+		
+		Queue<MPair> result = new LinkedList<MPair>(pairs);
+		
+		for(int i = 0; i < result.size(); i++) {
+			MPair pair = result.poll();
+			Type lhsType;
+			Type rhsType;
+			if(pair.getPairOp() == PairOperator.EQUALSDOT 
+					&& ((lhsType = pair.getLhsType()) instanceof PlaceholderType) 
+					&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType)
+					&& occursInSet(lhsType, allTypes)
+					&& !occurs(lhsType, rhsType)) {
+				Unifier uni = new Unifier(lhsType,  rhsType);
+				result = result.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new));
+			}
+			result.add(pair);
+		}
+		
+		return new HashSet<>(result);
+	}
+	
+	private boolean occursInSet(Type t, Set<Type> types) {
+		int origSize = types.size();
+		types.add(t);
+		return types.size() == origSize;
+	}
+	
+	private boolean occurs(Type t1, Type t2) {
+		TypeParams t2Params = t2.getTypeParams();
+		for(Type t2Param : t2Params)
+			if(t1.equals(t2Param) || occurs(t1, t2Param))
+				return true;
+		return false;
 	}
 	
 }
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
index 64313fb7..3626fd05 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
+++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
@@ -88,11 +88,21 @@ public class Unify {
 		 */
 		
 		
+		/*
+		 * TODO 
+		 * Im Paper wird Eq'' genannt, es wird also von einer Menge in einer Menge in einer Menge ausgegangen.
+		 * Durch das flache Kartesische Produkt gibt es hier aber nur Mengen in Mengen.
+		 * Richtig so?
+		 */
+
+		
+		
+		
 		/*
 		 * Step 6: 	a) Restart for pairs where subst was applied
 		 * 			b) Union over everything
 		 */
-
+		
 		 /*
 		  * Step 7: Filter result for solved pairs
 		  */