From b8415b122b3cee3f588a626d091b1f75d3855f8b Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Thu, 21 Apr 2016 20:26:33 +0200 Subject: [PATCH 1/8] stringbuilder in logger --- src/de/dhbwstuttgart/logger/Logger.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/de/dhbwstuttgart/logger/Logger.java b/src/de/dhbwstuttgart/logger/Logger.java index 64836c07..c1bbd93e 100755 --- a/src/de/dhbwstuttgart/logger/Logger.java +++ b/src/de/dhbwstuttgart/logger/Logger.java @@ -127,11 +127,11 @@ class LogHistory extends ArrayList{ @Override public String toString(){ - String ret = ""; + StringBuilder ret = new StringBuilder(); for(LogLine l : this){ - ret += l.toString() + "\n"; + ret.append(l.toString() + "\n"); } - return ret; + return ret.toString(); } } From bb8df92cba2257491524b587086d4ad5f578d55b Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Thu, 21 Apr 2016 22:19:48 +0200 Subject: [PATCH 2/8] equals / hashcode optimization --- .../unify/model/ExtendsType.java | 12 ++++++-- .../unify/model/FiniteClosure.java | 1 - .../typeinference/unify/model/FunNType.java | 11 +++++-- .../unify/model/ReferenceType.java | 25 +++++++++++++--- .../typeinference/unify/model/SuperType.java | 8 ++++- .../typeinference/unify/model/TypeParams.java | 30 ++++++++++++++++--- .../typeinference/unify/model/UnifyPair.java | 3 ++ .../unify/model/WildcardType.java | 3 ++ 8 files changed, 79 insertions(+), 14 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java index d5490e96..13049c88 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); + super("? extends " + extendedType.getName(), extendedType); } /** @@ -44,7 +44,10 @@ public final class ExtendsType extends WildcardType { @Override UnifyType apply(Unifier unif) { - return new ExtendsType(wildcardedType.apply(unif)); + UnifyType newType = wildcardedType.apply(unif); + /*if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created*/ + return new ExtendsType(newType); } @Override @@ -61,7 +64,12 @@ public final class ExtendsType extends WildcardType { if(!(obj instanceof ExtendsType)) return false; + if(obj.hashCode() != this.hashCode()) + return false; + ExtendsType other = (ExtendsType) obj; + + return other.getWildcardedType().equals(wildcardedType); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index ac0862cc..a08f79cb 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -33,7 +33,6 @@ public class FiniteClosure implements IFiniteClosure { */ private Set pairs; - //TODO Prüfen: Typen ohne Kante im Graph als extra Menge im Konstruktor mitgeben? /** * Creates a new instance using the inheritance tree defined in the pairs. */ diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java index 94ac1cf8..31517891 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java @@ -58,7 +58,11 @@ public class FunNType extends UnifyType { UnifyType apply(Unifier unif) { // TODO this bypasses the validation of the type parameters. // Wildcard types can be unified into FunNTypes. - return new FunNType(typeParams.apply(unif)); + TypeParams newParams = typeParams.apply(unif); + /*if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this;*/ + + return new FunNType(newParams); } @Override @@ -71,8 +75,11 @@ public class FunNType extends UnifyType { if(!(obj instanceof FunNType)) return false; - FunNType other = (FunNType) obj; + if(obj.hashCode() != this.hashCode()) + return false; + FunNType other = (FunNType) obj; + return other.getTypeParams().equals(typeParams); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java index ad02c9ab..9ffea796 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java @@ -11,12 +11,19 @@ import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; */ public final class ReferenceType extends UnifyType { - public ReferenceType(String name, UnifyType... typeParams) { - super(name, new TypeParams(typeParams)); + /** + * The buffered hashCode + */ + private final int hashCode; + + public ReferenceType(String name, UnifyType... params) { + super(name, new TypeParams(params)); + hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); } public ReferenceType(String name, TypeParams params) { super(name, params); + hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); } @Override @@ -31,17 +38,24 @@ public final class ReferenceType extends UnifyType { @Override UnifyType apply(Unifier unif) { - return new ReferenceType(typeName, typeParams.apply(unif)); + TypeParams newParams = typeParams.apply(unif); + + /*if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this;*/ + + return new ReferenceType(new String(typeName), newParams); } @Override public UnifyType setTypeParams(TypeParams newTp) { + /*if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) + return this; // reduced the amount of objects created*/ return new ReferenceType(new String(typeName), newTp); } @Override public int hashCode() { - return 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); + return hashCode; } @Override @@ -49,6 +63,9 @@ public final class ReferenceType extends UnifyType { if(!(obj instanceof ReferenceType)) return false; + if(obj.hashCode() != this.hashCode()) + return false; + ReferenceType other = (ReferenceType) obj; if(!other.getName().equals(typeName)) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java index 8a828156..664e1624 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -50,7 +50,10 @@ public final class SuperType extends WildcardType { @Override UnifyType apply(Unifier unif) { - return new SuperType(wildcardedType.apply(unif)); + UnifyType newType = wildcardedType.apply(unif); + /*if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created*/ + return new SuperType(newType); } @Override @@ -67,6 +70,9 @@ public final class SuperType extends WildcardType { if(!(obj instanceof SuperType)) return false; + if(obj.hashCode() != this.hashCode()) + return false; + SuperType other = (SuperType) obj; return other.getSuperedType().equals(wildcardedType); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index 7ce251d9..f2336e96 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -39,7 +39,7 @@ public final class TypeParams implements Iterable{ */ public TypeParams(UnifyType... types) { typeParams = types; - + // Hashcode calculation is expensive and must be cached. hashCode = Arrays.hashCode(typeParams); } @@ -73,8 +73,22 @@ public final class TypeParams implements Iterable{ */ public TypeParams apply(Unifier unif) { UnifyType[] newParams = new UnifyType[typeParams.length]; - for(int i = 0; i < typeParams.length; i++) - newParams[i] = typeParams[i].apply(unif); + + // If true, a type was modified and a new typeparams object has to be created. + // Otherwise it is enough to return this object, since it is immutable + // This reduced the needed TypeParams-Instances for the lambda14-Test from + // 130.000 to 30.000 without a decrease in speed. + boolean isNew = false; + + for(int i = 0; i < typeParams.length; i++) { + UnifyType newType = typeParams[i].apply(unif); + newParams[i] = newType; + //if(!isNew && (newType.hashCode() != typeParams[i].hashCode() || !newType.equals(typeParams[i]))) + //isNew = true; + } + + //if(!isNew) + // return this; return new TypeParams(newParams); } @@ -107,8 +121,13 @@ public final class TypeParams implements Iterable{ * @throws ArrayOutOfBoundsException if i > this.size()-1. */ public TypeParams set(UnifyType t, int idx) { + // Reduce the creation of new objects for less memory + // Reduced the needed instances of TypeParams in the lambda14-Test from + // 150.000 to 130.000 + /*if(t.hashCode() == typeParams[idx].hashCode() && t.equals(typeParams[idx])) + return this;*/ UnifyType[] newparams = Arrays.copyOf(typeParams, typeParams.length); - newparams[idx] = t; + newparams[idx] = t; return new TypeParams(newparams); } @@ -127,6 +146,9 @@ public final class TypeParams implements Iterable{ if(!(obj instanceof TypeParams)) return false; + if(obj.hashCode() != this.hashCode()) + return false; + TypeParams other = (TypeParams) obj; if(other.size() != this.size()) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java index 62de0c96..672a516d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java @@ -63,6 +63,9 @@ public class UnifyPair { public boolean equals(Object obj) { if(!(obj instanceof UnifyPair)) return false; + + if(obj.hashCode() != this.hashCode()) + return false; UnifyPair other = (UnifyPair) obj; diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java b/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java index 19efd88a..9b42c087 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java @@ -47,6 +47,9 @@ public abstract class WildcardType extends UnifyType { if(!(obj instanceof WildcardType)) return false; + if(obj.hashCode() != this.hashCode()) + return false; + WildcardType other = (WildcardType) obj; return other.getWildcardedType().equals(wildcardedType); } From 7b6b720b573967763e93bc33fc143f916213e6db Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Thu, 21 Apr 2016 22:31:36 +0200 Subject: [PATCH 3/8] memory optimization --- .../typeinference/unify/model/ExtendsType.java | 7 +++++-- .../typeinference/unify/model/FunNType.java | 6 ++++-- .../typeinference/unify/model/ReferenceType.java | 8 ++++---- .../typeinference/unify/model/SuperType.java | 7 +++++-- .../typeinference/unify/model/TypeParams.java | 16 ++++++++-------- 5 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java index 13049c88..014500bc 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java @@ -29,6 +29,9 @@ public final class ExtendsType extends WildcardType { */ @Override public UnifyType setTypeParams(TypeParams newTp) { + UnifyType newType = wildcardedType.setTypeParams(newTp); + if(newType == wildcardedType) + return this; // Reduced the amount of objects created return new ExtendsType(wildcardedType.setTypeParams(newTp)); } @@ -45,8 +48,8 @@ public final class ExtendsType extends WildcardType { @Override UnifyType apply(Unifier unif) { UnifyType newType = wildcardedType.apply(unif); - /*if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) - return this; // Reduced the amount of objects created*/ + if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created return new ExtendsType(newType); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java index 31517891..b7e5c60e 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FunNType.java @@ -41,6 +41,8 @@ public class FunNType extends UnifyType { @Override public UnifyType setTypeParams(TypeParams newTp) { + if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) + return this; return getFunNType(newTp); } @@ -59,8 +61,8 @@ public class FunNType extends UnifyType { // TODO this bypasses the validation of the type parameters. // Wildcard types can be unified into FunNTypes. TypeParams newParams = typeParams.apply(unif); - /*if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) - return this;*/ + if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this; return new FunNType(newParams); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java index 9ffea796..e82affe0 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java @@ -40,16 +40,16 @@ public final class ReferenceType extends UnifyType { UnifyType apply(Unifier unif) { TypeParams newParams = typeParams.apply(unif); - /*if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) - return this;*/ + if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this; return new ReferenceType(new String(typeName), newParams); } @Override public UnifyType setTypeParams(TypeParams newTp) { - /*if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) - return this; // reduced the amount of objects created*/ + if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) + return this; // reduced the amount of objects created return new ReferenceType(new String(typeName), newTp); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java index 664e1624..4f78602f 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -35,6 +35,9 @@ public final class SuperType extends WildcardType { */ @Override public UnifyType setTypeParams(TypeParams newTp) { + UnifyType newType = wildcardedType.setTypeParams(newTp); + if(newType == wildcardedType) + return this; // Reduced the amount of objects created return new SuperType(wildcardedType.setTypeParams(newTp)); } @@ -51,8 +54,8 @@ public final class SuperType extends WildcardType { @Override UnifyType apply(Unifier unif) { UnifyType newType = wildcardedType.apply(unif); - /*if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) - return this; // Reduced the amount of objects created*/ + if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created return new SuperType(newType); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index f2336e96..02edb933 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -30,7 +30,7 @@ public final class TypeParams implements Iterable{ typeParams[i] = types.get(i); // Hashcode calculation is expensive and must be cached. - hashCode = Arrays.hashCode(typeParams); + hashCode = Arrays.deepHashCode(typeParams); } /** @@ -41,7 +41,7 @@ public final class TypeParams implements Iterable{ typeParams = types; // Hashcode calculation is expensive and must be cached. - hashCode = Arrays.hashCode(typeParams); + hashCode = Arrays.deepHashCode(typeParams); } /** @@ -83,12 +83,12 @@ public final class TypeParams implements Iterable{ for(int i = 0; i < typeParams.length; i++) { UnifyType newType = typeParams[i].apply(unif); newParams[i] = newType; - //if(!isNew && (newType.hashCode() != typeParams[i].hashCode() || !newType.equals(typeParams[i]))) - //isNew = true; + if(!isNew && (newType.hashCode() != typeParams[i].hashCode() || !newType.equals(typeParams[i]))) + isNew = true; } - //if(!isNew) - // return this; + if(!isNew) + return this; return new TypeParams(newParams); } @@ -124,8 +124,8 @@ public final class TypeParams implements Iterable{ // Reduce the creation of new objects for less memory // Reduced the needed instances of TypeParams in the lambda14-Test from // 150.000 to 130.000 - /*if(t.hashCode() == typeParams[idx].hashCode() && t.equals(typeParams[idx])) - return this;*/ + if(t.hashCode() == typeParams[idx].hashCode() && t.equals(typeParams[idx])) + return this; UnifyType[] newparams = Arrays.copyOf(typeParams, typeParams.length); newparams[idx] = t; return new TypeParams(newparams); From 6eb7f2d1bbf2a0bc08c82e629575b4a4935a72d0 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Fri, 22 Apr 2016 10:24:33 +0200 Subject: [PATCH 4/8] removed creation of new strings --- .../typeinference/unify/model/ReferenceType.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java index e82affe0..02ab38a0 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java @@ -43,14 +43,14 @@ public final class ReferenceType extends UnifyType { if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) return this; - return new ReferenceType(new String(typeName), newParams); + return new ReferenceType(typeName, newParams); } @Override public UnifyType setTypeParams(TypeParams newTp) { if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) return this; // reduced the amount of objects created - return new ReferenceType(new String(typeName), newTp); + return new ReferenceType(typeName, newTp); } @Override From 752723020ecefcb856944186b0c5437ef34a59e7 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Fri, 22 Apr 2016 15:45:20 +0200 Subject: [PATCH 5/8] pipe execution --- .../typeinference/unify/TypeUnify.java | 88 +++++-------------- 1 file changed, 24 insertions(+), 64 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index 031576d9..5d51f137 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -3,7 +3,6 @@ package de.dhbwstuttgart.typeinference.unify; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; -import java.util.Collections; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.LinkedList; @@ -11,7 +10,6 @@ import java.util.List; import java.util.Map.Entry; import java.util.Optional; import java.util.Set; -import java.util.function.Function; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; @@ -19,13 +17,13 @@ import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; -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.SuperType; -import de.dhbwstuttgart.typeinference.unify.model.UnifyType; -import de.dhbwstuttgart.typeinference.unify.model.PairOperator; 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; /** @@ -49,10 +47,6 @@ public class TypeUnify { */ protected IRuleSet rules = new RuleSet(); - // Scheint momentan eher zu verlangsamen, vermutlich zu viele threads, - // threadpool und task-queue einbauen und minimale problemgröße für neuen thread - protected boolean parallel = false; - /** * Computes all principal type unifiers for a set of constraints. * @param eq The set of constraints @@ -138,66 +132,32 @@ public class TypeUnify { .collect(Collectors.toCollection(HashSet::new)); //System.out.println(result); - // Flatten the cartesian product - // TODO parallelisierung möglich (scheint sich nicht zu lohnen) - Set> eqPrimeSetFlat = new HashSet<>(); - for(Set> setToFlatten : eqPrimeSet) { - Set buffer = new HashSet<>(); - setToFlatten.stream().forEach(x -> buffer.addAll(x)); - eqPrimeSetFlat.add(buffer); - } - - - /* - * Step 5: Substitution - */ - Set> restartSet = new HashSet<>(); Set> eqPrimePrimeSet = new HashSet<>(); - - if(parallel) { - Set> restartSetSync = Collections.synchronizedSet(restartSet); - Set> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet); + // Flatten the cartesian product + // TODO parallelisierung möglich (scheint sich nicht zu lohnen) + for(Set> setToFlatten : eqPrimeSet) { + Set eqPrime = new HashSet<>(); + setToFlatten.stream().forEach(x -> eqPrime.addAll(x)); + + /* + * Step 5: Substitution + */ + Optional> eqPrimePrime = rules.subst(eqPrime); - eqPrimeSetFlat.parallelStream().forEach(eqPrime -> { - Optional> eqPrimePrime = rules.subst(eqPrime); - - if (eqPrime.equals(eq)) - eqPrimePrimeSetSync.add(eqPrime); - else if(eqPrimePrime.isPresent()) - restartSetSync.add(eqPrimePrime.get()); - else - restartSetSync.add(eqPrime); - }); + + /* + * Step 6 a) Restart for pairs where subst was applied + * b) Build the union over everything + */ + if (eqPrime.equals(eq)) + eqPrimePrimeSet.add(eqPrime); + else if(eqPrimePrime.isPresent()) + eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc)); + else + eqPrimePrimeSet.addAll(this.unify(eqPrime, fc)); } - else { - for(Set eqPrime : eqPrimeSetFlat) { - Optional> eqPrimePrime = rules.subst(eqPrime); - - if (eqPrime.equals(eq)) - eqPrimePrimeSet.add(eqPrime); - else if(eqPrimePrime.isPresent()) - restartSet.add(eqPrimePrime.get()); - else - restartSet.add(eqPrime); - } - } - - /* - * Step 6 a) Restart for pairs where subst was applied - * b) Build the union over everything - */ - // TODO parallelisierung möglich (lohnt sich vermutlich) - if(parallel) { - Set> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet); - restartSet.parallelStream().forEach( x -> eqPrimePrimeSetSync.addAll(unify(x, fc))); - } - else { - for(Set eqss : restartSet) - eqPrimePrimeSet.addAll(this.unify(eqss, fc)); - } - /* * Step 7: Filter empty sets; */ From 8fa8fc8758c8270d5424d594691d834af1b99cdd Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Fri, 22 Apr 2016 16:11:18 +0200 Subject: [PATCH 6/8] comment --- src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index 5d51f137..d0af8c9e 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -134,9 +134,14 @@ public class TypeUnify { Set> eqPrimePrimeSet = new HashSet<>(); - // Flatten the cartesian product // TODO parallelisierung möglich (scheint sich nicht zu lohnen) + /* + * Die Parallelisierung über parallelStream() ist langsamer als die serielle Ausführung, + * vermutlich wird zuviel thread-overhead erzeugt. + * Vermutlich ist die beste Lösung hier ein Fork-Join-Framework. + */ for(Set> setToFlatten : eqPrimeSet) { + // Flatten the cartesian product Set eqPrime = new HashSet<>(); setToFlatten.stream().forEach(x -> eqPrime.addAll(x)); From 7d75f1831989627a890b658c12d55d23faa6d7b1 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Fri, 22 Apr 2016 16:51:05 +0200 Subject: [PATCH 7/8] Parallelisierung mit Fork-Join Pool --- .../typeinference/unify/TypeUnify.java | 601 +---------------- .../typeinference/unify/TypeUnifyTask.java | 631 ++++++++++++++++++ test/unify/UnifyTest.java | 94 +-- 3 files changed, 684 insertions(+), 642 deletions(-) create mode 100644 src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index d0af8c9e..ec013f9d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -1,605 +1,16 @@ package de.dhbwstuttgart.typeinference.unify; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collection; -import java.util.HashSet; -import java.util.LinkedHashSet; -import java.util.LinkedList; -import java.util.List; -import java.util.Map.Entry; -import java.util.Optional; import java.util.Set; -import java.util.stream.Collectors; +import java.util.concurrent.ForkJoinPool; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; -import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; -import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; -import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typeinference.unify.model.PairOperator; -import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typeinference.unify.model.SuperType; -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 type unification algorithm - * @author Florian Steurer - */ public class TypeUnify { - - /** - * The implementation of setOps that will be used during the unification - */ - protected ISetOperations setOps = new GuavaSetOperations(); - - /** - * The implementation of the standard unify that will be used during the unification - */ - protected IUnify stdUnify = new MartelliMontanariUnify(); - - /** - * The implementation of the rules that will be used during the unification. - */ - protected IRuleSet rules = new RuleSet(); - - /** - * Computes all principal type unifiers for a set of constraints. - * @param eq The set of constraints - * @param fc The finite closure - * @return The set of all principal type unifiers - */ - public Set> unify(Set eq, IFiniteClosure fc) { - /* - * Step 1: Repeated application of reduce, adapt, erase, swap - */ - Set eq0 = applyTypeUnificationRules(eq, fc); - - /* - * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs - */ - Set eq1s = new HashSet<>(); - Set eq2s = new HashSet<>(); - splitEq(eq0, eq1s, eq2s); - - /* - * Step 4: Create possible typings - * - * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) - * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia - */ - - // There are up to 10 toplevel set. 8 of 10 are the result of the - // cartesian product of the sets created by pattern matching. - List>> topLevelSets = new ArrayList<>(); - - if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. - Set> wrap = new HashSet<>(); - wrap.add(eq1s); - topLevelSets.add(wrap); // Add Eq1' - } - - // Add the set of [a =. Theta | (a=. Theta) in Eq2'] - Set bufferSet = eq2s.stream() - .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) - .collect(Collectors.toSet()); - - if(bufferSet.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. - Set> wrap = new HashSet<>(); - wrap.add(bufferSet); - topLevelSets.add(wrap); - eq2s.removeAll(bufferSet); - } - - // Sets that originate from pair pattern matching - // Sets of the "second level" - Set undefinedPairs = new HashSet<>(); - Set>>> secondLevelSets = calculatePairSets(eq2s, fc, undefinedPairs); - - // If pairs occured that did not match one of the cartesian product cases, - // those pairs are contradictory and the unification is impossible. - if(!undefinedPairs.isEmpty()) - return new HashSet<>(); - - /* Up to here, no cartesian products are calculated. - * filters for pairs and sets can be applied here */ - - // Sub cartesian products of the second level (pattern matched) sets - // "the big (x)" - // TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich (scheint sich nicht zu lohnen) - for(Set>> secondLevelSet : secondLevelSets) { - List>> secondLevelSetList = new ArrayList<>(secondLevelSet); - Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); - - // Flatten and add to top level sets - Set> flat = new HashSet<>(); - for(List> s : cartResult) { - Set flat1 = new HashSet<>(); - for(Set s1 : s) - flat1.addAll(s1); - flat.add(flat1); - } - topLevelSets.add(flat); - } - - // Cartesian product over all (up to 10) top level sets - Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) - .stream().map(x -> new HashSet<>(x)) - .collect(Collectors.toCollection(HashSet::new)); - //System.out.println(result); - - Set> eqPrimePrimeSet = new HashSet<>(); - - // TODO parallelisierung möglich (scheint sich nicht zu lohnen) - /* - * Die Parallelisierung über parallelStream() ist langsamer als die serielle Ausführung, - * vermutlich wird zuviel thread-overhead erzeugt. - * Vermutlich ist die beste Lösung hier ein Fork-Join-Framework. - */ - for(Set> setToFlatten : eqPrimeSet) { - // Flatten the cartesian product - Set eqPrime = new HashSet<>(); - setToFlatten.stream().forEach(x -> eqPrime.addAll(x)); - - /* - * Step 5: Substitution - */ - Optional> eqPrimePrime = rules.subst(eqPrime); - - - /* - * Step 6 a) Restart for pairs where subst was applied - * b) Build the union over everything - */ - if (eqPrime.equals(eq)) - eqPrimePrimeSet.add(eqPrime); - else if(eqPrimePrime.isPresent()) - eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc)); - else - eqPrimePrimeSet.addAll(this.unify(eqPrime, fc)); - } - - /* - * Step 7: Filter empty sets; - */ - return eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x)).collect(Collectors.toCollection(HashSet::new)); - - } - - /** - * Checks whether a set of pairs is in solved form. - * @param eqPrimePrime The set of pair - * @return True if in solved form, false otherwise. - */ - protected boolean isSolvedForm(Set eqPrimePrime) { - for(UnifyPair pair : eqPrimePrime) { - UnifyType lhsType = pair.getLhsType(); - UnifyType rhsType = pair.getRhsType(); - - if(!(lhsType instanceof PlaceholderType)) - return false; - - // If operator is not equals, both sides must be placeholders - if(pair.getPairOp() != PairOperator.EQUALSDOT && !(rhsType instanceof PlaceholderType)) - return false; - } - return true; - } - - /** - * Repeatedly applies type unification rules to a set of equations. - * 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) { - - /* - * Rule Application Strategy: - * - * 1. Swap all pairs and erase all erasable pairs - * 2. Apply all possible rules to a single pair, then move it to the result set. - * Iterating over pairs first, then iterating over rules prevents the application - * of rules to a "finished" pair over and over. - * 2.1 Apply all rules repeatedly except for erase rules. If - * the application of a rule creates new pairs, check immediately - * against the erase rules. - */ - - - LinkedHashSet targetSet = new LinkedHashSet(); - LinkedList eqQueue = new LinkedList<>(); - - /* - * Swap all pairs and erase all erasable pairs - */ - eq.forEach(x -> swapAddOrErase(x, fc, eqQueue)); - - /* - * Apply rules until the queue is empty - */ - while(!eqQueue.isEmpty()) { - UnifyPair pair = eqQueue.pollFirst(); - - // ReduceUp, ReduceLow, ReduceUpLow - Optional opt = rules.reduceUpLow(pair); - opt = opt.isPresent() ? opt : rules.reduceLow(pair); - opt = opt.isPresent() ? opt : rules.reduceUp(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardLow(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardLowRight(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardUp(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardUpRight(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair); - opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair); - - // Reduce TPH - opt = opt.isPresent() ? opt : rules.reduceTph(pair); - - // One of the rules has been applied - if(opt.isPresent()) { - swapAddOrErase(opt.get(), fc, eqQueue); - continue; - } - - // Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq - Optional> optSet = rules.reduce1(pair, fc); - optSet = optSet.isPresent() ? optSet : rules.reduce2(pair); - optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc); - optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc); - optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair); - - // ReduceTphExt, ReduceTphSup - optSet = optSet.isPresent() ? optSet : rules.reduceTphExt(pair); - optSet = optSet.isPresent() ? optSet : rules.reduceTphSup(pair); - - // One of the rules has been applied - if(optSet.isPresent()) { - optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue)); - continue; - } - - // Adapt, AdaptExt, AdaptSup - opt = rules.adapt(pair, fc); - opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc); - opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc); - - // One of the rules has been applied - if(opt.isPresent()) { - swapAddOrErase(opt.get(), fc, eqQueue); - continue; - } - - // None of the rules has been applied - targetSet.add(pair); - } - - return targetSet; - } - - /** - * Applies the rule swap to a pair if possible. Then adds the pair to the set if no erase rule applies. - * If an erase rule applies, the pair is not added (erased). - * @param pair The pair to swap and add or erase. - * @param collection The collection to which the pairs are added. - */ - protected void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection collection) { - Optional opt = rules.swap(pair); - UnifyPair pair2 = opt.isPresent() ? opt.get() : pair; - - if(rules.erase1(pair2, fc) || rules.erase3(pair2) || rules.erase2(pair2, fc)) - return; - - collection.add(pair2); - } - - /** - * Splits the equation eq into a set eq1s where both terms are type variables, - * and a set eq2s where one of both terms is not a type variable. - * @param eq Set of pairs to be splitted. - * @param eq1s Subset of eq where both terms are type variables. - * @param eq2s eq/eq1s. - */ - protected void splitEq(Set eq, Set eq1s, Set eq2s) { - for(UnifyPair pair : eq) - if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType) - eq1s.add(pair); - else - eq2s.add(pair); - } - - /** - * Creates sets of pairs specified in the fourth step. Does not calculate cartesian products. - * @param undefined All pairs that did not match one of the 8 cases are added to this set. - * @return The set of the eight cases (without empty sets). Each case is a set, containing sets generated - * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements - * (as in case 1 where sigma is added to the innermost set). - */ - protected Set>>> calculatePairSets(Set eq2s, IFiniteClosure fc, Set undefined) { - List>>> result = new ArrayList<>(8); - - // Init all 8 cases - for(int i = 0; i < 8; i++) - result.add(new HashSet<>()); - - for(UnifyPair pair : eq2s) { - PairOperator pairOp = pair.getPairOp(); - UnifyType lhsType = pair.getLhsType(); - UnifyType rhsType = pair.getRhsType(); - - // Case 1: (a <. Theta') - if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) - result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); - - // Case 2: (a <.? ? ext Theta') - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) - result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); - - // Case 3: (a <.? ? sup Theta') - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) - result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); - - // Case 4 was replaced by an inference rule - // Case 4: (a <.? Theta') - //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) - // result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); - - // Case 5: (Theta <. a) - else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) - result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); - - // Case 6 was replaced by an inference rule. - // Case 6: (? ext Theta <.? a) - //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) - // result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); - - // Case 7 was replaced by an inference rule - // Case 7: (? sup Theta <.? a) - //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) - // result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); - - // Case 8: (Theta <.? a) - else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) - result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); - // Case unknown: If a pair fits no other case, then the type unification has failed. - // Through application of the rules, every pair should have one of the above forms. - // Pairs that do not have one of the aboves form are contradictory. - else - undefined.add(pair); - } - - // Filter empty sets or sets that only contain an empty set. - return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new))) - .filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); - } - - /** - * Cartesian product Case 1: (a <. Theta') - */ - protected Set> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { - Set> result = new HashSet<>(); - - 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 = stdUnify.unify(tqp, thetaPrime); - if (!opt.isPresent()) - continue; - - Unifier unifier = opt.get(); - unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams()); - Set substitutionSet = new HashSet<>(); - for (Entry sigma : unifier) - 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<>(); - - 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); - } - } - - } - } - - return result; - } - - /** - * Cartesian Product Case 2: (a <.? ? ext Theta') - */ - protected Set> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) { - Set> result = new HashSet<>(); - - UnifyType aPrime = PlaceholderType.freshPlaceholder(); - UnifyType extAPrime = new ExtendsType(aPrime); - UnifyType thetaPrime = extThetaPrime.getExtendedType(); - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT)); - 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; - } - - /** - * Cartesian Product Case 3: (a <.? ? sup Theta') - */ - protected Set> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) { - Set> result = new HashSet<>(); - - UnifyType aPrime = PlaceholderType.freshPlaceholder(); - UnifyType supAPrime = new SuperType(aPrime); - UnifyType thetaPrime = subThetaPrime.getSuperedType(); - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT)); - result.add(resultPrime); - - resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT)); - resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT)); - result.add(resultPrime); - - return result; - } - - /** - * Cartesian Product Case 4: (a <.? Theta') - */ - protected Set> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { - Set> result = new HashSet<>(); - Set resultPrime = new HashSet<>(); - resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.EQUALSDOT)); - result.add(resultPrime); - - return result; - } - - /** - * Cartesian Product Case 5: (Theta <. a) - */ - protected Set> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) { - Set> result = new HashSet<>(); - for(UnifyType thetaS : fc.greater(theta)) { - Set resultPrime = new HashSet<>(); - - 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); - } - - return result; - } - - /** - * Cartesian Product Case 6: (? ext Theta <.? a) - */ - protected Set> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) { - Set> result = new HashSet<>(); - 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; - } - - /** - * Cartesian Product Case 7: (? sup Theta <.? a) - */ - protected Set> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) { - Set> result = new HashSet<>(); - - UnifyType aPrime = PlaceholderType.freshPlaceholder(); - UnifyType supAPrime = new SuperType(aPrime); - UnifyType theta = supTheta.getSuperedType(); - 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; - } - - /** - * Cartesian Product Case 8: (Theta <.? a) - */ - 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, 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; - } - - /** - * Takes a set of candidates for each position and computes all possible permutations. - * @param candidates The length of the list determines the number of type params. Each set - * contains the candidates for the corresponding position. - */ - protected Set permuteParams(ArrayList> candidates) { - Set result = new HashSet<>(); - permuteParams(candidates, 0, result, new UnifyType[candidates.size()]); - return result; - } - - /** - * Takes a set of candidates for each position and computes all possible permutations. - * @param candidates The length of the list determines the number of type params. Each set - * contains the candidates for the corresponding position. - * @param idx Idx for the current permutatiton. - * @param result Set of all permutations found so far - * @param current The permutation of type params that is currently explored - */ - private void permuteParams(ArrayList> candidates, int idx, Set result, UnifyType[] current) { - if(candidates.size() == idx) { - result.add(new TypeParams(Arrays.copyOf(current, current.length))); - return; - } - - Set localCandidates = candidates.get(idx); - - for(UnifyType t : localCandidates) { - current[idx] = t; - permuteParams(candidates, idx+1, result, current); - } + public Set> unify(Set eq, IFiniteClosure fc) { + TypeUnifyTask unifyTask = new TypeUnifyTask(eq, fc); + ForkJoinPool pool = new ForkJoinPool(); + pool.invoke(unifyTask); + return unifyTask.join(); } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java new file mode 100644 index 00000000..8254caf1 --- /dev/null +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -0,0 +1,631 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Map.Entry; +import java.util.Optional; +import java.util.Set; +import java.util.concurrent.RecursiveTask; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; +import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +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 type unification algorithm + * @author Florian Steurer + */ +public class TypeUnifyTask extends RecursiveTask>> { + + /** + * The implementation of setOps that will be used during the unification + */ + protected ISetOperations setOps = new GuavaSetOperations(); + + /** + * The implementation of the standard unify that will be used during the unification + */ + protected IUnify stdUnify = new MartelliMontanariUnify(); + + /** + * The implementation of the rules that will be used during the unification. + */ + protected IRuleSet rules = new RuleSet(); + + protected Set eq; + + protected IFiniteClosure fc; + + public TypeUnifyTask(Set eq, IFiniteClosure fc) { + this.eq = eq; + this.fc = fc; + } + + @Override + protected Set> compute() { + return unify(eq, fc); + } + + /** + * Computes all principal type unifiers for a set of constraints. + * @param eq The set of constraints + * @param fc The finite closure + * @return The set of all principal type unifiers + */ + public Set> unify(Set eq, IFiniteClosure fc) { + /* + * Step 1: Repeated application of reduce, adapt, erase, swap + */ + Set eq0 = applyTypeUnificationRules(eq, fc); + + /* + * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs + */ + Set eq1s = new HashSet<>(); + Set eq2s = new HashSet<>(); + splitEq(eq0, eq1s, eq2s); + + /* + * Step 4: Create possible typings + * + * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) + * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia + */ + + // There are up to 10 toplevel set. 8 of 10 are the result of the + // cartesian product of the sets created by pattern matching. + List>> topLevelSets = new ArrayList<>(); + + if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. + Set> wrap = new HashSet<>(); + wrap.add(eq1s); + topLevelSets.add(wrap); // Add Eq1' + } + + // Add the set of [a =. Theta | (a=. Theta) in Eq2'] + Set bufferSet = eq2s.stream() + .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) + .collect(Collectors.toSet()); + + if(bufferSet.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. + Set> wrap = new HashSet<>(); + wrap.add(bufferSet); + topLevelSets.add(wrap); + eq2s.removeAll(bufferSet); + } + + // Sets that originate from pair pattern matching + // Sets of the "second level" + Set undefinedPairs = new HashSet<>(); + Set>>> secondLevelSets = calculatePairSets(eq2s, fc, undefinedPairs); + + // If pairs occured that did not match one of the cartesian product cases, + // those pairs are contradictory and the unification is impossible. + if(!undefinedPairs.isEmpty()) + return new HashSet<>(); + + /* Up to here, no cartesian products are calculated. + * filters for pairs and sets can be applied here */ + + // Sub cartesian products of the second level (pattern matched) sets + // "the big (x)" + for(Set>> secondLevelSet : secondLevelSets) { + List>> secondLevelSetList = new ArrayList<>(secondLevelSet); + Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); + + // Flatten and add to top level sets + Set> flat = new HashSet<>(); + for(List> s : cartResult) { + Set flat1 = new HashSet<>(); + for(Set s1 : s) + flat1.addAll(s1); + flat.add(flat1); + } + topLevelSets.add(flat); + } + + // Cartesian product over all (up to 10) top level sets + Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) + .stream().map(x -> new HashSet<>(x)) + .collect(Collectors.toCollection(HashSet::new)); + //System.out.println(result); + + Set> eqPrimePrimeSet = new HashSet<>(); + + Set forks = new HashSet<>(); + for(Set> setToFlatten : eqPrimeSet) { + // Flatten the cartesian product + Set eqPrime = new HashSet<>(); + setToFlatten.stream().forEach(x -> eqPrime.addAll(x)); + + /* + * Step 5: Substitution + */ + Optional> eqPrimePrime = rules.subst(eqPrime); + + + /* + * Step 6 a) Restart (fork) for pairs where subst was applied + */ + Set restart = new HashSet<>(); + + if (eqPrime.equals(eq)) + eqPrimePrimeSet.add(eqPrime); + else if(eqPrimePrime.isPresent()) { + TypeUnifyTask fork = new TypeUnifyTask(eqPrimePrime.get(), fc); + forks.add(fork); + fork.fork(); + } + //eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc)); + else { + TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc); + forks.add(fork); + fork.fork(); + // eqPrimePrimeSet.addAll(this.unify(eqPrime, fc)); + } + } + + /* + * Step 6 b) Build the union over everything. + */ + + // TODO Parallel stream und synced set? + for(TypeUnifyTask fork : forks) + eqPrimePrimeSet.addAll(fork.join()); + + /* + * Step 7: Filter empty sets; + */ + return eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x)).collect(Collectors.toCollection(HashSet::new)); + + } + + /** + * Checks whether a set of pairs is in solved form. + * @param eqPrimePrime The set of pair + * @return True if in solved form, false otherwise. + */ + protected boolean isSolvedForm(Set eqPrimePrime) { + for(UnifyPair pair : eqPrimePrime) { + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + if(!(lhsType instanceof PlaceholderType)) + return false; + + // If operator is not equals, both sides must be placeholders + if(pair.getPairOp() != PairOperator.EQUALSDOT && !(rhsType instanceof PlaceholderType)) + return false; + } + return true; + } + + /** + * Repeatedly applies type unification rules to a set of equations. + * 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) { + + /* + * Rule Application Strategy: + * + * 1. Swap all pairs and erase all erasable pairs + * 2. Apply all possible rules to a single pair, then move it to the result set. + * Iterating over pairs first, then iterating over rules prevents the application + * of rules to a "finished" pair over and over. + * 2.1 Apply all rules repeatedly except for erase rules. If + * the application of a rule creates new pairs, check immediately + * against the erase rules. + */ + + + LinkedHashSet targetSet = new LinkedHashSet(); + LinkedList eqQueue = new LinkedList<>(); + + /* + * Swap all pairs and erase all erasable pairs + */ + eq.forEach(x -> swapAddOrErase(x, fc, eqQueue)); + + /* + * Apply rules until the queue is empty + */ + while(!eqQueue.isEmpty()) { + UnifyPair pair = eqQueue.pollFirst(); + + // ReduceUp, ReduceLow, ReduceUpLow + Optional opt = rules.reduceUpLow(pair); + opt = opt.isPresent() ? opt : rules.reduceLow(pair); + opt = opt.isPresent() ? opt : rules.reduceUp(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLow(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLowRight(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardUp(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardUpRight(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair); + + // Reduce TPH + opt = opt.isPresent() ? opt : rules.reduceTph(pair); + + // One of the rules has been applied + if(opt.isPresent()) { + swapAddOrErase(opt.get(), fc, eqQueue); + continue; + } + + // Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq + Optional> optSet = rules.reduce1(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduce2(pair); + optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair); + + // ReduceTphExt, ReduceTphSup + optSet = optSet.isPresent() ? optSet : rules.reduceTphExt(pair); + optSet = optSet.isPresent() ? optSet : rules.reduceTphSup(pair); + + // One of the rules has been applied + if(optSet.isPresent()) { + optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue)); + continue; + } + + // Adapt, AdaptExt, AdaptSup + opt = rules.adapt(pair, fc); + opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc); + opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc); + + // One of the rules has been applied + if(opt.isPresent()) { + swapAddOrErase(opt.get(), fc, eqQueue); + continue; + } + + // None of the rules has been applied + targetSet.add(pair); + } + + return targetSet; + } + + /** + * Applies the rule swap to a pair if possible. Then adds the pair to the set if no erase rule applies. + * If an erase rule applies, the pair is not added (erased). + * @param pair The pair to swap and add or erase. + * @param collection The collection to which the pairs are added. + */ + protected void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection collection) { + Optional opt = rules.swap(pair); + UnifyPair pair2 = opt.isPresent() ? opt.get() : pair; + + if(rules.erase1(pair2, fc) || rules.erase3(pair2) || rules.erase2(pair2, fc)) + return; + + collection.add(pair2); + } + + /** + * Splits the equation eq into a set eq1s where both terms are type variables, + * and a set eq2s where one of both terms is not a type variable. + * @param eq Set of pairs to be splitted. + * @param eq1s Subset of eq where both terms are type variables. + * @param eq2s eq/eq1s. + */ + protected void splitEq(Set eq, Set eq1s, Set eq2s) { + for(UnifyPair pair : eq) + if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType) + eq1s.add(pair); + else + eq2s.add(pair); + } + + /** + * Creates sets of pairs specified in the fourth step. Does not calculate cartesian products. + * @param undefined All pairs that did not match one of the 8 cases are added to this set. + * @return The set of the eight cases (without empty sets). Each case is a set, containing sets generated + * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements + * (as in case 1 where sigma is added to the innermost set). + */ + protected Set>>> calculatePairSets(Set eq2s, IFiniteClosure fc, Set undefined) { + List>>> result = new ArrayList<>(8); + + // Init all 8 cases + for(int i = 0; i < 8; i++) + result.add(new HashSet<>()); + + for(UnifyPair pair : eq2s) { + PairOperator pairOp = pair.getPairOp(); + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + // Case 1: (a <. Theta') + if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) + result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); + + // Case 2: (a <.? ? ext Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) + result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); + + // Case 3: (a <.? ? sup Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) + result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); + + // Case 4 was replaced by an inference rule + // Case 4: (a <.? Theta') + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) + // result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); + + // Case 5: (Theta <. a) + else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) + result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); + + // Case 6 was replaced by an inference rule. + // Case 6: (? ext Theta <.? a) + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) + // result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); + + // Case 7 was replaced by an inference rule + // Case 7: (? sup Theta <.? a) + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) + // result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); + + // Case 8: (Theta <.? a) + else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) + result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); + // Case unknown: If a pair fits no other case, then the type unification has failed. + // Through application of the rules, every pair should have one of the above forms. + // Pairs that do not have one of the aboves form are contradictory. + else + undefined.add(pair); + } + + // Filter empty sets or sets that only contain an empty set. + return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new))) + .filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); + } + + /** + * Cartesian product Case 1: (a <. Theta') + */ + protected Set> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { + Set> result = new HashSet<>(); + + 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 = stdUnify.unify(tqp, thetaPrime); + if (!opt.isPresent()) + continue; + + Unifier unifier = opt.get(); + unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams()); + Set substitutionSet = new HashSet<>(); + for (Entry sigma : unifier) + 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<>(); + + 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); + } + } + + } + } + + return result; + } + + /** + * Cartesian Product Case 2: (a <.? ? ext Theta') + */ + protected Set> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) { + Set> result = new HashSet<>(); + + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + UnifyType extAPrime = new ExtendsType(aPrime); + UnifyType thetaPrime = extThetaPrime.getExtendedType(); + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT)); + 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; + } + + /** + * Cartesian Product Case 3: (a <.? ? sup Theta') + */ + protected Set> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) { + Set> result = new HashSet<>(); + + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + UnifyType supAPrime = new SuperType(aPrime); + UnifyType thetaPrime = subThetaPrime.getSuperedType(); + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT)); + result.add(resultPrime); + + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT)); + resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT)); + result.add(resultPrime); + + return result; + } + + /** + * Cartesian Product Case 4: (a <.? Theta') + */ + protected Set> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { + Set> result = new HashSet<>(); + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.EQUALSDOT)); + result.add(resultPrime); + + return result; + } + + /** + * Cartesian Product Case 5: (Theta <. a) + */ + protected Set> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) { + Set> result = new HashSet<>(); + for(UnifyType thetaS : fc.greater(theta)) { + Set resultPrime = new HashSet<>(); + + 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); + } + + return result; + } + + /** + * Cartesian Product Case 6: (? ext Theta <.? a) + */ + protected Set> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) { + Set> result = new HashSet<>(); + 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; + } + + /** + * Cartesian Product Case 7: (? sup Theta <.? a) + */ + protected Set> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) { + Set> result = new HashSet<>(); + + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + UnifyType supAPrime = new SuperType(aPrime); + UnifyType theta = supTheta.getSuperedType(); + 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; + } + + /** + * Cartesian Product Case 8: (Theta <.? a) + */ + 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, 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; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + */ + protected Set permuteParams(ArrayList> candidates) { + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new UnifyType[candidates.size()]); + return result; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + * @param idx Idx for the current permutatiton. + * @param result Set of all permutations found so far + * @param current The permutation of type params that is currently explored + */ + private void permuteParams(ArrayList> candidates, int idx, Set result, UnifyType[] current) { + if(candidates.size() == idx) { + result.add(new TypeParams(Arrays.copyOf(current, current.length))); + return; + } + + Set localCandidates = candidates.get(idx); + + for(UnifyType t : localCandidates) { + current[idx] = t; + permuteParams(candidates, idx+1, result, current); + } + } +} diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index af6e044f..45551710 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -17,7 +17,7 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType; import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import junit.framework.Assert; -public class UnifyTest extends TypeUnify { +public class UnifyTest extends TypeUnify{ /** * Testing the unification for cases with (n)one pair and without generics. @@ -792,52 +792,52 @@ public class UnifyTest extends TypeUnify { } - @Test - public void permuteParamsTest() { - TypeFactory tf = new TypeFactory(); - ArrayList> candidates = new ArrayList<>(); - - UnifyType p11 = tf.getPlaceholderType("p11"); - UnifyType p12 = tf.getExtendsType(tf.getSimpleType("p12")); - UnifyType p13 = tf.getSimpleType("p13"); - UnifyType p21 = tf.getPlaceholderType("p21"); - UnifyType p22 = tf.getPlaceholderType("p22"); - UnifyType p31 = tf.getSimpleType("p31", "T"); - - Set p1 = new HashSet<>(); - p1.add(p11); - p1.add(p12); - p1.add(p13); - - Set p2 = new HashSet<>(); - p2.add(p21); - p2.add(p22); - - Set p3 = new HashSet<>(); - p3.add(p31); - - candidates.add(p1); - candidates.add(p2); - candidates.add(p3); - - - /* - * Expected Result: - * { | x in { p11, p12, p13}, y in { p21, p22 }, z in { p31 }} - */ - Set expected = Arrays.stream(new TypeParams[] { - new TypeParams(p11, p21, p31), - new TypeParams(p11, p22, p31), - new TypeParams(p12, p21, p31), - new TypeParams(p12, p22, p31), - new TypeParams(p13, p21, p31), - new TypeParams(p13, p22, p31) - }).collect(Collectors.toSet()); - - Set actual = permuteParams(candidates); - - Assert.assertEquals(expected, actual); - } +// @Test +// public void permuteParamsTest() { +// TypeFactory tf = new TypeFactory(); +// ArrayList> candidates = new ArrayList<>(); +// +// UnifyType p11 = tf.getPlaceholderType("p11"); +// UnifyType p12 = tf.getExtendsType(tf.getSimpleType("p12")); +// UnifyType p13 = tf.getSimpleType("p13"); +// UnifyType p21 = tf.getPlaceholderType("p21"); +// UnifyType p22 = tf.getPlaceholderType("p22"); +// UnifyType p31 = tf.getSimpleType("p31", "T"); +// +// Set p1 = new HashSet<>(); +// p1.add(p11); +// p1.add(p12); +// p1.add(p13); +// +// Set p2 = new HashSet<>(); +// p2.add(p21); +// p2.add(p22); +// +// Set p3 = new HashSet<>(); +// p3.add(p31); +// +// candidates.add(p1); +// candidates.add(p2); +// candidates.add(p3); +// +// +// /* +// * Expected Result: +// * { | x in { p11, p12, p13}, y in { p21, p22 }, z in { p31 }} +// */ +// Set expected = Arrays.stream(new TypeParams[] { +// new TypeParams(p11, p21, p31), +// new TypeParams(p11, p22, p31), +// new TypeParams(p12, p21, p31), +// new TypeParams(p12, p22, p31), +// new TypeParams(p13, p21, p31), +// new TypeParams(p13, p22, p31) +// }).collect(Collectors.toSet()); +// +// Set actual = permuteParams(candidates); +// +// Assert.assertEquals(expected, actual); +// } private Set> filterGeneratedTPHsMultiple(Set> set) { return set.stream().map(x -> filterGeneratedTPHs(x)).collect(Collectors.toSet()); From 856f5da86bf1192ee24c7abeeec820c6ec5babcd Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Fri, 22 Apr 2016 16:52:16 +0200 Subject: [PATCH 8/8] Parallelisierung mit Fork-Join Pool --- .../dhbwstuttgart/typeinference/unify/TypeUnifyTask.java | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 8254caf1..c4d49693 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -32,7 +32,9 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType; * @author Florian Steurer */ public class TypeUnifyTask extends RecursiveTask>> { - + + private static final long serialVersionUID = 1L; + /** * The implementation of setOps that will be used during the unification */ @@ -163,8 +165,6 @@ public class TypeUnifyTask extends RecursiveTask>> { /* * Step 6 a) Restart (fork) for pairs where subst was applied */ - Set restart = new HashSet<>(); - if (eqPrime.equals(eq)) eqPrimePrimeSet.add(eqPrime); else if(eqPrimePrime.isPresent()) { @@ -172,12 +172,10 @@ public class TypeUnifyTask extends RecursiveTask>> { forks.add(fork); fork.fork(); } - //eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc)); else { TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc); forks.add(fork); fork.fork(); - // eqPrimePrimeSet.addAll(this.unify(eqPrime, fc)); } }