From d19a79bd6394cc5726f9cd9e7e8a9391c9a8d27a Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Wed, 16 Mar 2016 23:27:45 +0100 Subject: [PATCH 1/4] finite closure greater smaller funktioniert jetzt auch mit wildcards (muss noch getestet werden) --- .../unify/model/FiniteClosure.java | 69 ++++++++++++++++--- test/unify/FiniteClosureTest.java | 10 +-- 2 files changed, 66 insertions(+), 13 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index e618482d..977f36ee 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -1,5 +1,7 @@ package de.dhbwstuttgart.typeinference.unify.model; +import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; import java.util.HashSet; import java.util.Optional; @@ -57,12 +59,30 @@ public class FiniteClosure implements IFiniteClosure { */ @Override public Set smaller(Type type) { - if(!inheritanceGraph.containsKey(type)) - return new HashSet<>(); - - Set result = inheritanceGraph.get(type).getContentOfDescendants(); + Set result = inheritanceGraph.containsKey(type) ? inheritanceGraph.get(type).getContentOfDescendants() : new HashSet<>(); result.add(type); + if(type.getTypeParams().size() == 0) + return result; + + ArrayList> paramCandidates = new ArrayList<>(); + for(Type param : type.getTypeParams()) { + if(param instanceof ExtendsType || param instanceof SuperType) { + Set pc = param.smArg(this); + paramCandidates.add(pc); + } else { + HashSet pc = new HashSet<>(); + pc.add(param); + paramCandidates.add(pc); + } + } + + Set permResult = new HashSet<>(); + permuteParams(paramCandidates, 0, permResult, new Type[paramCandidates.size()]); + + for(TypeParams newParams : permResult) + result.add(type.setTypeParams(newParams)); + return result; } @@ -72,11 +92,30 @@ public class FiniteClosure implements IFiniteClosure { */ @Override public Set greater(Type type) { - if(!inheritanceGraph.containsKey(type)) - return new HashSet<>(); - - Set result = inheritanceGraph.get(type).getContentOfPredecessors(); + Set result = inheritanceGraph.containsKey(type) ? inheritanceGraph.get(type).getContentOfPredecessors() : new HashSet<>(); result.add(type); + + if(type.getTypeParams().size() == 0) + return result; + + ArrayList> paramCandidates = new ArrayList<>(); + for(Type param : type.getTypeParams()) { + if(param instanceof ExtendsType || param instanceof SuperType) { + Set pc = param.grArg(this); + paramCandidates.add(pc); + } else { + HashSet pc = new HashSet<>(); + pc.add(param); + paramCandidates.add(pc); + } + } + + Set permResult = new HashSet<>(); + permuteParams(paramCandidates, 0, permResult, new Type[paramCandidates.size()]); + + for(TypeParams newParams : permResult) + result.add(type.setTypeParams(newParams)); + return result; } @@ -213,4 +252,18 @@ public class FiniteClosure implements IFiniteClosure { return new HashSet<>(); return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new)); } + + 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); + } + } } diff --git a/test/unify/FiniteClosureTest.java b/test/unify/FiniteClosureTest.java index 9b5c72e6..7b1b6664 100644 --- a/test/unify/FiniteClosureTest.java +++ b/test/unify/FiniteClosureTest.java @@ -1,15 +1,11 @@ package unify; -import java.util.HashSet; -import java.util.Set; - 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.unifynew.TypeFactory; -import de.dhbwstuttgart.typeinference.unify.model.Type; public class FiniteClosureTest { @@ -37,10 +33,14 @@ public class FiniteClosureTest { @Test public void testSmaller() { - IFiniteClosure fc = new FiniteClosureBuilder().getCollectionExample(); + FiniteClosureBuilder fcb = new FiniteClosureBuilder(); TypeFactory tf = new TypeFactory(); + fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number")); + IFiniteClosure fc = fcb.getCollectionExample(); + System.out.println("\n\n----- Smaller Test -----"); + System.out.println("Smaller(List) = " + fc.smaller(tf.getSimpleType("List", tf.getExtendsType(tf.getSimpleType("Number"))))); System.out.println("Smaller(List) = " + fc.smaller(tf.getSimpleType("List", "T"))); System.out.println("Smaller(TreeSet) = " + fc.smaller(tf.getSimpleType("TreeSet", "T"))); System.out.println("Smaller(Collection) = " + fc.smaller(tf.getSimpleType("Collection"))); From fa9627b8835580217217a74f0b128b00c9961b11 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Thu, 17 Mar 2016 16:35:33 +0100 Subject: [PATCH 2/4] unify case 1 --- .../unify/model/FiniteClosure.java | 4 ++ .../typeinference/unifynew/Unify.java | 61 ++++++++++--------- test/unify/UnifyTest.java | 2 +- 3 files changed, 36 insertions(+), 31 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 977f36ee..516d85fe 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -144,6 +144,7 @@ public class FiniteClosure implements IFiniteClosure { return new HashSet(); Set result = new HashSet(); + result.add(type); Type t = type.getExtendedType(); @@ -158,6 +159,7 @@ public class FiniteClosure implements IFiniteClosure { return new HashSet(); Set result = new HashSet(); + result.add(type); Type t = type.getSuperedType(); @@ -194,6 +196,7 @@ public class FiniteClosure implements IFiniteClosure { return new HashSet(); Set result = new HashSet(); + result.add(type); Type t = type.getExtendedType(); @@ -213,6 +216,7 @@ public class FiniteClosure implements IFiniteClosure { return new HashSet(); Set result = new HashSet(); + result.add(type); Type t = type.getSuperedType(); diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 548340b3..ce7e13c4 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -232,38 +232,39 @@ public class Unify { Set set = new HashSet<>(); IUnify unify = new MartelliMontanariUnify(); - //Set cs = fc.getAllTypes(rhsType.getName()); - Type c = rhsType; + Set cs = fc.getAllTypes(rhsType.getName()); - //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()]); + Set thetaQs = cs.stream().flatMap( + x -> fc.smaller(x).stream().filter(y -> y.getTypeParams().arePlaceholders()) + ).collect(Collectors.toCollection(HashSet::new)); + + for(Type c : cs) { + 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(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)); + 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)); + } } } } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 8524c1dc..1b120dae 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -38,7 +38,7 @@ public class UnifyTest extends Unify { 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("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", tf.getSimpleType("Number")), PairOperator.SMALLERDOT)); + eq.add(new MPair(tf.getPlaceholderType("A"), 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)); From 299f8f56cada9e6c1744a16c8a1dd9647905c2a9 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Sun, 20 Mar 2016 15:09:12 +0100 Subject: [PATCH 3/4] added missing cases --- .../unify/interfaces/IFiniteClosure.java | 2 +- .../unify/model/FiniteClosure.java | 71 ++++- .../typeinference/unify/model/Unifier.java | 2 +- .../unifynew/MartelliMontanariUnify.java | 6 +- .../typeinference/unifynew/Unify.java | 278 +++++++++++++----- test/unify/FiniteClosureTest.java | 28 +- test/unify/UnifyTest.java | 8 +- 7 files changed, 301 insertions(+), 94 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index 62b65b27..3af29411 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -50,5 +50,5 @@ public interface IFiniteClosure { public Set smArg(PlaceholderType type); public Optional getGenericType(String typeName); - public Set getAllTypes(String typeName); + public Set getAllTypesByName(String typeName); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 516d85fe..64fb6862 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -9,13 +9,19 @@ import java.util.Set; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify; public class FiniteClosure implements IFiniteClosure { private HashMap> inheritanceGraph; private HashMap>> strInheritanceGraph; + public FiniteClosure() { + + } + public FiniteClosure(Set pairs) { inheritanceGraph = new HashMap>(); @@ -52,16 +58,34 @@ public class FiniteClosure implements IFiniteClosure { strInheritanceGraph.get(key.getName()).add(inheritanceGraph.get(key)); } } - + /** * Returns all types of the finite closure that are subtypes of the argument. * @return The set of subtypes of the argument. */ @Override public Set smaller(Type type) { + // - if(T < T') then T <=* T' Set result = inheritanceGraph.containsKey(type) ? inheritanceGraph.get(type).getContentOfDescendants() : new HashSet<>(); result.add(type); + // if T1 <=* T2 then sigma1(T1) <=* sigma1(T2) + // where foreach type var a in T2: + // sigma1(T1) <=* sigma2(T2) + /*if(strInheritanceGraph.containsKey(type.getName())) { + IUnify unify = new MartelliMontanariUnify(); + HashSet> candidateNodes = strInheritanceGraph.get(type.getName()); + for(Node candidateNode : candidateNodes) { + Type theta2 = candidateNode.getContent(); + Optional sigma2 = unify.unify(theta2, type); + if(!sigma2.isPresent()) + continue; + for(Type sigma1theta1 : candidateNode.getContentOfDescendants()) { + Type theta1 = sigma2.get().apply(sigma1theta1); + } + } + }*/ + if(type.getTypeParams().size() == 0) return result; @@ -86,6 +110,37 @@ public class FiniteClosure implements IFiniteClosure { return result; } + /** + * @param t1 + * @param t2 + * @return + */ + protected Optional match(Type t1, Type t2) { + if(!t1.getName().equals(t2.getName())) + return Optional.empty(); + + TypeParams t1Params = t1.getTypeParams(); + TypeParams t2Params = t2.getTypeParams(); + + if(t1Params.size() != t2Params.size()) + return Optional.empty(); + + Unifier result = new Unifier(); + for(int i = 0; i < t1Params.size(); i++) { + Type t1i = t1Params.get(i); + Type t2i = t2Params.get(i); + + boolean equal = t1i.equals(t2i); + if(!equal && !(t2i instanceof PlaceholderType)) + return Optional.empty(); + + if(!equal && t2i instanceof PlaceholderType) + result.Add((PlaceholderType) t2i, t1i); + } + + return Optional.of(result); + } + /** * Returns all types of the finite closure that are supertypes of the argument. * @return The set of supertypes of the argument. @@ -170,7 +225,11 @@ public class FiniteClosure implements IFiniteClosure { @Override public Set grArg(PlaceholderType type) { - return new HashSet<>(); + HashSet result = new HashSet<>(); + result.add(type); + result.add(new SuperType(type)); + result.add(new ExtendsType(type)); + return result; } @Override @@ -231,7 +290,11 @@ public class FiniteClosure implements IFiniteClosure { @Override public Set smArg(PlaceholderType type) { - return new HashSet<>(); + HashSet result = new HashSet<>(); + result.add(type); + result.add(new SuperType(type)); + result.add(new ExtendsType(type)); + return result; } @Override @@ -251,7 +314,7 @@ public class FiniteClosure implements IFiniteClosure { } @Override - public Set getAllTypes(String typeName) { + public Set getAllTypesByName(String typeName) { if(!strInheritanceGraph.containsKey(typeName)) return new HashSet<>(); return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new)); diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java index 0a1fde25..add681e5 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -5,7 +5,7 @@ import java.util.Map.Entry; import java.util.Set; import java.util.function.Function; -public class Unifier implements Function { +public class Unifier implements Function /*, Set*/ { // TODO set implementieren private HashMap substitutions = new HashMap<>(); public static Unifier IDENTITY = new Unifier(); diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 6db1a512..d15fefdd 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -101,12 +101,12 @@ public class MartelliMontanariUnify implements IUnify { TypeParams rhsTypeParams = rhs.getTypeParams(); TypeParams lhsTypeParams = lhs.getTypeParams(); + if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size()) + return null; // conflict + if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0) return Optional.empty(); - if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size()) - return null; // conflict - for(int i = 0; i < rhsTypeParams.size(); i++) result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT)); diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index ce7e13c4..807c8d7f 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -227,105 +227,223 @@ public class Unify { Type rhsType = pair.getRhsType(); // Case 1: (a <. Theta') - if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) { - Type thetaPrime = pair.getRhsType(); - Set set = new HashSet<>(); - IUnify unify = new MartelliMontanariUnify(); - - Set cs = fc.getAllTypes(rhsType.getName()); - - Set thetaQs = cs.stream().flatMap( - x -> fc.smaller(x).stream().filter(y -> y.getTypeParams().arePlaceholders()) - ).collect(Collectors.toCollection(HashSet::new)); - - for(Type c : cs) { - 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)); - } - } - } - } - - result.add(set); - } + if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) + result.add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); // Case 2: (a <.? ? ext Theta') - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){ - throw new NotImplementedException(); // TODO - } + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) + result.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) { - Set set = new HashSet<>(); - for(Type theta : fc.smArg(rhsType)) - set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT)); - result.add(set); - } + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) + result.add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); // Case 4: (a <.? Theta') - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) { - Set set = new HashSet<>(); - set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT)); - result.add(set); - } + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) + result.add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); // Case 5: (Theta <. a) - else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) { - Set set = new HashSet<>(); - for(Type thetaS : fc.greater(lhsType)) - set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.add(set); - } + else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) + result.add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); // Case 6: (? ext Theta <.? a) - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) { - Set set = new HashSet<>(); - for(Type thetaS : fc.grArg(lhsType)) - set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.add(set); - } - + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) + result.add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); + // Case 7: (? sup Theta <.? a) - else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) { - throw new NotImplementedException(); // TODO - } + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) + result.add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); // Case 8: (Theta <.? a) - else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) { - Set set = new HashSet<>(); - for(Type thetaS : fc.grArg(lhsType)) - set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.add(set); + else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) + result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); + } + + return result; + } + + protected Set unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) { + Set result = new HashSet<>(); + IUnify unify = new MartelliMontanariUnify(); + + Set cs = fc.getAllTypesByName(thetaPrime.getName()); + + for(Type c : cs) { + + // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? + Set thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); + thetaQs.add(c); // reflexive + + Set thetaQPrimes = new HashSet<>(); + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + for(Type param : cParams) + candidateParams.add(fc.grArg(param)); + + for(TypeParams tp : permuteParams(candidateParams)) + thetaQPrimes.add(c.setTypeParams(tp)); + } + + for(Type tqp : thetaQPrimes) { + Optional opt = unify.unify(tqp, thetaPrime); + if (!opt.isPresent()) + continue; + + Unifier unifier = opt.get(); + Set> substitutions = unifier.getSubstitutions(); + for (Entry sigma : substitutions) + result.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(a, x, PairOperator.EQUALSDOT)) + .forEach(x -> result.add(x)); + } + } } return result; } - protected void permuteParams(ArrayList> candidates, int idx, Set result, Type[] current) { + protected Set unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) { + Set result = new HashSet<>(); + IUnify unify = new MartelliMontanariUnify(); + + Type thetaPrime = extThetaPrime.getExtendedType(); + Set cs = fc.getAllTypesByName(thetaPrime.getName()); + + for(Type c : cs) { + + // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? + Set thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); + thetaQs.add(c); // reflexive + + Set thetaQPrimes = new HashSet<>(); + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + for(Type param : cParams) + candidateParams.add(fc.grArg(param)); + + for(TypeParams tp : permuteParams(candidateParams)) + thetaQPrimes.add(c.setTypeParams(tp)); + } + + for(Type tqp : thetaQPrimes) { + Optional opt = unify.unify(tqp, thetaPrime); + if (!opt.isPresent()) + continue; + + Unifier unifier = opt.get(); + Set> substitutions = unifier.getSubstitutions(); + for (Entry sigma : substitutions) + result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); + for (Type tq : thetaQs) { + ExtendsType extTq = new ExtendsType(tq); + Set smaller = fc.smaller(unifier.apply(extTq)); + smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT)) + .forEach(x -> result.add(x)); + } + + } + } + + return result; + } + + protected Set unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) { + Set result = new HashSet<>(); + for(Type theta : fc.smArg(subThetaPrime)) + result.add(new MPair(a, theta, PairOperator.EQUALSDOT)); + return result; + } + + protected Set unifyCase4(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) { + Set result = new HashSet<>(); + result.add(new MPair(a, thetaPrime, PairOperator.EQUALSDOT)); + return result; + } + + protected Set unifyCase5(Type theta, PlaceholderType a, IFiniteClosure fc) { + Set result = new HashSet<>(); + for(Type thetaS : fc.greater(theta)) + result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT)); + return result; + } + + protected Set unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) { + Set result = new HashSet<>(); + for(Type thetaS : fc.grArg(extTheta)) + result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT)); + return result; + } + + protected Set unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) { + Set result = new HashSet<>(); + IUnify unify = new MartelliMontanariUnify(); + + Type theta = supTheta.getSuperedType(); + Set cs = fc.getAllTypesByName(theta.getName()); + + for(Type c : cs) { + + // Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig? + Set thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); + thetaQs.add(c); // reflexive + + Set thetaQPrimes = new HashSet<>(); + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + for(Type param : cParams) + candidateParams.add(fc.grArg(param)); + + for(TypeParams tp : permuteParams(candidateParams)) + thetaQPrimes.add(c.setTypeParams(tp)); + } + + for(Type tqp : thetaQPrimes) { + Optional opt = unify.unify(tqp, theta); + if (!opt.isPresent()) + continue; + + Unifier unifier = opt.get(); + Set> substitutions = unifier.getSubstitutions(); + for (Entry sigma : substitutions) + result.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(a, new SuperType(x), PairOperator.EQUALSDOT)) + .forEach(x -> result.add(x)); + } + + } + } + + return result; + } + + protected Set unifyCase8(Type theta, PlaceholderType a, IFiniteClosure fc) { + Set result = new HashSet<>(); + for(Type thetaS : fc.grArg(theta)) + result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT)); + return result; + } + + protected Set permuteParams(ArrayList> candidates) { + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new Type[candidates.size()]); + return result; + } + + private void permuteParams(ArrayList> candidates, int idx, Set result, Type[] current) { if(candidates.size() == idx) { result.add(new TypeParams(Arrays.copyOf(current, current.length))); return; diff --git a/test/unify/FiniteClosureTest.java b/test/unify/FiniteClosureTest.java index 7b1b6664..073b4a94 100644 --- a/test/unify/FiniteClosureTest.java +++ b/test/unify/FiniteClosureTest.java @@ -1,13 +1,39 @@ package unify; +import org.junit.Assert; 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.FiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.Type; import de.dhbwstuttgart.typeinference.unifynew.TypeFactory; -public class FiniteClosureTest { +public class FiniteClosureTest extends FiniteClosure { + + @Test + public void testMatch() { + TypeFactory tf = new TypeFactory(); + + Type a = tf.getPlaceholderType("a"); + Type b = tf.getPlaceholderType("b"); + Type c = tf.getPlaceholderType("c"); + + Type A = tf.getSimpleType("A"); + Type B = tf.getSimpleType("B"); + Type C1 = tf.getSimpleType("C", a, b, c); + Type C2 = tf.getSimpleType("C", a, A, b); + Type C3 = tf.getSimpleType("C", A, B, A); + Type D1 = tf.getSimpleType("D", C1, a, b, c); + Type D2 = tf.getSimpleType("D", C3, A, B, A); + + System.out.println(match(C2, C1)); + System.out.println(match(C3, C1)); + System.out.println(match(D2, D1)); + Assert.assertFalse(match(C3, C2).isPresent()); + Assert.assertFalse(match(C1, C2).isPresent()); + } @Test public void testGreater() { diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 1b120dae..5c3ad04e 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -25,6 +25,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("MyList"), tf.getSimpleType("List", tf.getSimpleType("Integer"))); //fcb.add(tf.getSimpleType("List", "T")); IFiniteClosure fc = fcb.getCollectionExample(); @@ -35,10 +36,10 @@ public class UnifyTest extends Unify { // Number <. A // 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("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("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("Number"), PairOperator.SMALLERDOT)); + eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "A"), 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)); @@ -80,8 +81,7 @@ public class UnifyTest extends Unify { candidates.add(p2); candidates.add(p3); - Set result = new HashSet<>(); - permuteParams(candidates, 0, result, new Type[candidates.size()]); + Set result = permuteParams(candidates); System.out.println(result); } From 21c6aef7fd8a8268c05837f739d192abb55a6f7a Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Sun, 20 Mar 2016 18:05:34 +0100 Subject: [PATCH 4/4] =?UTF-8?q?cartesische=20produkte=20=C3=BCberarbeitet?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../typeinference/unifynew/Unify.java | 111 ++++++++++-------- test/unify/UnifyTest.java | 6 +- 2 files changed, 65 insertions(+), 52 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 807c8d7f..ae702fba 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -57,33 +57,48 @@ public class Unify { * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia */ - // All Sets - List> sets = new ArrayList>(); + // 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) - sets.add(eq1s); // Add Eq1' + if(eq1s.size() != 0) { + 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) - sets.add(bufferSet); + if(bufferSet.size() != 0) { + Set> wrap = new HashSet<>(); + wrap.add(bufferSet); + topLevelSets.add(wrap); + } // Sets that originate from pair pattern matching // Sets of the "second level" - - sets.addAll(calculatePairSets(eq2s, fc)); + Set>> secondLevelSets = calculatePairSets(eq2s, fc); /* Up to here, no cartesian products are calculated. - * Around here, filters for pairs and sets can be applied */ + * filters for pairs and sets can be applied here */ ISetOperations setOps = new GuavaSetOperations(); - // Calculate the cartesian products - Set> result = setOps.cartesianProduct(sets).stream() - .map(x -> new HashSet(x)).collect(Collectors.toCollection(HashSet::new)); + // Sub cartesian products of the second level (pattern matched) sets + for(Set> secondLevelSet : secondLevelSets) { + List> secondLevelSetList = new ArrayList<>(secondLevelSet); + topLevelSets.add(setOps.cartesianProduct(secondLevelSetList) + .stream().map(x -> new HashSet<>(x)) + .collect(Collectors.toCollection(HashSet::new))); + } + + // 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); /* @@ -91,38 +106,41 @@ public class Unify { */ /* - * TODO - * Im Paper wird Eq'' genannt, es wird also von einer Menge in einer Menge in einer Menge ausgegangen. - * Durch das flache Kartesische Produkt gibt es hier aber nur Mengen in Mengen. - * Richtig so? + * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht) */ + Set> eqPrimeSetFlat = new HashSet<>(); + for(Set> setToFlatten : eqPrimeSet) { + Set buffer = new HashSet<>(); + setToFlatten.stream().forEach(x -> buffer.addAll(x)); + eqPrimeSetFlat.add(buffer); + } IRuleSet rules = new RuleSet(fc); Set> changed = new HashSet<>(); - Set> unchanged = new HashSet<>(); + Set> eqPrimePrimeSet = new HashSet<>(); - for(Set eqss : result) { - Optional> newEqss = rules.subst(eqss); - if(newEqss.isPresent()) - changed.add(newEqss.get()); - else - unchanged.add(eqss); + for(Set eqPrime : eqPrimeSetFlat) { + Optional> eqPrimePrime = rules.subst(eqPrime); + + if(eqPrimePrime.isPresent()) + changed.add(eqPrimePrime.get()); + else + eqPrimePrimeSet.add(eqPrime); } - /* * Step 6 a) Restart for pairs where subst was applied * b) Build the union over everything */ - for(Set eqss : changed) - unchanged.addAll(this.unify(eqss, fc)); + for(Set eqss : changed) { + eqPrimePrimeSet.addAll(this.unify(eqss, fc)); + } /* - * Step 7: Filter result for solved pairs TODO wie? + * Step 7: Filter result for solved pairs */ - - return unchanged; + return eqPrimePrimeSet; } @@ -217,8 +235,12 @@ public class Unify { } - protected List> calculatePairSets(Set eq2s, IFiniteClosure fc) { - List> result = new ArrayList>(); + protected Set>> calculatePairSets(Set eq2s, IFiniteClosure fc) { + List>> result = new ArrayList<>(); + + // Init all 8 cases + for(int i = 0; i < 8; i++) + result.add(new HashSet<>()); for(MPair pair : eq2s) { @@ -228,38 +250,38 @@ public class Unify { // Case 1: (a <. Theta') if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) - result.add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); + 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.add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); + 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.add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); + result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); // Case 4: (a <.? Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) - result.add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); + result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); // Case 5: (Theta <. a) else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) - result.add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); + result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); // Case 6: (? ext Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) - result.add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); + result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); // Case 7: (? sup Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) - result.add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); + result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); // Case 8: (Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) - result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); + result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); } - return result; + return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); } protected Set unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) { @@ -456,13 +478,4 @@ public class Unify { permuteParams(candidates, idx+1, result, current); } } - - private Set getAllInstantiations(Type t, IFiniteClosure fc) { - Set result = new HashSet<>(); - result.add(t); - return result; - - // TODO - } - } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 5c3ad04e..ae219dd2 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -36,10 +36,10 @@ public class UnifyTest extends Unify { // Number <. A // 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("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("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "A"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "A"), 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));