From 4576efe3ec8dc0520a893b59c99c9a053fb551e6 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Mon, 23 Nov 2015 00:12:08 +0100 Subject: [PATCH] implemented step 4 (some cases still missing) --- .../unify/interfaces/IFiniteClosure.java | 2 +- .../typeinference/unifynew/Unify.java | 135 +++++++++++++----- 2 files changed, 100 insertions(+), 37 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index e469f41ac..0601d70f3 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -22,7 +22,7 @@ public interface IFiniteClosure { * @return The set of supertypes of the argument. */ public Set greater(Type type); - + /** * Wo passt Type rein? * @param type diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index b87cd2b62..cb8ff602f 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -16,30 +16,26 @@ import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; +import de.dhbwstuttgart.typinference.unify.model.ExtendsType; import de.dhbwstuttgart.typinference.unify.model.MPair; import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; import de.dhbwstuttgart.typinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typinference.unify.model.SuperType; +import de.dhbwstuttgart.typinference.unify.model.Type; /** - * Implementierung des Unifikationsalgorithmus. + * Implementation of the type unification algorithm * @author Florian Steurer */ public class Unify { - public Menge> unify(Menge eq, IFiniteClosure fc) { - /* - * Preparations: Create Mapping - */ - - Set eq0 = null; - - + public Menge> unify(Menge eq, IFiniteClosure fc) { /* * Step 1: Repeated application of reduce, adapt, erase, swap */ - eq0 = applyTypeUnificationRules(eq0, fc); + Set eq0 = applyTypeUnificationRules(eq, fc); /* @@ -51,35 +47,34 @@ public class Unify { splitEq(eq0, eq1s, eq2s); /* - * Step 4: Magic + * Step 4: Create possible typings */ // Sets that originate from pair pattern matching // Sets of the "second level" - Set>> pairSets = new HashSet>>(); - for(MPair pair : eq2s) - pairSets.add(calculateSets(pair)); - + List>> pairSets = calculatePairSets(eq2s, fc); + // The sets of the "first level" Set> sets = new HashSet>(); - - // Add Eq1' - sets.add(eq1s); + sets.add(eq1s); // Add Eq1' // Add the set of [a =. Theta | (a=. Theta) in Eq2'] sets.add(eq2s.stream() .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) .collect(Collectors.toSet())); - /* - * Around here, filters for pairs and sets can be applied - */ + /* Up to here, no cartesian products are calculated. + * Around here, filters for pairs and sets can be applied */ ISetOperations setOps = new GuavaSetOperations(); - for(List> pairSet : pairSets) - setOps.cartesianProduct(pairSet).forEach(x -> sets.add(new HashSet(x))); - // Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte + // Calculate the inner cartesian products + // Cartesian products of the second level + for(List> pairSet : pairSets) // Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte + setOps.cartesianProduct(pairSet).forEach(x -> sets.add(new HashSet(x))); + + // Calculate the outer cartesian products + // Cartesian products of the first level Set> eqsSet = setOps.cartesianProduct(new ArrayList<>(sets)); /* @@ -99,18 +94,6 @@ public class Unify { throw new NotImplementedException(); } - protected List> calculateSets(MPair pair) { - return null; - } - - protected void splitEq(Set eq, Set eq1s, Set eq2s) { - for(MPair pair : eq) - if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType) - eq1s.add(pair); - else - eq2s.add(pair); - } - protected Set applyTypeUnificationRules(Set eq, IFiniteClosure fc) { /* @@ -183,4 +166,84 @@ public class Unify { collection.add(pair2); } + + protected void splitEq(Set eq, Set eq1s, Set eq2s) { + for(MPair pair : eq) + if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType) + eq1s.add(pair); + else + eq2s.add(pair); + } + + + protected List>> calculatePairSets(Set eq2s, IFiniteClosure fc) { + List>> result = new ArrayList>>(); + for(int i = 0; i < 8; i++) + result.add(new ArrayList>()); + + + for(MPair pair : eq2s) { + + PairOperator pairOp = pair.getPairOp(); + Type lhsType = pair.getLhsType(); + Type rhsType = pair.getRhsType(); + + // Case 1: (a <. Theta') + if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) { + // TODO + } + + // Case 2: (a <.? ? ext Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){ + // TODO + } + + // Case 3: (a <.? ? sup Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) { + Set set = new HashSet<>(); + for(Type theta : fc.smArg(rhsType)) + set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT)); + + result.get(2).add(set); + } + + // Case 4: (a <.? Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) { + Set set = new HashSet<>(); + set.add(new MPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT)); + result.get(3).add(set); + } + + // Case 5: (Theta <. a) + else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) { + Set set = new HashSet<>(); + for(Type thetaS : fc.greater(lhsType)) + set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); + result.get(4).add(set); + } + + // Case 6: (? ext Theta <.? a) + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) { + Set set = new HashSet<>(); + for(Type thetaS : fc.grArg(lhsType)) + set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); + result.get(5).add(set); + } + + // Case 7: (? sup Theta <.? a) + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) { + // TODO + } + + // Case 8: (Theta <.? a) + else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) { + Set set = new HashSet<>(); + for(Type thetaS : fc.grArg(lhsType)) + set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); + result.get(7).add(set); + } + } + + return result.stream().filter(x -> !x.isEmpty()).collect(Collectors.toList()); + } }