diff --git a/src/de/dhbwstuttgart/typeinference/unify/Unify.java b/src/de/dhbwstuttgart/typeinference/unify/Unify.java index b9c1d9b1..6d7d978d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/Unify.java @@ -119,22 +119,26 @@ public class Unify { } IRuleSet rules = new RuleSet(fc); - Set> changed = new HashSet<>(); + Set> restartSet = new HashSet<>(); Set> eqPrimePrimeSet = new HashSet<>(); for(Set eqPrime : eqPrimeSetFlat) { Optional> eqPrimePrime = rules.subst(eqPrime); - if(eqPrime.equals(eq)) + /*if (eqPrime.equals(eq)) eqPrimePrimeSet.add(eqPrime); - else if(eqPrimePrime.isPresent()) - eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc)); + else if(eqPrimePrime.isPresent()) { + Set> subUnifyResult = unify(eqPrimePrime.get(), fc); + eqPrimePrimeSet.addAll(subUnifyResult); + } else - eqPrimePrimeSet.addAll(this.unify(eqPrime, fc)); - /*if(eqPrimePrime.isPresent()) - changed.add(eqPrimePrime.get()); + eqPrimePrimeSet.addAll(this.unify(eqPrime, fc));*/ + if(eqPrimePrime.isPresent()) + restartSet.add(eqPrimePrime.get()); + else if(!isSolvedForm(eqPrime)) + restartSet.add(eqPrime); else - eqPrimePrimeSet.add(eqPrime);*/ + eqPrimePrimeSet.add(eqPrime); } /* @@ -142,7 +146,7 @@ public class Unify { * b) Build the union over everything */ - for(Set eqss : changed) + for(Set eqss : restartSet) eqPrimePrimeSet.addAll(this.unify(eqss, fc)); /* @@ -326,16 +330,36 @@ public class Unify { IUnify unify = new MartelliMontanariUnify(); Set cs = fc.getAllTypesByName(thetaPrime.getName()); + cs.add(thetaPrime); for(UnifyType c : cs) { Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); - + thetaQs.add(thetaPrime); + Set thetaQPrimes = new HashSet<>(); TypeParams cParams = c.getTypeParams(); if(cParams.size() == 0) thetaQPrimes.add(c); else { ArrayList> candidateParams = new ArrayList<>(); + + /* + * TODO Optimierungsmöglichkeit: + * + * An dieser Stelle gibt es Raum für Optimierung. + * Z.B. resultiert (a <. C) durch Permutation der Parameter mit grArg in: + * (a = C, b' <.? ? extends Number) + * (a = C, b' <.? ? extends Integer) + * (a = C, b' <.? Integer) + * usw... + * + * Der erste Fall ist am allgemeinsten und schließt alle anderen Fälle mit ein. Jeder Fall resultiert in einem + * rekursiven Aufruf des Unify. Es würde reichen nur den allgemeinsten Fall zu betrachten da dieser den Lösungraum + * der anderen Fälle miteinschließt. + * + * (Gibt es einen einzigen maximalen fall? Wsl. ? super x (x möglichst klein) und ? ext y (y möglichst groß)) + */ + for(UnifyType param : cParams) candidateParams.add(fc.grArg(param)); @@ -354,18 +378,20 @@ public class Unify { for (Entry sigma : unifier.getSubstitutions()) substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); + List freshTphs = new ArrayList<>(); for (UnifyType tq : thetaQs) { Set smaller = fc.smaller(unifier.apply(tq)); for(UnifyType theta : smaller) { Set resultPrime = new HashSet<>(); - UnifyType[] freshTphs = new UnifyType[theta.getTypeParams().size()]; - for(int i = 0; i < freshTphs.length; i++) { - freshTphs[i] = PlaceholderType.freshPlaceholder(); - resultPrime.add(new UnifyPair(freshTphs[i], theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC)); + //UnifyType[] freshTphs = new UnifyType[theta.getTypeParams().size()]; + for(int i = 0; i < theta.getTypeParams().size(); i++) { + if(freshTphs.size()-1 < i) + freshTphs.add(PlaceholderType.freshPlaceholder()); + resultPrime.add(new UnifyPair(freshTphs.get(i), theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC)); } - UnifyType freshTheta = theta.setTypeParams(new TypeParams(freshTphs)); + UnifyType freshTheta = theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))); resultPrime.add(new UnifyPair(a, freshTheta, PairOperator.EQUALSDOT)); resultPrime.addAll(substitutionSet); result.add(resultPrime); @@ -380,53 +406,74 @@ public class Unify { protected Set> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) { Set> result = new HashSet<>(); - IUnify unify = new MartelliMontanariUnify(); + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + UnifyType extAPrime = new ExtendsType(aPrime); UnifyType thetaPrime = extThetaPrime.getExtendedType(); - Set cs = fc.getAllTypesByName(thetaPrime.getName()); - - for(UnifyType c : cs) { - Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); - - Set thetaQPrimes = new HashSet<>(); - TypeParams cParams = c.getTypeParams(); - if(cParams.size() == 0) - thetaQPrimes.add(c); - else { - ArrayList> candidateParams = new ArrayList<>(); - for(UnifyType param : cParams) - candidateParams.add(fc.grArg(param)); + //for(UnifyType theta : fc.smArg(subThetaPrime)) { + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, aPrime, PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT)); + result.add(resultPrime); - for(TypeParams tp : permuteParams(candidateParams)) - thetaQPrimes.add(c.setTypeParams(tp)); - } - - for(UnifyType tqp : thetaQPrimes) { - Optional opt = unify.unify(tqp, thetaPrime); - if (!opt.isPresent()) - continue; - - Unifier unifier = opt.get(); - - Set substitutionSet = new HashSet<>(); - for (Entry sigma : unifier.getSubstitutions()) - substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); - - for (UnifyType tq : thetaQs) { - ExtendsType extTq = new ExtendsType(tq); - Set smArg = fc.smArg(unifier.apply(extTq)); - for(UnifyType theta : smArg) { - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT)); - resultPrime.addAll(substitutionSet); - result.add(resultPrime); - } - } - - } - } + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT)); + result.add(resultPrime); + //} return result; + +// Set> result = new HashSet<>(); +// IUnify unify = new MartelliMontanariUnify(); +// +// UnifyType thetaPrime = extThetaPrime.getExtendedType(); +// Set cs = fc.getAllTypesByName(thetaPrime.getName()); +// cs.add(thetaPrime); +// +// for(UnifyType c : cs) { +// Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); +// thetaQs.add(thetaPrime); +// +// Set thetaQPrimes = new HashSet<>(); +// TypeParams cParams = c.getTypeParams(); +// if(cParams.size() == 0) +// thetaQPrimes.add(c); +// else { +// ArrayList> candidateParams = new ArrayList<>(); +// for(UnifyType param : cParams) +// candidateParams.add(fc.grArg(param)); +// +// for(TypeParams tp : permuteParams(candidateParams)) +// thetaQPrimes.add(c.setTypeParams(tp)); +// } +// +// for(UnifyType tqp : thetaQPrimes) { +// Optional opt = unify.unify(tqp, thetaPrime); +// if (!opt.isPresent()) +// continue; +// +// Unifier unifier = opt.get(); +// +// Set substitutionSet = new HashSet<>(); +// for (Entry sigma : unifier.getSubstitutions()) +// substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); +// +// for (UnifyType tq : thetaQs) { +// ExtendsType extTq = new ExtendsType(tq); +// Set smArg = fc.smArg(unifier.apply(extTq)); +// for(UnifyType theta : smArg) { +// Set resultPrime = new HashSet<>(); +// resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT)); +// resultPrime.addAll(substitutionSet); +// result.add(resultPrime); +// } +// } +// +// } +// } +// +// return result; } protected Set> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) { @@ -494,62 +541,89 @@ public class Unify { protected Set> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); - IUnify unify = new MartelliMontanariUnify(); + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + UnifyType supAPrime = new SuperType(aPrime); UnifyType theta = supTheta.getSuperedType(); - Set cs = fc.getAllTypesByName(theta.getName()); - - for(UnifyType c : cs) { - Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); - - Set thetaQPrimes = new HashSet<>(); - TypeParams cParams = c.getTypeParams(); - if(cParams.size() == 0) - thetaQPrimes.add(c); - else { - ArrayList> candidateParams = new ArrayList<>(); - for(UnifyType param : cParams) - candidateParams.add(fc.grArg(param)); - - for(TypeParams tp : permuteParams(candidateParams)) - thetaQPrimes.add(c.setTypeParams(tp)); - } - - for(UnifyType tqp : thetaQPrimes) { - Optional opt = unify.unify(tqp, theta); - if (!opt.isPresent()) - continue; - - Unifier unifier = opt.get(); - - Set substitutionSet = new HashSet<>(); - for (Entry sigma : unifier.getSubstitutions()) - substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); - - for (UnifyType tq : thetaQs) { - Set smaller = fc.smaller(unifier.apply(tq)); - - for(UnifyType thetaPrime : smaller) { - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, new SuperType(thetaPrime), PairOperator.EQUALSDOT)); - resultPrime.addAll(substitutionSet); - result.add(resultPrime); - } - } - - } - } + //for(UnifyType theta : fc.smArg(subThetaPrime)) { + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(aPrime, theta, PairOperator.SMALLERDOT)); + result.add(resultPrime); + //} return result; + +// Set> result = new HashSet<>(); +// IUnify unify = new MartelliMontanariUnify(); +// +// UnifyType theta = supTheta.getSuperedType(); +// Set cs = fc.getAllTypesByName(theta.getName()); +// cs.add(theta); +// +// for(UnifyType c : cs) { +// Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); +// thetaQs.add(theta); +// +// Set thetaQPrimes = new HashSet<>(); +// TypeParams cParams = c.getTypeParams(); +// if(cParams.size() == 0) +// thetaQPrimes.add(c); +// else { +// ArrayList> candidateParams = new ArrayList<>(); +// for(UnifyType param : cParams) +// candidateParams.add(fc.grArg(param)); +// +// for(TypeParams tp : permuteParams(candidateParams)) +// thetaQPrimes.add(c.setTypeParams(tp)); +// } +// +// for(UnifyType tqp : thetaQPrimes) { +// Optional opt = unify.unify(tqp, theta); +// if (!opt.isPresent()) +// continue; +// +// Unifier unifier = opt.get(); +// +// Set substitutionSet = new HashSet<>(); +// for (Entry sigma : unifier.getSubstitutions()) +// substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); +// +// for (UnifyType tq : thetaQs) { +// Set smaller = fc.smaller(unifier.apply(tq)); +// +// for(UnifyType thetaPrime : smaller) { +// Set resultPrime = new HashSet<>(); +// resultPrime.add(new UnifyPair(a, new SuperType(thetaPrime), PairOperator.EQUALSDOT)); +// resultPrime.addAll(substitutionSet); +// result.add(resultPrime); +// } +// } +// +// } +// } +// +// return result; } protected Set> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); - for(UnifyType thetaS : fc.grArg(theta)) { - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT)); - result.add(resultPrime); - } + //for(UnifyType thetaS : fc.grArg(theta)) { + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT)); + result.add(resultPrime); + + UnifyType freshTph = PlaceholderType.freshPlaceholder(); + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT)); + result.add(resultPrime); + + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT)); + result.add(resultPrime); + //} return result; } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java index f45a4a13..879fe87d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java @@ -31,7 +31,7 @@ public final class PlaceholderType extends UnifyType{ String name = nextName + randomChar(); while(EXISTING_PLACEHOLDERS.contains(name)); - nextName += randomChar(); + name += randomChar(); return new PlaceholderType(name, true); } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 6f0597fd..666731b8 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -157,6 +157,7 @@ public class UnifyTest extends Unify { addAsSet(expected, new UnifyPair(tphA, supNumber, PairOperator.EQUALSDOT)); actual = unify(eq, fc); + actual = filterGeneratedTPHsMultiple(actual); Assert.assertEquals(expected, actual); @@ -199,6 +200,7 @@ public class UnifyTest extends Unify { addAsSet(expected, new UnifyPair(tphA, number, PairOperator.EQUALSDOT)); actual = unify(eq, fc); + actual = filterGeneratedTPHsMultiple(actual); Assert.assertEquals(expected, actual); @@ -309,7 +311,7 @@ public class UnifyTest extends Unify { Set> expected = new HashSet<>(); Set> actual = unify(eq, fc); - System.out.println(actual); + //System.out.println(actual); //Assert.assertEquals(actual, expected); @@ -343,8 +345,8 @@ public class UnifyTest extends Unify { expected = new HashSet<>(); actual = unify(eq, fc); - - //System.out.println(actual); + + System.out.println(actual); //Assert.assertEquals(actual, expected); /* @@ -384,8 +386,10 @@ public class UnifyTest extends Unify { UnifyType object = tf.getSimpleType("Object"); UnifyType integer = tf.getSimpleType("Integer"); UnifyType doubl = tf.getSimpleType("Double"); + UnifyType mygeneric = tf.getSimpleType("MyGeneric", "T"); - //fcb.add(number, object); + + fcb.add(mygeneric, object); fcb.add(integer, number); //fcb.add(doubl, number); @@ -433,9 +437,21 @@ public class UnifyTest extends Unify { * * This is a test for th extension of case 2 of the cartesian product of step 4. * - * TODO + * (a <.? ? ext b) + * (b =. Number) */ + eq = new HashSet<>(); + eq.add(new UnifyPair(tphA, extB, PairOperator.SMALLERDOTWC)); + eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + System.out.println("Case 2"); + System.out.println(actual); + /* * Test 3: * This is a test for the extension of case 3 of the cartesian product of step 4. @@ -453,6 +469,8 @@ public class UnifyTest extends Unify { actual = unify(eq, fc); + + System.out.println("Case 3"); System.out.println(actual); //Assert.assertEquals(expected, actual); @@ -498,6 +516,47 @@ public class UnifyTest extends Unify { System.out.println(actual); //Assert.assertEquals(expected, actual); + /* + * Test 7: + * This is a test for the extension of case 7 of the cartesian product of step 4. + * + * ? sup b <.? a + * b =. Number + */ + + eq = new HashSet<>(); + eq.add(new UnifyPair(supB, tphA, PairOperator.SMALLERDOTWC)); + eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + System.out.println("Case 7"); + System.out.println(actual); + //Assert.assertEquals(expected, actual); + + + /* + * Test 8: + * This is a test for the extension of case 8 of the cartesian product of step 4. + * + * MyGeneric <.? a + * b =. Integer + */ + + eq = new HashSet<>(); + eq.add(new UnifyPair(tf.getSimpleType("MyGeneric", extB), tphA, PairOperator.SMALLERDOTWC)); + eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + System.out.println("Case 8:"); + System.out.println(actual); + //Assert.assertEquals(expected, actual); + } @Test