diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 807c8d7f4..ae702fbaa 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -57,33 +57,48 @@ public class Unify { * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia */ - // All Sets - List> sets = new ArrayList>(); + // There are up to 10 toplevel set. 8 of 10 are the result of the + // cartesian product of the sets created by pattern matching. + List>> topLevelSets = new ArrayList<>(); - if(eq1s.size() != 0) - sets.add(eq1s); // Add Eq1' + if(eq1s.size() != 0) { + Set> wrap = new HashSet<>(); + wrap.add(eq1s); + topLevelSets.add(wrap); // Add Eq1' + } // Add the set of [a =. Theta | (a=. Theta) in Eq2'] Set bufferSet = eq2s.stream() .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) .collect(Collectors.toSet()); - if(bufferSet.size() != 0) - sets.add(bufferSet); + if(bufferSet.size() != 0) { + Set> wrap = new HashSet<>(); + wrap.add(bufferSet); + topLevelSets.add(wrap); + } // Sets that originate from pair pattern matching // Sets of the "second level" - - sets.addAll(calculatePairSets(eq2s, fc)); + Set>> secondLevelSets = calculatePairSets(eq2s, fc); /* Up to here, no cartesian products are calculated. - * Around here, filters for pairs and sets can be applied */ + * filters for pairs and sets can be applied here */ ISetOperations setOps = new GuavaSetOperations(); - // Calculate the cartesian products - Set> result = setOps.cartesianProduct(sets).stream() - .map(x -> new HashSet(x)).collect(Collectors.toCollection(HashSet::new)); + // Sub cartesian products of the second level (pattern matched) sets + for(Set> secondLevelSet : secondLevelSets) { + List> secondLevelSetList = new ArrayList<>(secondLevelSet); + topLevelSets.add(setOps.cartesianProduct(secondLevelSetList) + .stream().map(x -> new HashSet<>(x)) + .collect(Collectors.toCollection(HashSet::new))); + } + + // Cartesian product over all (up to 10) top level sets + Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) + .stream().map(x -> new HashSet<>(x)) + .collect(Collectors.toCollection(HashSet::new)); //System.out.println(result); /* @@ -91,38 +106,41 @@ 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? + * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht) */ + Set> eqPrimeSetFlat = new HashSet<>(); + for(Set> setToFlatten : eqPrimeSet) { + Set buffer = new HashSet<>(); + setToFlatten.stream().forEach(x -> buffer.addAll(x)); + eqPrimeSetFlat.add(buffer); + } IRuleSet rules = new RuleSet(fc); Set> changed = new HashSet<>(); - Set> unchanged = new HashSet<>(); + Set> eqPrimePrimeSet = new HashSet<>(); - for(Set eqss : result) { - Optional> newEqss = rules.subst(eqss); - if(newEqss.isPresent()) - changed.add(newEqss.get()); - else - unchanged.add(eqss); + for(Set eqPrime : eqPrimeSetFlat) { + Optional> eqPrimePrime = rules.subst(eqPrime); + + if(eqPrimePrime.isPresent()) + changed.add(eqPrimePrime.get()); + else + eqPrimePrimeSet.add(eqPrime); } - /* * Step 6 a) Restart for pairs where subst was applied * b) Build the union over everything */ - for(Set eqss : changed) - unchanged.addAll(this.unify(eqss, fc)); + for(Set eqss : changed) { + eqPrimePrimeSet.addAll(this.unify(eqss, fc)); + } /* - * Step 7: Filter result for solved pairs TODO wie? + * Step 7: Filter result for solved pairs */ - - return unchanged; + return eqPrimePrimeSet; } @@ -217,8 +235,12 @@ public class Unify { } - protected List> calculatePairSets(Set eq2s, IFiniteClosure fc) { - List> result = new ArrayList>(); + protected Set>> calculatePairSets(Set eq2s, IFiniteClosure fc) { + List>> result = new ArrayList<>(); + + // Init all 8 cases + for(int i = 0; i < 8; i++) + result.add(new HashSet<>()); for(MPair pair : eq2s) { @@ -228,38 +250,38 @@ public class Unify { // Case 1: (a <. Theta') if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) - result.add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); + result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); // Case 2: (a <.? ? ext Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) - result.add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); + result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); // Case 3: (a <.? ? sup Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) - result.add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); + result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); // Case 4: (a <.? Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) - result.add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); + result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); // Case 5: (Theta <. a) else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) - result.add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); + result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); // Case 6: (? ext Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) - result.add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); + result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); // Case 7: (? sup Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) - result.add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); + result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); // Case 8: (Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) - result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); + result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); } - return result; + return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); } protected Set unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) { @@ -456,13 +478,4 @@ public class Unify { permuteParams(candidates, idx+1, result, current); } } - - private Set getAllInstantiations(Type t, IFiniteClosure fc) { - Set result = new HashSet<>(); - result.add(t); - return result; - - // TODO - } - } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 5c3ad04e0..ae219dd29 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -36,10 +36,10 @@ public class UnifyTest extends Unify { // 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("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); + 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("Number")), 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("List", "A"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "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));