diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java index da59af1a..9fb3e454 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java @@ -35,6 +35,11 @@ public final class ExtendsType extends Type { public TypeParams getTypeParams() { return extendedType.getTypeParams(); } + + @Override + public Type setTypeParams(TypeParams newTp) { + return new ExtendsType(extendedType.setTypeParams(newTp)); + } @Override Set smArg(IFiniteClosure fc) { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java index e1f1697a..5a3d5341 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java @@ -20,6 +20,11 @@ public final class PlaceholderType extends Type{ return fc.grArg(this); } + @Override + public Type setTypeParams(TypeParams newTp) { + return this; + } + @Override public int hashCode() { return typeName.hashCode(); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java index 1283ceb6..ef01652a 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java @@ -28,6 +28,11 @@ public final class SimpleType extends Type { return new SimpleType(typeName, typeParams.apply(unif)); } + @Override + public Type setTypeParams(TypeParams newTp) { + return new SimpleType(new String(typeName), newTp); + } + @Override public int hashCode() { return typeName.hashCode(); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java index 7090d86a..2503e748 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -27,6 +27,11 @@ public final class SuperType extends Type { return superedType.getTypeParams(); } + @Override + public Type setTypeParams(TypeParams newTp) { + return new SuperType(superedType.setTypeParams(newTp)); + } + @Override Set smArg(IFiniteClosure fc) { return fc.smArg(this); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Type.java b/src/de/dhbwstuttgart/typeinference/unify/model/Type.java index 52977fbf..3c179110 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Type.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Type.java @@ -27,6 +27,8 @@ public abstract class Type { return typeParams; } + public abstract Type setTypeParams(TypeParams newTp); + abstract Set smArg(IFiniteClosure fc); abstract Set grArg(IFiniteClosure fc); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java index e9c26e59..0a1fde25 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -2,6 +2,7 @@ package de.dhbwstuttgart.typeinference.unify.model; import java.util.HashMap; import java.util.Map.Entry; +import java.util.Set; import java.util.function.Function; public class Unifier implements Function { @@ -43,6 +44,10 @@ public class Unifier implements Function { public Type getSubstitute(Type t) { return substitutions.get(t); } + + public Set> getSubstitutions() { + return substitutions.entrySet(); + } @Override public String toString() { diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 6b05338b..548340b3 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -1,11 +1,13 @@ package de.dhbwstuttgart.typeinference.unifynew; 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; @@ -24,6 +26,7 @@ import de.dhbwstuttgart.typeinference.unify.model.SuperType; import de.dhbwstuttgart.typeinference.unify.model.Type; import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; import de.dhbwstuttgart.typeinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; /** @@ -225,48 +228,47 @@ public class Unify { // Case 1: (a <. Theta') if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) { + Type thetaPrime = pair.getRhsType(); + Set set = new HashSet<>(); IUnify unify = new MartelliMontanariUnify(); - Set possibleCs = fc.getAllTypes(rhsType.getName()); + //Set cs = fc.getAllTypes(rhsType.getName()); + Type c = rhsType; + //Set thetaQs = cs.stream().flatMap(x -> fc.smaller(x).stream()).collect(Collectors.toCollection(HashSet::new)); + Set thetaQs = fc.smaller(c); + Set thetaQPrimes = new HashSet<>(); + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + for(Type param : cParams) + candidateParams.add(fc.grArg(param)); + Set permutations = new HashSet(); + permuteParams(candidateParams, 0, permutations, new Type[candidateParams.size()]); + + for(TypeParams tp : permutations) + thetaQPrimes.add(c.setTypeParams(tp)); + } + for(Type tqp : thetaQPrimes) { + Optional opt = unify.unify(tqp, thetaPrime); + if(opt.isPresent()) { + Unifier unifier = opt.get(); + Set> substitutions = unifier.getSubstitutions(); + for(Entry sigma : substitutions) + set.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); + for(Type tq : thetaQs) { + Set smaller = fc.smaller(unifier.apply(tq)); + smaller.stream().map(x -> new MPair(lhsType, x, PairOperator.EQUALSDOT)).forEach(x -> set.add(x)); + } + } + } - /*IUnify unify = new MartelliMontanariUnify(); - - Set possibleCs = fc.getAllTypes(rhsType.getName()); - Set possibleThetas = possibleCs.stream() - .flatMap(x -> fc.smaller(x).stream()) - .collect(Collectors.toCollection(HashSet::new)); - Set possibleThetaPrimes = possibleThetas.stream() - .flatMap(x -> getAllInstantiations(x, fc).stream()) - .collect(Collectors.toCollection(HashSet::new)); - */ - // TODO - - /*Set unifiers = possibleThetaPrimes.stream() - .map(x -> unify.unify(x, rhsType)) - .filter(x -> x.isPresent()) - .flatMap(x -> x.get().stream()) - .map(x -> new Unifier(x.getLhsType(), x.getRhsType())) - .collect(Collectors.toCollection(HashSet::new)); - - Set thetas = new HashSet<>(); - - for(Unifier sigma : unifiers) - for(Type thetaQuer : possibleThetas) - thetas.addAll(fc.smaller(sigma.apply(thetaQuer))); - - Set resultSet = new HashSet<>(); - thetas.forEach(x -> resultSet.add(new MPair(lhsType, x, PairOperator.EQUALSDOT))); - unifiers.forEach(x -> resultSet.add(new MPair(x.getSource(), x.getTarget(), PairOperator.EQUALSDOT))); - - result.add(resultSet); - // TODO Speedup - Potenzial durch auschließen unmöglicher kombinationen (z.B. wenn in theta' eine Variable festgelegt ist) - // TODO speedup durch pipelining mit streams - // TODO speedup teure berechnungen mit proxy rauszögern - */ + result.add(set); } // Case 2: (a <.? ? ext Theta') @@ -285,7 +287,7 @@ public class Unify { // 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)); + set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT)); result.add(set); } @@ -322,6 +324,20 @@ public class Unify { return result; } + protected void permuteParams(ArrayList> candidates, int idx, Set result, Type[] current) { + if(candidates.size() == idx) { + result.add(new TypeParams(Arrays.copyOf(current, current.length))); + return; + } + + Set localCandidates = candidates.get(idx); + + for(Type t : localCandidates) { + current[idx] = t; + permuteParams(candidates, idx+1, result, current); + } + } + private Set getAllInstantiations(Type t, IFiniteClosure fc) { Set result = new HashSet<>(); result.add(t); diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index be759f6e..51e178f4 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -1,5 +1,6 @@ package unify; +import java.util.ArrayList; import java.util.HashSet; import java.util.Set; @@ -8,6 +9,8 @@ import org.junit.Test; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.model.MPair; import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import de.dhbwstuttgart.typeinference.unifynew.Unify; public class UnifyTest extends Unify { @@ -21,6 +24,7 @@ public class UnifyTest extends Unify { //fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object")); fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number")); fcb.add(tf.getSimpleType("Double"), tf.getSimpleType("Number")); + //fcb.add(tf.getSimpleType("List", "T")); IFiniteClosure fc = fcb.getCollectionExample(); @@ -31,9 +35,9 @@ public class UnifyTest extends Unify { // Double <. B // B <. Object eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); - //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("Integer"), PairOperator.SMALLERDOT)); + eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", tf.getSimpleType("Number")), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT)); @@ -53,4 +57,32 @@ public class UnifyTest extends Unify { } + @Test + public void permuteParamsTest() { + TypeFactory tf = new TypeFactory(); + ArrayList> candidates = new ArrayList<>(); + + Set p1 = new HashSet<>(); + p1.add(tf.getPlaceholderType("p11")); + p1.add(tf.getExtendsType(tf.getSimpleType("p12"))); + p1.add(tf.getSimpleType("p13")); + + Set p2 = new HashSet<>(); + p2.add(tf.getPlaceholderType("p21")); + p2.add(tf.getPlaceholderType("p22")); + + Set p3 = new HashSet<>(); + p3.add(tf.getSimpleType("p31", "T")); + p3.add(tf.getSimpleType("p32")); + + candidates.add(p1); + candidates.add(p2); + candidates.add(p3); + + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new Type[candidates.size()]); + + System.out.println(result); + } + }