merge

src/de/dhbwstuttgart/core/JavaTXCompiler.java

@@ -102,8 +102,8 @@ public class JavaTXCompiler {
 
             System.out.println(xConsSet);
             Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure);
-            System.out.println("RESULT: " + result);
+            System.out.println("RESULT: " + result.size());
-            results.addAll(result);
+            //results.addAll(result);
         }
         return results.stream().map((unifyPairs ->
                 new ResultSet(UnifyTypeFactory.convert(unifyPairs, generateTPHMap(cons))))).collect(Collectors.toList());

src/de/dhbwstuttgart/typeinference/unify/Match.java

@@ -0,0 +1,89 @@
+package de.dhbwstuttgart.typeinference.unify;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import de.dhbwstuttgart.typeinference.unify.interfaces.IMatch;
+import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
+import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
+import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
+import de.dhbwstuttgart.typeinference.unify.model.Unifier;
+import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
+import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
+
+/**
+ * Implementation of match derived from unification algorithm.
+ * @author Martin Pluemicke
+ */
+public class Match implements IMatch {
+
+	@Override
+	public Optional<Unifier> match(ArrayList<UnifyPair> termsList) {
+		
+		// Start with the identity unifier. Substitutions will be added later.
+		Unifier mgu = Unifier.identity();
+		
+		// Apply rules while possible
+		int idx = 0;
+		while(idx < termsList.size()) {
+			UnifyPair pair = termsList.get(idx);
+			UnifyType rhsType = pair.getRhsType();
+			UnifyType lhsType = pair.getLhsType();
+			TypeParams rhsTypeParams = rhsType.getTypeParams();
+			TypeParams lhsTypeParams = lhsType.getTypeParams();
+			
+			// REDUCE - Rule
+			if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
+				Set<UnifyPair> result = new HashSet<>();
+				
+				// f<...> = g<...> with f != g are not unifiable
+				if(!rhsType.getName().equals(lhsType.getName()))
+					return Optional.empty(); // conflict
+				// f<t1,...,tn> = f<s1,...,sm> are not unifiable
+				if(rhsTypeParams.size() != lhsTypeParams.size())
+					return Optional.empty(); // conflict
+				// f = g is not unifiable (cannot be f = f because erase rule would have been applied)
+				//if(rhsTypeParams.size() == 0)
+					//return Optional.empty();
+					
+				// Unpack the arguments
+				for(int i = 0; i < rhsTypeParams.size(); i++)
+					result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
+				
+				termsList.remove(idx);
+				termsList.addAll(result);
+				continue;
+			}
+			
+			// DELETE - Rule
+			if(pair.getRhsType().equals(pair.getLhsType())) {
+				termsList.remove(idx);
+				continue; 
+			}
+
+			// SWAP - Rule
+			if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
+				return Optional.empty(); // conflict
+			}
+			
+			// OCCURS-CHECK
+			//deleted
+			
+			// SUBST - Rule
+			if(lhsType instanceof PlaceholderType) {
+				mgu.add((PlaceholderType) lhsType, rhsType);
+				termsList = termsList.stream().map(mgu::applyleft).collect(Collectors.toCollection(ArrayList::new));
+				idx = idx+1 == termsList.size() ? 0 : idx+1;
+				continue;
+			}
+			
+			idx++;
+		}
+		
+		return Optional.of(mgu);
+	}
+}

src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java

@@ -34,6 +34,7 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 
 	private static final long serialVersionUID = 1L;
+	private static int i = 0;
 
 	/**
 	 * The implementation of setOps that will be used during the unification
@@ -77,6 +78,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 		/*
 		 * Step 1: Repeated application of reduce, adapt, erase, swap 
 		 */
+		//System.out.println("Unifikation: " + eq);
 		Set<UnifyPair> eq0 = applyTypeUnificationRules(eq, fc);
 
 		/*
@@ -97,6 +99,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 		// cartesian product of the sets created by pattern matching.
 		List<Set<Set<UnifyPair>>> topLevelSets = new ArrayList<>();
 		
+		System.out.println(eq2s);
+		
 		if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
 			Set<Set<UnifyPair>> wrap = new HashSet<>();
 			wrap.add(eq1s);
@@ -134,12 +138,16 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 		// Sub cartesian products of the second level (pattern matched) sets
 		// "the big (x)"
 		for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
+			//System.out.println("secondLevelSet "+secondLevelSet.size());
 			List<Set<Set<UnifyPair>>> secondLevelSetList = new ArrayList<>(secondLevelSet);
 			Set<List<Set<UnifyPair>>> cartResult = setOps.cartesianProduct(secondLevelSetList);
-			
+			//System.out.println("CardResult: "+cartResult.size());
 			// Flatten and add to top level sets
 			Set<Set<UnifyPair>> flat = new HashSet<>();
+			int j = 0;
 			for(List<Set<UnifyPair>> s : cartResult) {
+				j++;
+				//System.out.println("s from CardResult: "+cartResult.size() + " " + j);
 				Set<UnifyPair> flat1 = new HashSet<>();
 				for(Set<UnifyPair> s1 : s)
 					flat1.addAll(s1);
@@ -164,6 +172,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 			/*
 			 * Step 5: Substitution
 			 */
+			System.out.println("vor Subst: " + eqPrime);
 			Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
 			
 			/*
@@ -176,11 +185,13 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 					                              //(!eqPrimePrime.isPresent()) erfolgt ist, ist das Ergebnis erzielt.
 					eqPrimePrimeSet.add(eqPrime);
 				else if(eqPrimePrime.isPresent()) {
+					System.out.println("nextStep: " + eqPrimePrime.get());
 					TypeUnifyTask fork = new TypeUnifyTask(eqPrimePrime.get(), fc, true);
 					forks.add(fork);
 					fork.fork();
 				}
 				else {
+					System.out.println("nextStep: " + eqPrime);
 					TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc, true);
 					forks.add(fork);
 					fork.fork();
@@ -381,9 +392,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 			UnifyType rhsType = pair.getRhsType();
 	
 			// Case 1: (a <. Theta')
-			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
+			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
-				result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
+				System.out.println(pair);
-			
+				Set<Set<UnifyPair>> x1 = unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc);
+				System.out.println(x1);
+				result.get(0).add(x1);
+			}
 			// Case 2: (a <.? ? ext Theta')
 			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
 				result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
@@ -442,13 +456,24 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 				break;
 			}
 		
-		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
+		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());//cs= [java.util.Vector<NP>, java.util.Vector<java.util.Vector<java.lang.Integer>>, ????java.util.Vector<gen_hv>???]
-		cs.add(thetaPrime);
+		
+		//PL 18-02-06 entfernt, kommt durch unify wieder rein
+		//cs.add(thetaPrime);
+		//PL 18-02-06 entfernt
 		
 		for(UnifyType c : cs) {
-			Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
+			//PL 18-02-05 getChildren durch smaller ersetzt in getChildren werden die Varianlen nicht ersetzt.
-		    thetaQs.add(thetaPrime); //PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert, 
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().collect(Collectors.toCollection(HashSet::new));
+			//Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
+		    //thetaQs.add(thetaPrime); //PL 18-02-05 wieder geloescht
+			                           //PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert, 
 		                               //da children offensichtlich ein echtes kleiner und kein kleinergleich ist
+			
+			//PL 18-02-06: eingefuegt, thetaQs der Form V<V<...>> <. V'<V<...>> werden entfernt
+			thetaQs = thetaQs.stream().filter(ut -> ut.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			//PL 18-02-06: eingefuegt
+			
 			Set<UnifyType> thetaQPrimes = new HashSet<>();
 			TypeParams cParams = c.getTypeParams();
 			if(cParams.size() == 0)
@@ -464,6 +489,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 			}
 			
 			for(UnifyType tqp : thetaQPrimes) {
+				//System.out.println(tqp.toString());
+				//i++;
+				//System.out.println(i);
+				//if (i == 62)
+				//	System.out.println(tqp.toString());
 				Optional<Unifier> opt = stdUnify.unify(tqp, thetaPrime);
 				if (!opt.isPresent())
 					continue;
@@ -474,10 +504,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
 				for (Entry<PlaceholderType, UnifyType> sigma : unifier)
 					substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
 				
-				List<UnifyType> freshTphs = new ArrayList<>();
+				//List<UnifyType> freshTphs = new ArrayList<>(); PL 18-02-06 in die For-Schleife verschoben
 				for (UnifyType tq : thetaQs) {
 					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq)); 
 					for(UnifyType theta : smaller) {
+						List<UnifyType> freshTphs = new ArrayList<>();
 						Set<UnifyPair> resultPrime = new HashSet<>();
 						
 						for(int i = 0; !allGen && i < theta.getTypeParams().size(); i++) {

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

@@ -0,0 +1,35 @@
+package de.dhbwstuttgart.typeinference.unify.interfaces;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
+import de.dhbwstuttgart.typeinference.unify.model.Unifier;
+import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
+
+/**
+ * Match
+ * @author Martin Pluemicke
+ */
+public interface IMatch {
+	
+	/**
+	 * Finds the most general unifier sigma of the set {t1,...,tn} so that
+	 * sigma(t1) = sigma(t2) = ... = sigma(tn). 
+	 * @param terms The set of terms to be unified
+	 * @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
+	 */
+	public Optional<Unifier> match(ArrayList<UnifyPair> termsList);
+
+	/**
+	 * Finds the most general unifier sigma of the set {t1,...,tn} so that
+	 * sigma(t1) = sigma(t2) = ... = sigma(tn). 
+	 * @param terms The set of terms to be unified
+	 * @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
+	 */
+	
+
+}

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

@@ -8,7 +8,11 @@ import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
 
+//PL 18-02-05 Unifier durch Matcher ersetzt
+//mus greater noch erstezt werden
 import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
+
+import de.dhbwstuttgart.typeinference.unify.Match;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 
@@ -46,6 +50,13 @@ public class FiniteClosure implements IFiniteClosure {
 			if(pair.getPairOp() != PairOperator.SMALLER)
 				continue;
 			
+			//VERSUCH PL 18-02-06
+			//koennte ggf. die FC reduzieren
+			//TO DO: Ueberpruefen, ob das sinnvll und korrekt ist 
+			//if (!pair.getLhsType().getTypeParams().arePlaceholders() 
+			//		&& !pair.getRhsType().getTypeParams().arePlaceholders())
+			//	continue;
+;			
 			// Add nodes if not already in the graph
 			if(!inheritanceGraph.containsKey(pair.getLhsType()))
 				inheritanceGraph.put(pair.getLhsType(), new Node<UnifyType>(pair.getLhsType()));
@@ -93,7 +104,9 @@ public class FiniteClosure implements IFiniteClosure {
 	private Set<UnifyType> computeSmaller(Set<UnifyType> types) {
 		HashSet<UnifyType> result = new HashSet<>();
 		
-		IUnify unify = new MartelliMontanariUnify();
+		//PL 18-02-05 Unifier durch Matcher ersetzt
+		//IUnify unify = new MartelliMontanariUnify();
+		Match match = new Match();
 		
 		for(UnifyType t : types) {
 			
@@ -112,10 +125,16 @@ public class FiniteClosure implements IFiniteClosure {
 				continue;
 			
 			// if T <* T' then sigma(T) <* sigma(T')
-			Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
+			Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName()); //cadidates= [???Node(java.util.Vector<java.util.Vector<java.lang.Integer>>)???
+			                                                                       // , Node(java.util.Vector<gen_hv>)
+			                                                                         //]
 			for(Node<UnifyType> candidate :  candidates) {
 				UnifyType theta2 = candidate.getContent();
-				Optional<Unifier> optSigma = unify.unify(theta2, t);
+				//PL 18-02-05 Unifier durch Matcher ersetzt ANFANG
+				ArrayList<UnifyPair> termList= new ArrayList<UnifyPair>();
+				termList.add(new UnifyPair(theta2,t, PairOperator.EQUALSDOT));
+				Optional<Unifier> optSigma = match.match(termList);
+				//PL 18-02-05 Unifier durch Matcher ersetzt ENDE
 				if(!optSigma.isPresent())
 					continue;
 				

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

@@ -94,6 +94,7 @@ class Node<T> {
 	
 	@Override
 	public String toString() {
-		return "Node(" + content.toString() + ")\n";
+		return "Elem: Node(" + content.toString() + ")\nPrec: " + getContentOfPredecessors().toString() 
+				+ "\nDesc: " + getContentOfDescendants().toString() + "\n\n";
 	}
 }

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

@@ -102,9 +102,9 @@ public final class TypeParams implements Iterable<UnifyType>{
 				if(p.equals(t))
 					return true;
 			}
-			else
+			else {
 				if(p.getTypeParams().occurs(t))
-					return true;
+					return true; }
 		return false;
 	}
 	

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

@@ -66,6 +66,14 @@ public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<P
 		return new UnifyPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp());
 	}
 	
+	/**
+	 * Applies the unifier to the left terms of the pair.
+	 * @return A new pair where the left and right-hand side are applied
+	 */
+	public UnifyPair applyleft(UnifyPair p) {
+		return new UnifyPair(this.apply(p.getLhsType()), p.getRhsType(), p.getPairOp());
+	}
+	
 	/**
 	 * True if the typevariable t will be substituted if the unifier is applied.
 	 * false otherwise.

test/javFiles/Matrix.jav

@@ -6,21 +6,21 @@ class Matrix extends Vector<Vector<Integer>> {
     mul(m) {
         var ret = new Matrix();
         var i = 0;
-        while(i < size()) {
+        //while(i < size()) {
             var v1 = this.elementAt(i);
-            var v2 = new Vector<Integer>();
+            //var v2 = new Vector<Integer>();
-            var j = 0;
+            //var j = 0;
-            while(j < v1.size()) {
+            //while(j < v1.size()) {
-                var erg = 0;
+                //var erg = 0;
-                var k = 0;
+                //var k = 0;
-                while(k < v1.size()) {
+                //while(k < v1.size()) {
-                    erg = erg + v1.elementAt(k)
+                    //erg = erg + v1.elementAt(k)
-                             * m.elementAt(k).elementAt(j);
+                    //         * m.elementAt(k).elementAt(j);
-                    k++; }
+                    //k++; }
-                v2.addElement(new Integer(erg));
+                //v2.addElement(new Integer(erg));
-                j++; }
+                //j++; }
-            ret.addElement(v2);
+            //ret.addElement(v2);
-            i++; }
+            //i++; }
         return ret;
     }
 }