diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 7319787b..79c0f329 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -25,11 +25,14 @@ 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; +import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair; import java.io.File; import java.io.FileWriter; import java.io.IOException; +import com.google.common.collect.Ordering; + /** * Implementation of the type unification algorithm @@ -63,11 +66,18 @@ public class TypeUnifyTask extends RecursiveTask>> { protected IFiniteClosure fc; + protected Ordering> oup; + protected boolean parallel; + public TypeUnifyTask() { + rules = new RuleSet(); + } + public TypeUnifyTask(Set eq, IFiniteClosure fc, boolean parallel) { this.eq = eq; this.fc = fc; + this.oup = new OrderingUnifyPair(fc); this.parallel = parallel; try { logFile = new FileWriter(new File(rootDirectory+"log")); @@ -138,7 +148,7 @@ public class TypeUnifyTask extends RecursiveTask>> { // Sets of the "second level" Set undefinedPairs = new HashSet<>(); if (printtag) System.out.println("eq2s " + eq2s); - writeLog(bufferSet.toString()+"\n"); + writeLog("BufferSet: " + bufferSet.toString()+"\n"); Set>>> secondLevelSets = calculatePairSets(eq2s, fc, undefinedPairs); //PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer //nicht ausgewertet Faculty Beispiel im 1. Schritt @@ -180,13 +190,13 @@ public class TypeUnifyTask extends RecursiveTask>> { //Aufruf von computeCartesianRecursive ANFANG - //return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, fc, parallel); + return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, fc, parallel); - //} + } - //Set> unify2(Set> setToFlatten, Set eq, IFiniteClosure fc, boolean parallel) { + Set> unify2(Set> setToFlatten, Set eq, IFiniteClosure fc, boolean parallel) { //Aufruf von computeCartesianRecursive ENDE //keine Ahnung woher das kommt @@ -194,9 +204,9 @@ public class TypeUnifyTask extends RecursiveTask>> { //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG // Cartesian product over all (up to 10) top level sets - Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) - .stream().map(x -> new HashSet<>(x)) - .collect(Collectors.toCollection(HashSet::new)); + //Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) + // .stream().map(x -> new HashSet<>(x)) + // .collect(Collectors.toCollection(HashSet::new)); //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE Set> eqPrimePrimeSet = new HashSet<>(); @@ -204,7 +214,7 @@ public class TypeUnifyTask extends RecursiveTask>> { Set forks = new HashSet<>(); //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG - for(Set> setToFlatten : eqPrimeSet) { + //for(Set> setToFlatten : eqPrimeSet) { // Flatten the cartesian product //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE Set eqPrime = new HashSet<>(); @@ -266,7 +276,7 @@ public class TypeUnifyTask extends RecursiveTask>> { } } //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG - } + //} //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE /* @@ -292,17 +302,25 @@ public class TypeUnifyTask extends RecursiveTask>> { ArrayList> newSet = new ArrayList<>(set); Set> result = null; int i = 0; - for(Set a : newSet) { + Set a_next = oup.min(newSet.iterator()); + while (newSet.size() != 0) { + Set a = a_next; + writeLog("NewSet: " + newSet.toString()+ "\n"); + newSet.remove(a); + if (newSet.size() > 0) a_next = oup.min(newSet.iterator()); + //for(Set a : newSet) { i++; Set> elems = new HashSet>(fstElems); elems.add(a); if (newSets.isEmpty()) { - //BEI BENUTZUNG EIKOMMENTIEREN result = unify2(elems, eq, fc, parallel); + result = unify2(elems, eq, fc, parallel); + System.out.println(""); } else { result = computeCartesianRecursive(elems,newSets, eq, fc, parallel); } - if (!result.isEmpty()) break; + if (!result.isEmpty()) //&& (oup.compare(a, a_next) == -1)) break; + if (oup.compare(a, a_next) == -1) break; } return result; } @@ -332,7 +350,7 @@ public class TypeUnifyTask extends RecursiveTask>> { * This is step one of the unification algorithm. * @return The set of pairs that results from repeated application of the inference rules. */ - protected Set applyTypeUnificationRules(Set eq, IFiniteClosure fc) { + public Set applyTypeUnificationRules(Set eq, IFiniteClosure fc) { /* * Rule Application Strategy: @@ -663,9 +681,10 @@ public class TypeUnifyTask extends RecursiveTask>> { else resultPrime.add(new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT)); resultPrime.addAll(substitutionSet); - writeLog(substitutionSet.toString()); + writeLog("Substitution: " + substitutionSet.toString()); result.add(resultPrime); - writeLog(resultPrime.toString()); + writeLog("Result: " + resultPrime.toString()); + //writeLog("MAX: " + oup.max(resultPrime.iterator()).toString()); } } @@ -692,7 +711,7 @@ public class TypeUnifyTask extends RecursiveTask>> { resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT)); resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT)); result.add(resultPrime); - writeLog(resultPrime.toString()); + writeLog("Result: " + resultPrime.toString()); return result; } diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index dcb6c4d1..110ff4b8 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -60,5 +60,7 @@ public interface IFiniteClosure { public Optional getLeftHandedType(String typeName); public Set getAncestors(UnifyType t); public Set getChildren(UnifyType t); - public Set getAllTypesByName(String typeName); + public Set getAllTypesByName(String typeName); + + public int compare(UnifyType rhsType, UnifyType rhsType2); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 5613953a..6500abcf 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -8,11 +8,14 @@ import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; +import com.google.common.collect.Ordering; + //PL 18-02-05 Unifier durch Matcher ersetzt //mus greater noch erstezt werden import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify; import de.dhbwstuttgart.typeinference.unify.Match; +import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; @@ -20,7 +23,7 @@ import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; * The finite closure for the type unification * @author Florian Steurer */ -public class FiniteClosure implements IFiniteClosure { +public class FiniteClosure extends Ordering implements IFiniteClosure { /** * A map that maps every type to the node in the inheritance graph that contains that type. @@ -430,4 +433,24 @@ public class FiniteClosure implements IFiniteClosure { public String toString(){ return this.inheritanceGraph.toString(); } + + public int compare (UnifyType left, UnifyType right) { + UnifyPair up = new UnifyPair(left, right, PairOperator.SMALLERDOT); + TypeUnifyTask unifyTask = new TypeUnifyTask(); + HashSet hs = new HashSet<>(); + hs.add(up); + Set smallerRes = unifyTask.applyTypeUnificationRules(hs, this); + long smallerLen = smallerRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count(); + if (smallerLen == 0) return -1; + else { + up = new UnifyPair(right, left, PairOperator.SMALLERDOT); + //TypeUnifyTask unifyTask = new TypeUnifyTask(); + hs = new HashSet<>(); + hs.add(up); + Set greaterRes = unifyTask.applyTypeUnificationRules(hs, this); + long greaterLen = greaterRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count(); + if (greaterLen == 0) return 1; + else return 0; + } + } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java new file mode 100644 index 00000000..5cf69f76 --- /dev/null +++ b/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java @@ -0,0 +1,39 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashMap; +import java.util.Optional; +import java.util.Set; +import java.util.function.BinaryOperator; +import java.util.stream.Stream; + +import com.google.common.collect.Ordering; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; + + + +public class OrderingUnifyPair extends Ordering> { + + protected IFiniteClosure fc; + + public OrderingUnifyPair(IFiniteClosure fc) { + this.fc = fc; + } + + public int compare (UnifyPair left, UnifyPair right) { + if (left == null || right == null) + System.out.println("Fehler"); + return fc.compare(left.getRhsType(), right.getRhsType()); + } + + public int compare (Set left, Set right) { + Stream ls = left.stream().filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)); + Stream rs = right.stream().filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)); + BinaryOperator> combiner = (x,y) -> { x.putAll(y); return x;}; + HashMap hm = rs.reduce(new HashMap(), (x, y)-> { x.put(y.getLhsType(),y); return x; }, combiner); + ls = ls.filter(x -> !(hm.get(x.getLhsType()) == null)); + Optional si = ls.map(x -> compare(x, hm.get(x.getLhsType()))).reduce((x,y)-> { if (x == y) return x; else return 0; } ); + if (!si.isPresent()) return 0; + else return si.get(); + } +} diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java index 0909690a..8d038fd3 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java @@ -4,6 +4,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; + /** * A pair which contains two types and an operator, e.q. (Integer <. a). * @author Florian Steurer