diff --git a/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java b/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java index ba456841..b51fb648 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java +++ b/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java @@ -7,10 +7,16 @@ import com.google.common.collect.Sets; import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; +/** + * Implements set operations using google guava. + * @author DH10STF + * + */ public class GuavaSetOperations implements ISetOperations { @Override public Set> cartesianProduct(List> sets) { + // Wraps the call to google guava return Sets.cartesianProduct(sets); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java index 3531b716..ae017235 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java @@ -1,21 +1,19 @@ package de.dhbwstuttgart.typeinference.unify; -import java.util.AbstractMap; import java.util.ArrayList; import java.util.HashSet; import java.util.Iterator; -import java.util.Map.Entry; import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; -import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; import de.dhbwstuttgart.typeinference.unify.model.PairOperator; import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typeinference.unify.model.UnifyType; 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 the Martelli-Montanari unification algorithm. @@ -25,60 +23,77 @@ public class MartelliMontanariUnify implements IUnify { @Override public Optional unify(Set terms) { + // Sets with less than 2 terms are trivially unified if(terms.size() < 2) return Optional.of(Unifier.Identity()); - ArrayList termsQ = new ArrayList(); + // For the the set of terms {t1,...,tn}, + // build a list of equations {(t1 = t2), (t2 = t3), (t3 = t4), ....} + ArrayList termsList = new ArrayList(); Iterator iter = terms.iterator(); UnifyType prev = iter.next(); while(iter.hasNext()) { UnifyType next = iter.next(); - termsQ.add(new UnifyPair(prev, next, PairOperator.EQUALSDOT)); + termsList.add(new UnifyPair(prev, next, PairOperator.EQUALSDOT)); prev = next; } + // Start with the identity unifier. Substitutions will be added later. Unifier mgu = Unifier.Identity(); + // Apply rules while possible int idx = 0; - while(idx < termsQ.size()) { - UnifyPair pair = termsQ.get(idx); + 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(); - if(delete(pair)) { - termsQ.remove(idx); + // DELETE - Rule + if(pair.getRhsType().equals(pair.getLhsType())) { + termsList.remove(idx); + continue; + } + + // REDUCE - Rule + if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType) + && (rhsTypeParams.size() != 0 || lhsTypeParams.size() != 0)) { + Set result = new HashSet<>(); + + // f<...> = g<...> with f != g are not unifiable + if(!rhsType.getName().equals(lhsType.getName())) + return Optional.empty(); // conflict + // f = f are not unifiable + if(rhsTypeParams.size() != lhsTypeParams.size()) + return Optional.empty(); // conflict + + // Unpack the arguments + for(int i = 0; i < rhsTypeParams.size(); i++) + result.add(new UnifyPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT)); + + termsList.remove(idx); + termsList.addAll(result); + continue; + } + + // SWAP - Rule + if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) { + termsList.remove(idx); + termsList.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT)); continue; } - Optional> optSet = decompose(pair); - - if(optSet == null) - return Optional.empty(); // Unification failed - - if(optSet.isPresent()) { - termsQ.addAll(optSet.get()); - idx = idx+1 == termsQ.size() ? 0 : idx+1; - continue; - } - - Optional optPair = swap(pair); - - if(optPair.isPresent()) { - termsQ.add(optPair.get()); - idx = idx+1 == termsQ.size() ? 0 : idx+1; - continue; - } - - // Occurs-Check + // OCCURS-CHECK if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType())) return Optional.empty(); - Optional> optUni = eliminate(pair); - - if(optUni.isPresent()) { - Entry substitution = optUni.get(); - mgu.Add(substitution.getKey(), substitution.getValue()); - termsQ = termsQ.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new)); - idx = idx+1 == termsQ.size() ? 0 : idx+1; + // SUBST - Rule + if(lhsType instanceof PlaceholderType) { + mgu.Add((PlaceholderType) lhsType, rhsType); + termsList = termsList.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new)); + idx = idx+1 == termsList.size() ? 0 : idx+1; continue; } @@ -87,55 +102,4 @@ public class MartelliMontanariUnify implements IUnify { return Optional.of(mgu); } - - private boolean delete(UnifyPair pair) { - return pair.getRhsType().equals(pair.getLhsType()); - } - - private Optional> decompose(UnifyPair pair) { - Set result = new HashSet<>(); - - UnifyType rhs = pair.getRhsType(); - UnifyType lhs = pair.getLhsType(); - - TypeParams rhsTypeParams = rhs.getTypeParams(); - TypeParams lhsTypeParams = lhs.getTypeParams(); - - if(!(rhs instanceof PlaceholderType) && !(lhs instanceof PlaceholderType)) { - if(!rhs.getName().equals(lhs.getName())) - return null; // conflict - if(rhsTypeParams.size() != lhsTypeParams.size()) - return null; // conflict; - } - - if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0) - return Optional.empty(); - - for(int i = 0; i < rhsTypeParams.size(); i++) - result.add(new UnifyPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT)); - - return Optional.of(result); - } - - private Optional swap(UnifyPair pair) { - UnifyType rhs = pair.getRhsType(); - UnifyType lhs = pair.getLhsType(); - - if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType)) - return Optional.of(new UnifyPair(rhs, lhs, PairOperator.EQUALSDOT)); - - return Optional.empty(); - } - - private Optional> eliminate(UnifyPair pair) { - UnifyType rhs = pair.getRhsType(); - UnifyType lhs = pair.getLhsType(); - - // TODO only apply when lhs is element of vars(termsQ)? - - if(!(lhs instanceof PlaceholderType)) - return Optional.empty(); - - return Optional.of(new AbstractMap.SimpleImmutableEntry((PlaceholderType) lhs, rhs)); - } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java index e18e6156..82ee9683 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java @@ -25,16 +25,26 @@ import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import de.dhbwstuttgart.typeinference.unify.model.Unifier; import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +/** + * Implementation of the type inference rules. + * @author Florian Steurer + * + */ public class RuleSet implements IRuleSet{ - + protected IFiniteClosure finiteClosure; + /** + * Creates a new instance that uses the specified FC for greater, grArg, etc. + * @param fc The FC that is used for greater, grArg, etc. + */ public RuleSet(IFiniteClosure fc) { finiteClosure = fc; } @Override public Optional reduceUp(UnifyPair pair) { + // Check if reduce up is applicable if(pair.getPairOp() != PairOperator.SMALLERDOT) return Optional.empty(); @@ -46,11 +56,13 @@ public class RuleSet implements IRuleSet{ if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType)) return Optional.empty(); + // Rule is applicable, unpack the SuperType return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT)); } @Override public Optional reduceLow(UnifyPair pair) { + // Check if rule is applicable if(pair.getPairOp() != PairOperator.SMALLERDOT) return Optional.empty(); @@ -62,11 +74,13 @@ public class RuleSet implements IRuleSet{ if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType)) return Optional.empty(); + // Rule is applicable, unpack the ExtendsType return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT)); } @Override public Optional reduceUpLow(UnifyPair pair) { + // Check if rule is applicable if(pair.getPairOp() != PairOperator.SMALLERDOT) return Optional.empty(); @@ -78,6 +92,7 @@ public class RuleSet implements IRuleSet{ if(!(rhsType instanceof SuperType)) return Optional.empty(); + // Rule is applicable, unpack both sides return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT)); } @@ -104,7 +119,7 @@ public class RuleSet implements IRuleSet{ if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size()) return Optional.empty(); - UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX).orElse(null); + UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); @@ -156,7 +171,7 @@ public class RuleSet implements IRuleSet{ if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size()) return Optional.empty(); - UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX).orElse(null); + UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); @@ -234,7 +249,7 @@ public class RuleSet implements IRuleSet{ if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size()) return Optional.empty(); - UnifyType cFromFc = finiteClosure.getLeftHandedType(c).orElse(null); + UnifyType cFromFc = finiteClosure.getLeftHandedType(c.getName()).orElse(null); if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); @@ -383,7 +398,7 @@ public class RuleSet implements IRuleSet{ return Optional.empty(); - Optional opt = finiteClosure.getLeftHandedType(typeD); + Optional opt = finiteClosure.getLeftHandedType(typeD.getName()); if(!opt.isPresent()) return Optional.empty(); @@ -427,9 +442,9 @@ public class RuleSet implements IRuleSet{ UnifyType typeDgen; if(typeD instanceof ReferenceType) - typeDgen = finiteClosure.getLeftHandedType(typeD).orElse(null); + typeDgen = finiteClosure.getLeftHandedType(typeD.getName()).orElse(null); else { - Optional opt = finiteClosure.getLeftHandedType(((ExtendsType) typeD).getExtendedType()); + Optional opt = finiteClosure.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName()); typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null; } @@ -472,7 +487,7 @@ public class RuleSet implements IRuleSet{ return Optional.empty(); - Optional opt = finiteClosure.getLeftHandedType(((SuperType) typeSupD).getSuperedType()); + Optional opt = finiteClosure.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName()); if(!opt.isPresent()) return Optional.empty(); diff --git a/src/de/dhbwstuttgart/typeinference/unify/Unify.java b/src/de/dhbwstuttgart/typeinference/unify/Unify.java index 6f4fa514..0d2014b9 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/Unify.java @@ -32,6 +32,8 @@ import de.dhbwstuttgart.typeinference.unify.model.Unifier; */ public class Unify { + protected ISetOperations setOps = new GuavaSetOperations(); + public Set> unify(Set eq, IFiniteClosure fc) { /* * Step 1: Repeated application of reduce, adapt, erase, swap @@ -89,8 +91,6 @@ public class Unify { /* Up to here, no cartesian products are calculated. * filters for pairs and sets can be applied here */ - ISetOperations setOps = new GuavaSetOperations(); - // Sub cartesian products of the second level (pattern matched) sets for(Set>> secondLevelSet : secondLevelSets) { List>> secondLevelSetList = new ArrayList<>(secondLevelSet); @@ -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,12 +330,11 @@ public class Unify { IUnify unify = new MartelliMontanariUnify(); Set cs = fc.getAllTypesByName(thetaPrime.getName()); + cs.add(thetaPrime); - for(UnifyType c : cs) { - - // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? - Set thetaQs = fc.getChildren(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); - thetaQs.add(c); // reflexive + 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(); @@ -339,6 +342,26 @@ public class Unify { 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 und smaller 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. + * + * Prüfen: + * Gibt es einen einzigen maximalen Fall? + * Wahrscheinlich gibt es 2: ? super x (x möglichst klein) und ? ext y (y möglichst groß)) + */ + for(UnifyType param : cParams) candidateParams.add(fc.grArg(param)); @@ -352,15 +375,26 @@ public class Unify { continue; Unifier unifier = opt.get(); + unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams().toArray()); Set substitutionSet = new HashSet<>(); 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<>(); - resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT)); + + //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.toArray(new UnifyType[0]))); + resultPrime.add(new UnifyPair(a, freshTheta, PairOperator.EQUALSDOT)); resultPrime.addAll(substitutionSet); result.add(resultPrime); } @@ -374,56 +408,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) { + //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); - // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? - Set thetaQs = fc.getChildren(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); - thetaQs.add(c); // reflexive - - 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); - } - } - - } - } + 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) { @@ -460,7 +512,14 @@ public class Unify { Set> result = new HashSet<>(); for(UnifyType thetaS : fc.greater(theta)) { Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT)); + + UnifyType[] freshTphs = new UnifyType[thetaS.getTypeParams().size()]; + for(int i = 0; i < freshTphs.length; i++) { + freshTphs[i] = PlaceholderType.freshPlaceholder(); + resultPrime.add(new UnifyPair(thetaS.getTypeParams().get(i), freshTphs[i], PairOperator.SMALLERDOTWC)); + } + + resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT)); result.add(resultPrime); } @@ -469,76 +528,104 @@ public class Unify { protected Set> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); - for(UnifyType thetaS : fc.grArg(extTheta)) { - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT)); - result.add(resultPrime); - } + //for(UnifyType thetaS : fc.smaller(extTheta.getExtendedType())) { + UnifyType freshTph = PlaceholderType.freshPlaceholder(); + UnifyType extFreshTph = new ExtendsType(freshTph); + + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, extFreshTph, PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(extTheta.getExtendedType(), freshTph, PairOperator.SMALLERDOT)); + result.add(resultPrime); + //} return result; } 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) { - - // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? - Set thetaQs = fc.getChildren(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); - thetaQs.add(c); // reflexive - - 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/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index bd15999a..dcb6c4d1 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -10,6 +10,10 @@ import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; import de.dhbwstuttgart.typeinference.unify.model.SuperType; import de.dhbwstuttgart.typeinference.unify.model.UnifyType; +/** + * + * @author Florian Steurer + */ public interface IFiniteClosure { /** @@ -53,7 +57,7 @@ public interface IFiniteClosure { public Set grArg(FunNType type); public Set smArg(FunNType type); - public Optional getLeftHandedType(UnifyType t); + public Optional getLeftHandedType(String typeName); public Set getAncestors(UnifyType t); public Set getChildren(UnifyType t); public Set getAllTypesByName(String typeName); diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java index 11c98481..26ea0dce 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java @@ -5,6 +5,10 @@ import java.util.Set; import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; +/** + * Contains the inference rules that are applied to the set Eq. + * @author Florian Steurer + */ public interface IRuleSet { public Optional reduceUp(UnifyPair pair); @@ -17,7 +21,7 @@ public interface IRuleSet { public Optional> reduce2(UnifyPair pair); /* - * Missing Rules + * Missing Reduce-Rules for Wildcards */ public Optional reduceWildcardLow(UnifyPair pair); public Optional reduceWildcardLowRight(UnifyPair pair); @@ -34,8 +38,22 @@ public interface IRuleSet { public Optional> greaterFunN(UnifyPair pair); public Optional> smallerFunN(UnifyPair pair); + /** + * Checks whether the erase1-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ public boolean erase1(UnifyPair pair); + + /** + * Checks whether the erase2-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ public boolean erase2(UnifyPair pair); + + /** + * Checks whether the erase3-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ public boolean erase3(UnifyPair pair); public Optional swap(UnifyPair pair); @@ -44,5 +62,10 @@ public interface IRuleSet { public Optional adaptExt(UnifyPair pair); public Optional adaptSup(UnifyPair pair); - public Optional> subst(Set pair); + /** + * Applies the subst-Rule to a set of pairs (usually Eq'). + * @param pairs The set of pairs where the subst rule should apply. + * @return An optional of the modified set, if there were any substitutions. An empty optional if there were no substitutions. + */ + public Optional> subst(Set pairs); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java index caed79e4..4a98aaba 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java @@ -3,6 +3,14 @@ package de.dhbwstuttgart.typeinference.unify.interfaces; import java.util.List; import java.util.Set; +/** + * Contains operations on sets. + * @author Florian Steurer + */ public interface ISetOperations { + /** + * Calculates the cartesian product of the sets. + * @return The cartesian product + */ Set> cartesianProduct(List> sets); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index ef8775b1..524608f5 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -14,8 +14,20 @@ import de.dhbwstuttgart.typeinference.unify.model.Unifier; */ public interface IUnify { + /** + * 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 unify(Set terms); + /** + * 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. + */ default public Optional unify(UnifyType... terms) { return unify(Arrays.stream(terms).collect(Collectors.toSet())); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java index 847abfd5..9416d786 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java @@ -14,7 +14,7 @@ public final class ExtendsType extends WildcardType { * @param extendedType The extended type e.g. Integer in "? extends Integer" */ public ExtendsType(UnifyType extendedType) { - super("? extends " + extendedType.getName(), extendedType, extendedType.getTypeParams()); + super("? extends " + extendedType.getName(), extendedType); } public UnifyType getExtendedType() { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index d5aaaf72..aae6d7e6 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -18,7 +18,7 @@ public class FiniteClosure implements IFiniteClosure { private HashMap> inheritanceGraph; private HashMap>> strInheritanceGraph; private Set pairs; - private Set basicTypes; + //private Set basicTypes; //TODO im konstruktor mitgeben um typenabzuhandeln die keine extends beziehung haben. (Damit die FC diese Typen auch kennt) //(ALternative: immer die extends zu object beziehung einfügen) @@ -65,6 +65,13 @@ public class FiniteClosure implements IFiniteClosure { */ @Override public Set smaller(UnifyType type) { + if(type instanceof FunNType) + return computeSmallerFunN((FunNType) type); + + return computeSmaller(type); + } + + private Set computeSmaller(UnifyType type) { if(inheritanceGraph.containsKey(type)) { Set result = new HashSet<>(); result.add(type); @@ -82,8 +89,7 @@ public class FiniteClosure implements IFiniteClosure { for (UnifyType param : type.getTypeParams()) paramCandidates.add(smArg(param)); - Set permResult = new HashSet<>(); - permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]); + Set permResult = permuteParams(paramCandidates); for (TypeParams newParams : permResult) result1.add(type.setTypeParams(newParams));} @@ -94,16 +100,18 @@ public class FiniteClosure implements IFiniteClosure { strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent())); for(UnifyType typePrime : result1) { - for (UnifyType theta2 : candidates) { - Optional sigma2 = unify.unify(typePrime, theta2); - if (!sigma2.isPresent()) + for (UnifyType theta2 : candidates) { + Optional sigma2Opt = unify.unify(typePrime, theta2); + if (!sigma2Opt.isPresent()) continue; + Unifier sigma2 = sigma2Opt.get(); + sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams().toArray()); if(type.equals(theta2)) continue; Set theta1s = smaller(theta2); for (UnifyType theta1 : theta1s) { // Because only the most general type is calculated, sigma1 = sigma2 - UnifyType sigma1Theta1 = sigma2.get().apply(theta1); + UnifyType sigma1Theta1 = sigma2.apply(theta1); result2.add(sigma1Theta1); } } @@ -118,8 +126,7 @@ public class FiniteClosure implements IFiniteClosure { for (UnifyType param : t.getTypeParams()) paramCandidates.add(smArg(param)); - Set permResult = new HashSet<>(); - permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]); + Set permResult = permuteParams(paramCandidates); for (TypeParams newParams : permResult) { UnifyType tPrime = t.setTypeParams(newParams); @@ -127,19 +134,44 @@ public class FiniteClosure implements IFiniteClosure { result3.add(t); else result3.addAll(smaller(tPrime)); - } + } } return result3; } + + private Set computeSmallerFunN(FunNType type) { + Set result = new HashSet<>(); + + // if T = T' then T <=* T' + result.add(type); + + ArrayList> paramCandidates = new ArrayList<>(); + paramCandidates.add(smaller(type.getTypeParams().get(0))); + for (int i = 1; i < type.getTypeParams().size(); i++) + paramCandidates.add(greater(type.getTypeParams().get(i))); + + Set permResult = permuteParams(paramCandidates); + + for (TypeParams newParams : permResult) + result.add(type.setTypeParams(newParams)); + + return result; + } /** * Returns all types of the finite closure that are supertypes of the argument. * @return The set of supertypes of the argument. */ @Override - public Set greater(UnifyType type) { + public Set greater(UnifyType type) { + if(type instanceof FunNType) + return computeGreaterFunN((FunNType) type); + return computeGreater(type); + } + + protected Set computeGreater(UnifyType type) { IUnify unify = new MartelliMontanariUnify(); Set result1 = new HashSet<>(); @@ -166,22 +198,25 @@ public class FiniteClosure implements IFiniteClosure { for(UnifyType typePrime : result1) { for (UnifyType theta2 : candidates) { - Optional sigma2 = unify.unify(typePrime, theta2); - if (!sigma2.isPresent()) + Optional sigma2Opt = unify.unify(typePrime, theta2); + if (!sigma2Opt.isPresent()) continue; if(type.equals(theta2)) continue; + + Unifier sigma2 = sigma2Opt.get(); + sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams().toArray()); Set theta1s = greater(theta2); for (UnifyType theta1 : theta1s) { // Because only the most general type is calculated, sigma1 = sigma2 - UnifyType sigma1Theta1 = sigma2.get().apply(theta1); + UnifyType sigma1Theta1 = sigma2.apply(theta1); result2.add(sigma1Theta1); } } } } - result2.addAll(result1); + result2.addAll(result1); Set result3 = new HashSet<>(); for(UnifyType t : result2) { @@ -203,8 +238,27 @@ public class FiniteClosure implements IFiniteClosure { } return result3; - } + + protected Set computeGreaterFunN(FunNType type) { + Set result = new HashSet<>(); + + // if T = T' then T <=* T' + result.add(type); + + ArrayList> paramCandidates = new ArrayList<>(); + paramCandidates.add(greater(type.getTypeParams().get(0))); + for (int i = 1; i < type.getTypeParams().size(); i++) + paramCandidates.add(smaller(type.getTypeParams().get(i))); + + Set permResult = permuteParams(paramCandidates); + + for (TypeParams newParams : permResult) + result.add(type.setTypeParams(newParams)); + + return result; + } + @Override public Set grArg(UnifyType type) { @@ -341,12 +395,12 @@ public class FiniteClosure implements IFiniteClosure { } @Override - public Optional getLeftHandedType(UnifyType t) { - if(!strInheritanceGraph.containsKey(t.getName())) + public Optional getLeftHandedType(String typeName) { + if(!strInheritanceGraph.containsKey(typeName)) return Optional.empty(); for(UnifyPair pair : pairs) - if(pair.getLhsType().getName().equals(t.getName())) + if(pair.getLhsType().getName().equals(typeName)) return Optional.of(pair.getLhsType()); return Optional.empty(); @@ -370,6 +424,12 @@ public class FiniteClosure implements IFiniteClosure { return result; } + protected Set permuteParams(ArrayList> candidates) { + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new UnifyType[candidates.size()]); + return result; + } + protected void permuteParams(ArrayList> candidates, int idx, Set result, UnifyType[] current) { if(candidates.size() == idx) { result.add(new TypeParams(Arrays.copyOf(current, current.length))); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java index cb431cf9..3363be75 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java @@ -43,13 +43,26 @@ public class FunNType extends UnifyType { Set grArg(IFiniteClosure fc) { return fc.grArg(this); } - + @Override UnifyType apply(Unifier unif) { // TODO Auto-generated method stub return null; } - // TODO equals und hashcode + @Override + public int hashCode() { + return 31 + typeParams.hashCode(); + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof FunNType)) + return false; + + FunNType other = (FunNType) obj; + + return other.getTypeParams().equals(typeParams); + } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java index f45a4a13..ddb7d273 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java @@ -16,13 +16,13 @@ public final class PlaceholderType extends UnifyType{ private final boolean IsGenerated; public PlaceholderType(String name) { - super(name); + super(name, new TypeParams()); EXISTING_PLACEHOLDERS.add(name); IsGenerated = false; } protected PlaceholderType(String name, boolean isGenerated) { - super(name); + super(name, new TypeParams()); EXISTING_PLACEHOLDERS.add(name); IsGenerated = isGenerated; } @@ -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/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java index fd5a0ec1..4f557b53 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java @@ -22,7 +22,7 @@ public final class ReferenceType extends UnifyType { Set grArg(IFiniteClosure fc) { return fc.grArg(this); } - + @Override UnifyType apply(Unifier unif) { return new ReferenceType(typeName, typeParams.apply(unif)); @@ -35,7 +35,7 @@ public final class ReferenceType extends UnifyType { @Override public int hashCode() { - return typeName.hashCode(); + return 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); } @Override diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java index 51f640c9..7c557ade 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -5,10 +5,8 @@ import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; public final class SuperType extends WildcardType { - - public SuperType(UnifyType superedType) { - super("? super " + superedType.getName(), superedType, superedType.getTypeParams()); + super("? super " + superedType.getName(), superedType); } public UnifyType getSuperedType() { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index 0f39a621..f5b7686b 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -77,6 +77,9 @@ public final class TypeParams implements Iterable{ return new TypeParams(newparams); } + public UnifyType[] toArray() { + return Arrays.copyOf(typeParams, typeParams.length); + } @Override public Iterator iterator() { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java index 33f9daec..f5af52d0 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -17,7 +17,7 @@ public class Unifier implements Function /*, Set*/ /** * Identity function as an "unifier". */ - public Unifier() { + protected Unifier() { } @@ -52,6 +52,18 @@ public class Unifier implements Function /*, Set*/ public Set> getSubstitutions() { return substitutions.entrySet(); } + + public void swapPlaceholderSubstitutions(UnifyType... targetParams) { + for(UnifyType tph : targetParams) { + if(!(tph instanceof PlaceholderType)) + continue; + if(substitutions.containsKey(tph) && substitutions.get(tph) instanceof PlaceholderType) { + PlaceholderType newLhs = (PlaceholderType) substitutions.get(tph); + substitutions.remove(tph); + substitutions.put(newLhs, tph); + } + } + } @Override public String toString() { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java index cdc7b818..ed2c95ef 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java @@ -1,31 +1,55 @@ package de.dhbwstuttgart.typeinference.unify.model; +/** + * A pair which contains two types and an operator, e.q. (Integer <. a). + * @author Florian Steurer + */ public class UnifyPair { + /** + * The type on the left hand side of the pair. + */ private UnifyType lhs; + + /** + * The type on the right hand side of the pair. + */ private UnifyType rhs; + + /** + * The operator that determines the relation between the left and right hand side type. + */ private PairOperator pairOp; - /*public MPair(Type t1, Type t2) { - lhs = t1; - rhs = t2; - pairOp = PairOperator.SMALLER; - }*/ - - public UnifyPair(UnifyType t1, UnifyType t2, PairOperator op) { - lhs = t1; - rhs = t2; + /** + * Creates a new instance of the pair. + * @param lhs The type on the left hand side of the pair. + * @param rhs The type on the right hand side of the pair. + * @param op The operator that determines the relation between the left and right hand side type. + */ + public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op) { + this.lhs = lhs; + this.rhs = rhs; pairOp = op; } + /** + * Returns the type on the left hand side of the pair. + */ public UnifyType getLhsType() { return lhs; } + /** + * Returns the type on the right hand side of the pair. + */ public UnifyType getRhsType() { return rhs; } + /** + * Returns the operator that determines the relation between the left and right hand side type. + */ public PairOperator getPairOp() { return pairOp; } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java index 341eabd1..4f1965eb 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java @@ -4,35 +4,76 @@ import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +/** + * Represents a java type. + * @author Florian Steurer + */ public abstract class UnifyType { + /** + * The name of the type e.q. "Integer", "? extends Integer" or "List" for (List) + */ protected final String typeName; + + /** + * The type parameters of the type. + */ protected final TypeParams typeParams; - protected UnifyType(String name, UnifyType... typeParams) { - typeName = name; - this.typeParams = new TypeParams(typeParams); - } - + /** + * Creates a new instance + * @param name Name of the type (e.q. List for List, Integer or ? extends Integer) + * @param typeParams Parameters of the type (e.q. for List) + */ protected UnifyType(String name, TypeParams p) { typeName = name; typeParams = p; } + /** + * Returns the name of the type. + * @return The name e.q. List for List, Integer or ? extends Integer + */ public String getName() { return typeName; } + /** + * The parameters of the type. + * @return Parameters of the type, e.q. for List. + */ public TypeParams getTypeParams() { return typeParams; } + /** + * Returns a new type that equals this type except for the type parameters. + * @param newTp The type params of the new type. + * @return A new type object. + */ public abstract UnifyType setTypeParams(TypeParams newTp); + /** + * Implementation of the visitor-pattern. Returns the set of smArg + * by calling the most specific overload in the FC. + * @param fc The FC that is called. + * @return The set that is smArg(this) + */ abstract Set smArg(IFiniteClosure fc); + /** + * Implementation of the visitor-pattern. Returns the set of grArg + * by calling the most specific overload in the FC. + * @param fc The FC that is called. + * @return The set that is grArg(this) + */ abstract Set grArg(IFiniteClosure fc); + /** + * Applies a unifier to this object. + * @param unif The unifier + * @return A UnifyType, that may or may not be a new object, that has its subtypes substituted. + */ abstract UnifyType apply(Unifier unif); @Override diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java b/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java index 08c49783..9db59498 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java @@ -1,19 +1,30 @@ package de.dhbwstuttgart.typeinference.unify.model; +/** + * A wildcard type that is either a ExtendsType or a SuperType. + * @author Florian Steurer + */ public abstract class WildcardType extends UnifyType { + /** + * The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself. + */ protected UnifyType wildcardedType; - protected WildcardType(String name, UnifyType wildcardedType, UnifyType[] typeParams) { - super(name, typeParams); - this.wildcardedType = wildcardedType; - } - - protected WildcardType(String name, UnifyType wildcardedType, TypeParams p) { - super(name, p); + /** + * Creates a new instance. + * @param name The name of the type, e.q. ? extends Integer + * @param wildcardedType The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself. + */ + protected WildcardType(String name, UnifyType wildcardedType) { + super(name, wildcardedType.getTypeParams()); this.wildcardedType = wildcardedType; } + /** + * Returns the wildcarded type, e.q. Integer for ? extends Integer. + * @return The wildcarded type. Never a wildcard type itself. + */ public UnifyType getWildcardedType() { return wildcardedType; } diff --git a/test/unify/FiniteClosureTest.java b/test/unify/FiniteClosureTest.java index 519cf509..b58b9298 100644 --- a/test/unify/FiniteClosureTest.java +++ b/test/unify/FiniteClosureTest.java @@ -2,17 +2,13 @@ package unify; import java.util.Arrays; import java.util.HashSet; -import java.util.List; import java.util.Set; import java.util.stream.Collectors; import org.junit.Assert; import org.junit.Test; -import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; -import de.dhbwstuttgart.typeinference.unify.model.PairOperator; -import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.model.UnifyType; public class FiniteClosureTest { @@ -169,6 +165,7 @@ public class FiniteClosureTest { setExtT1, hashSetExtT1, treeSetExtT1, linkedHashSetExtT1 }).collect(Collectors.toSet())); + //System.out.println(fc.smaller(setExtT1)); Assert.assertEquals(expectedResult, fc.smaller(setExtT1)); /* @@ -395,7 +392,37 @@ public class FiniteClosureTest { Assert.assertEquals(82, actual.size()); Assert.assertTrue(actual.contains(myMapExtInt)); - Assert.assertTrue(actual.contains(myMapInt)); + Assert.assertTrue(actual.contains(myMapInt)); + + /* + * Test Case 16: + * + * smaller(FunN) = + * { FunN, FunN, + * FunN, FunN, + * FunN, FunN, + * FunN, FunN } + */ + + UnifyType object = tf.getSimpleType("Object"); + + fcb = new FiniteClosureBuilder(); + fcb.add(integer, number); + fcb.add(number, object); + fc = fcb.getCollectionExample(); + + UnifyType funNNumber = tf.getFunNType(number, number, number); + expectedResult = new HashSet<>(Arrays.stream(new UnifyType[] { + tf.getFunNType(number, number, number), tf.getFunNType(number, object, number), + tf.getFunNType(number, number, object), tf.getFunNType(number, object, object), + tf.getFunNType(integer, number, number), tf.getFunNType(integer, object, number), + tf.getFunNType(integer, number, object), tf.getFunNType(integer, object, object), + }).collect(Collectors.toSet())); + + actual = fc.smaller(funNNumber); + //System.out.println(actual); + Assert.assertEquals(expectedResult, actual); + } @Test @@ -633,41 +660,33 @@ public class FiniteClosureTest { * greater(SortedMap, ? super List>) = * */ - } - - @Test - public void testGrArg() { - IFiniteClosure fc = new FiniteClosureBuilder().getCollectionExample(); - TypeFactory tf = new TypeFactory(); - System.out.println("\n\n----- GrArg Test -----"); - System.out.println("GrArg(List) = " + fc.grArg(tf.getSimpleType("List", "T"))); - System.out.println("GrArg(? extends List) = " + fc.grArg(tf.getExtendsType(tf.getSimpleType("List", "T")))); - System.out.println("GrArg(? super List) = " + fc.grArg(tf.getSuperType(tf.getSimpleType("List", "T")))); - } - - - @Test - public void testSmArg() { - IFiniteClosure fc = new FiniteClosureBuilder().getCollectionExample(); - TypeFactory tf = new TypeFactory(); + /* + * Test Case 14: + * + * greater(FunN) = + * { FunN, FunN, + * FunN, FunN, + * FunN, FunN, + * FunN, FunN } + */ - System.out.println("\n\n----- SmArg Test -----"); - System.out.println("SmArg(List) = " + fc.smArg(tf.getSimpleType("List", "T"))); - System.out.println("SmArg(? extends List) = " + fc.smArg(tf.getExtendsType(tf.getSimpleType("List", "T")))); - System.out.println("SmArg(? super List) = " + fc.smArg(tf.getSuperType(tf.getSimpleType("List", "T")))); - } - - @Test - public void testGetGenericType() { - // TODO - } - - private void printDiff(Set expected, Set actual) { - System.out.println("Diff:"); - System.out.println("In expected but not in actual:"); - Set expected1 = new HashSet<>(expected); - expected1.removeAll(actual); - System.out.println(expected1); + UnifyType object = tf.getSimpleType("Object"); + + fcb = new FiniteClosureBuilder(); + fcb.add(integer, number); + fcb.add(number, object); + fc = fcb.getCollectionExample(); + + UnifyType funNNumber = tf.getFunNType(number, number, number); + expectedResult = new HashSet<>(Arrays.stream(new UnifyType[] { + tf.getFunNType(number, number, number), tf.getFunNType(number, integer, number), + tf.getFunNType(number, number, integer), tf.getFunNType(number, integer, integer), + tf.getFunNType(object, number, number), tf.getFunNType(object, integer, number), + tf.getFunNType(object, number, integer), tf.getFunNType(object, integer, integer) + }).collect(Collectors.toSet())); + + actual = fc.greater(funNNumber); + Assert.assertEquals(expectedResult, actual); } } diff --git a/test/unify/StandardUnifyTest.java b/test/unify/StandardUnifyTest.java index 2664324c..83f8abe1 100644 --- a/test/unify/StandardUnifyTest.java +++ b/test/unify/StandardUnifyTest.java @@ -32,8 +32,6 @@ public class StandardUnifyTest { System.out.println(unify.unify(f, y).get()); - // TODO ist das ergebnis { (x -> ? extends a), (y -> g) } in der richtigen form oder - // muss es { (x -> ? extends a), (y -> g) } sein? // {f,x> = f} UnifyType g = tf.getSimpleType("g", "x"); UnifyType f1 = tf.getSimpleType("f", g, x); diff --git a/test/unify/TypeFactory.java b/test/unify/TypeFactory.java index 099638e7..881222c8 100644 --- a/test/unify/TypeFactory.java +++ b/test/unify/TypeFactory.java @@ -4,9 +4,11 @@ import java.util.Arrays; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import de.dhbwstuttgart.typeinference.unify.model.UnifyType; public class TypeFactory { @@ -34,4 +36,9 @@ public class TypeFactory { public PlaceholderType getPlaceholderType(String name) { return new PlaceholderType(name); } + + public FunNType getFunNType(UnifyType... typeParams) { + return FunNType.getFunNType(new TypeParams(typeParams)); + } + } diff --git a/test/unify/UnifyOldTest.java b/test/unify/UnifyOldTest.java deleted file mode 100644 index e07f303c..00000000 --- a/test/unify/UnifyOldTest.java +++ /dev/null @@ -1,339 +0,0 @@ -package unify; - -import junit.framework.Assert; - -import org.junit.Test; - -import de.dhbwstuttgart.syntaxtree.factory.UnifyPairMengenBuilder; -import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory; -import de.dhbwstuttgart.syntaxtree.factory.Unify_FC_TTO_Builder; -import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType; -import de.dhbwstuttgart.syntaxtree.type.RefType; -import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType; -import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder; -import de.dhbwstuttgart.typeinference.Menge; -import de.dhbwstuttgart.typeinference.Pair; -import de.dhbwstuttgart.typeinference.unify.Unify; - -public class UnifyOldTest { - - @Test - public void unifyTest1() { - // Init Factories and Builders - UnifyTypeFactory typeFactory = new UnifyTypeFactory(); - Unify_FC_TTO_Builder fcBuilder = new Unify_FC_TTO_Builder(); - UnifyPairMengenBuilder assumptionBuilder = new UnifyPairMengenBuilder(); - UnifyPairMengenBuilder resultBuilder = new UnifyPairMengenBuilder(); - - TypePlaceholder a = typeFactory.GetTypePlaceholder("a"); - ExtendsWildcardType extA = typeFactory.GetExtendsType(a); - TypePlaceholder b = typeFactory.GetTypePlaceholder("a"); - ExtendsWildcardType extB = typeFactory.GetExtendsType(a); - RefType integer = typeFactory.GetSimpleType("Integer"); - SuperWildcardType supInt = typeFactory.GetSuperType(integer); - RefType listsupint = typeFactory.GetSimpleType("List", supInt); - RefType number = typeFactory.GetSimpleType("Number"); - RefType object = typeFactory.GetSimpleType("XObjectX"); - ExtendsWildcardType extNum = typeFactory.GetExtendsType(number); - RefType intlist = typeFactory.GetSimpleType("List", integer); - RefType alist = typeFactory.GetSimpleType("List", a); - RefType extBlist = typeFactory.GetSimpleType("List", extB); - RefType blist = typeFactory.GetSimpleType("List", b); - RefType extNumlist = typeFactory.GetSimpleType("List", extNum); - - fcBuilder.AddInheritance(number, object); - fcBuilder.AddInheritance(integer, number); - - - assumptionBuilder.addPair(alist, extBlist, PairOperator.Smaller); - assumptionBuilder.addPair(blist, extNumlist, PairOperator.Smaller); - - System.out.println(Unify.unify(assumptionBuilder.getPairMenge(), - fcBuilder.Get_FC_TTO())); - } -// -// @Test -// public void unifyTestSimpleTypes() { -// // Init Factories and Builders -// UnifyTypeFactory typeFactory = new UnifyTypeFactory(); -// Unify_FC_TTO_Builder fcBuilder = new Unify_FC_TTO_Builder(); -// UnifyPairMengenBuilder assumptionBuilder = new UnifyPairMengenBuilder(); -// UnifyPairMengenBuilder resultBuilder = new UnifyPairMengenBuilder(); -// -// /* -// * Test a <. Boolean -// */ -// -// // Init Types -// RefType boolT = typeFactory.GetSimpleType("java.lang.Boolean"); -// TypePlaceholder aTph = typeFactory.GetTypePlaceholder("a"); -// -// // Expected Result -// resultBuilder.clear(); -// resultBuilder.addPair(aTph, boolT, PairOperator.Equal); -// resultBuilder.addPair(aTph, typeFactory.GetExtendsType(boolT), -// PairOperator.Equal); -// Menge> expectedResult = resultBuilder.getNestedPairMenge(); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(aTph, boolT); -// Menge> actualResult = Unify.unify( -// assumptionBuilder.getPairMenge(), fcBuilder.Get_FC_TTO()); -// -// // System.out.println(expectedResult); -// // System.out.println(actualResult); -// -// Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// /* -// * Test b <. a, a <. Boolean -// */ -// -// // Init Types -// boolT = typeFactory.GetSimpleType("java.lang.Boolean"); -// aTph = typeFactory.GetTypePlaceholder("a"); -// TypePlaceholder bTph = typeFactory.GetTypePlaceholder("b"); -// -// // Expected Result -// resultBuilder.clear(); -// resultBuilder.addPair(aTph, boolT, PairOperator.Equal); -// resultBuilder.addPair(aTph, typeFactory.GetExtendsType(boolT), -// PairOperator.Equal); -// resultBuilder.addPair(bTph, boolT, PairOperator.Equal); -// resultBuilder.addPair(bTph, typeFactory.GetExtendsType(boolT), -// PairOperator.Equal); -// expectedResult = resultBuilder.getNestedPairMenge(); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(bTph, aTph); -// assumptionBuilder.addPair(aTph, boolT); -// actualResult = Unify.unify(assumptionBuilder.getPairMenge(), -// fcBuilder.Get_FC_TTO()); -// -// // System.out.println(expectedResult); -// // System.out.println(actualResult); -// -// // NOTE: Elemente im actualResult sind nicht unique -// // Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// /* -// * Test b <. a, a <. b -// */ -// -// aTph = typeFactory.GetTypePlaceholder("a"); -// bTph = typeFactory.GetTypePlaceholder("b"); -// -// // Expected Result -// resultBuilder.clear(); -// resultBuilder.addPair(bTph, aTph); -// resultBuilder.addPair(aTph, bTph); -// -// Menge buffer = resultBuilder.getPairMenge(); -// expectedResult = new Menge>(); -// expectedResult.add(buffer); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(bTph, aTph); -// assumptionBuilder.addPair(aTph, bTph); -// actualResult = Unify.unify(assumptionBuilder.getPairMenge(), -// fcBuilder.Get_FC_TTO()); -// -// // System.out.println(expectedResult); -// // System.out.println(actualResult); -// -// Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// /* -// * Test Integer <. a, a <. Boolean -// */ -// -// RefType intT = typeFactory.GetSimpleType("java.lang.Integer"); -// boolT = typeFactory.GetSimpleType("java.lang.Boolean"); -// aTph = typeFactory.GetTypePlaceholder("a"); -// bTph = typeFactory.GetTypePlaceholder("b"); -// -// // Expected Result -// resultBuilder.clear(); -// expectedResult = resultBuilder.getNestedPairMenge(); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(intT, aTph); -// assumptionBuilder.addPair(aTph, boolT); -// actualResult = Unify.unify(assumptionBuilder.getPairMenge(), -// fcBuilder.Get_FC_TTO()); -// -// // System.out.println(expectedResult); -// // System.out.println(actualResult); -// -// Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// } -// -// @Test -// public void unifyTestGenerics() { -// -// // Init Factories and Builders -// UnifyTypeFactory typeFactory = new UnifyTypeFactory(); -// Unify_FC_TTO_Builder fcBuilder = new Unify_FC_TTO_Builder(); -// UnifyPairMengenBuilder assumptionBuilder = new UnifyPairMengenBuilder(); -// UnifyPairMengenBuilder resultBuilder = new UnifyPairMengenBuilder(); -// -// /* -// * Test a <. MyClass -// */ -// -// TypePlaceholder aTph = typeFactory.GetTypePlaceholder("a"); -// RefType myType = typeFactory.GetSimpleType("MyClass", -// typeFactory.GetTypePlaceholder("T"), -// typeFactory.GetTypePlaceholder("F")); -// -// // Expected Result -// resultBuilder.clear(); -// resultBuilder.addPair(aTph, myType, PairOperator.Equal); -// resultBuilder.addPair(aTph, typeFactory.GetExtendsType(myType)); -// Menge> expectedResult = resultBuilder.getNestedPairMenge(); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(aTph, myType); -// Menge> actualResult = Unify.unify( -// assumptionBuilder.getPairMenge(), fcBuilder.Get_FC_TTO()); -// -// // System.out.println(expectedResult); -// // System.out.println(actualResult); -// -// Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// /* -// * Test List> <. List -// */ -// -// TypePlaceholder tTph = typeFactory.GetTypePlaceholder("T"); -// RefType list = typeFactory.GetSimpleType("List", tTph); -// RefType listlist = typeFactory.GetSimpleType("List", list); -// -// // Expected Result -// resultBuilder.clear(); -// resultBuilder.addPair(typeFactory.GetExtendsType(list), tTph, -// PairOperator.Equal); -// expectedResult = resultBuilder.getNestedPairMenge(); -// -// // Actual Result -// assumptionBuilder.clear(); -// assumptionBuilder.addPair(listlist, list); -// actualResult = Unify.unify(assumptionBuilder.getPairMenge(), -// fcBuilder.Get_FC_TTO()); -// -// System.out.println(expectedResult); -// System.out.println(actualResult); -// -// Assert.assertTrue(mengeEquals(expectedResult, actualResult)); -// -// /* -// * Test List <. List> -// */ -// } -// -// @Test -// public void unifyTestInheritance() { -// -// // Init Factories and Builders -// UnifyTypeFactory typeFactory = new UnifyTypeFactory(); -// Unify_FC_TTO_Builder fcBuilder = new Unify_FC_TTO_Builder(); -// UnifyPairMengenBuilder assumptionBuilder = new UnifyPairMengenBuilder(); -// UnifyPairMengenBuilder resultBuilder = new UnifyPairMengenBuilder(); -// -// // Init Types -// RefType tBool = typeFactory.GetSimpleType("java.lang.Boolean"); -// RefType tString = typeFactory.GetSimpleType("java.lang.String"); -// RefType tInt = typeFactory.GetSimpleType("java.lang.Integer"); -// TypePlaceholder tphA = typeFactory.GetTypePlaceholder("a"); -// -// // Build inheritance hierachy -// // Bool <. String <. Int -// fcBuilder.AddInheritance(tBool, tString); -// fcBuilder.AddInheritance(tString, tInt); -// -// // Build Assumptions -// assumptionBuilder.addPair(tphA, tString); -// -// // Build expected result -// resultBuilder.addPair(tphA, tBool, PairOperator.Equal); -// resultBuilder.addPair(tphA, typeFactory.GetExtendsType(tBool), -// PairOperator.Equal); -// resultBuilder.addPair(tphA, tString, PairOperator.Equal); -// resultBuilder.addPair(tphA, typeFactory.GetExtendsType(tString), -// PairOperator.Equal); -// -// // Assert -// Menge> actualResult = Unify.unify( -// assumptionBuilder.getPairMenge(), fcBuilder.Get_FC_TTO()); -// -// // System.out.println(actualResult); -// // System.out.println("-------------------"); -// // System.out.println(resultBuilder.getNestedPairMenge()); -// -// Assert.assertTrue(mengeEquals(resultBuilder.getNestedPairMenge(), -// actualResult)); -// } -// -// @Test -// public void unifyTestWildcards() { -// -// } -// -// private static boolean mengeEquals(Menge> m1, -// Menge> m2) { -// if (m1.size() != m2.size()) -// return false; -// -// return containsAll(m1, m2) && containsAll(m2, m1); -// } -// -// private static boolean containsAll(Menge> m1, -// Menge> m2) { -// for (Menge elem : m2) -// if (!contains(m1, elem)) -// return false; -// return true; -// } -// -// private static boolean contains(Menge> m1, Menge m2) { -// for (Menge elem : m1) -// if (mengePairEquals(elem, m2)) -// return true; -// return false; -// } -// -// private static boolean mengePairEquals(Menge m1, Menge m2) { -// if (m1.size() != m2.size()) -// return false; -// -// return containsAllPair(m1, m2) && containsAllPair(m2, m1); -// } -// -// private static boolean containsAllPair(Menge m1, Menge m2) { -// for (Pair elem : m1) -// if (contains(m2, elem)) -// return true; -// return false; -// } -// -// private static boolean contains(Menge m, Pair p) { -// for (Pair elem : m) -// if (pairEquals(elem, p)) -// return true; -// return false; -// -// } -// -// private static boolean pairEquals(Pair p1, Pair p2) { -// return (p1.TA1.equals(p2.TA1) && p1.TA2.equals(p2.TA2)) -// || (p1.TA1.equals(p2.TA2) && p1.TA2.equals(p2.TA1)); -// } - -} diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 3d091f5e..666731b8 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -129,6 +129,8 @@ public class UnifyTest extends Unify { addAsSet(expected, new UnifyPair(tphA, supObject, PairOperator.EQUALSDOT)); actual = unify(eq, fc); + System.out.println("? super Integer"); + System.out.println(actual); actual = filterGeneratedTPHsMultiple(actual); Assert.assertEquals(expected, actual); @@ -155,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); @@ -172,7 +175,7 @@ public class UnifyTest extends Unify { addAsSet(expected, new UnifyPair(tphA, extObject, PairOperator.EQUALSDOT)); actual = unify(eq, fc); - + actual = filterGeneratedTPHsMultiple(actual); Assert.assertEquals(expected, actual); @@ -197,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); @@ -278,9 +282,9 @@ public class UnifyTest extends Unify { UnifyType integer = tf.getSimpleType("Integer"); UnifyType doubl = tf.getSimpleType("Double"); - fcb.add(number, object); + //fcb.add(number, object); fcb.add(integer, number); - fcb.add(doubl, number); + //fcb.add(doubl, number); IFiniteClosure fc = fcb.getCollectionExample(); @@ -289,6 +293,10 @@ public class UnifyTest extends Unify { * * (Vector <. Vector) * (List <. List) + * + * Expected: + * {(b = Number), (a = Number)}, {(b = Number), (a = Integer)}, {(b = Number), (a = Integer)} + * (b = Integer), */ UnifyType tphA = tf.getPlaceholderType("a"); @@ -303,28 +311,9 @@ 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); - - /* - * Test 8: - * - * (a <.? ? sup b) - * (b = Number) - */ - - UnifyType supB = tf.getSuperType(tphB); - eq = new HashSet<>(); - eq.add(new UnifyPair(tphA, supB, PairOperator.SMALLERDOTWC)); - eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); - - expected = new HashSet<>(); - - actual = unify(eq, fc); - - System.out.println(actual); - //Assert.assertEquals(expected, actual); - + /* * Test 2: @@ -356,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); /* @@ -382,6 +371,194 @@ public class UnifyTest extends Unify { //Assert.assertEquals(actual, expected); } + /** + * These are tests that specifically test cases where the old unify algorithm was incomplete. + */ + @Test + public void unifyTestExtension() { + /* + * INIT + */ + TypeFactory tf = new TypeFactory(); + FiniteClosureBuilder fcb = new FiniteClosureBuilder(); + + UnifyType number = tf.getSimpleType("Number"); + UnifyType object = tf.getSimpleType("Object"); + UnifyType integer = tf.getSimpleType("Integer"); + UnifyType doubl = tf.getSimpleType("Double"); + UnifyType mygeneric = tf.getSimpleType("MyGeneric", "T"); + + + fcb.add(mygeneric, object); + fcb.add(integer, number); + //fcb.add(doubl, number); + + IFiniteClosure fc = fcb.getCollectionExample(); + + + /* + * Test 1: + * This is a Test for the extension of case 1 in the cartesian product of step 4. + * + * (a <. Vector) + * (List <. List) + * + * Expected: + * (b = Integer), (a = Vector) + * (b = ? extends Integer), (a = Vector), + * (b = ? extends Integer), (a = Vector), + * (b = ? super Integer), (a = Vector) + * (b = ? super Integer), (a = Vector) + * (b = ? super Integer), (a = Vector) + * (b = ? super Integer), (a = Vector) + * (b = ? extends Number), (a = Vector) + * (b = ? extends Number), (a = Vector) + * (b = ? extends Number), (a = Vector) + * (b = ? extends Number), (a = Vector) + */ + + UnifyType tphA = tf.getPlaceholderType("a"); + UnifyType tphB = tf.getPlaceholderType("b"); + UnifyType extB = tf.getExtendsType(tphB); + UnifyType extNum = tf.getExtendsType(number); + + Set eq = new HashSet(); + eq.add(new UnifyPair(tphA, tf.getSimpleType("Stack", tphB), PairOperator.SMALLERDOT)); + eq.add(new UnifyPair(tf.getSimpleType("List", integer), tf.getSimpleType("List", tphB), PairOperator.SMALLERDOT)); + + Set> expected = new HashSet<>(); + Set> actual = unify(eq, fc); + + System.out.println(actual); + //Assert.assertEquals(actual, expected); + + /* + * Test 2: + * + * This is a test for th extension of case 2 of the cartesian product of step 4. + * + * (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. + * + * (a <.? ? sup b) + * (b = Number) + */ + + UnifyType supB = tf.getSuperType(tphB); + eq = new HashSet<>(); + eq.add(new UnifyPair(tphA, supB, PairOperator.SMALLERDOTWC)); + eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + + System.out.println("Case 3"); + System.out.println(actual); + //Assert.assertEquals(expected, actual); + + /* + * Case 4 has no extension + */ + + /* + * Test 5: + * This is a test for the extension of case 5 of the cartesian product of step 4. + * + * Vector <. a + * b =. Number + */ + + eq = new HashSet<>(); + eq.add(new UnifyPair(tf.getSimpleType("HashSet", tphB), tphA, PairOperator.SMALLERDOT)); + eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + System.out.println(actual); + //Assert.assertEquals(expected, actual); + + /* + * Test 6: + * This is a test for the extension of case 6 of the cartesian product of step 4. + * + * ? extends b <.? a + * b =. Integer + */ + + eq = new HashSet<>(); + eq.add(new UnifyPair(extB, tphA, PairOperator.SMALLERDOTWC)); + eq.add(new UnifyPair(tphB, integer, PairOperator.EQUALSDOT)); + + expected = new HashSet<>(); + + actual = unify(eq, fc); + + 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 public void unifyTestComplex() { /*