added missing cases

This commit is contained in:
Florian Steurer 2016-03-20 15:09:12 +01:00
parent fa9627b883
commit 299f8f56ca
7 changed files with 301 additions and 94 deletions

View File

@ -50,5 +50,5 @@ public interface IFiniteClosure {
public Set<Type> smArg(PlaceholderType type);
public Optional<Type> getGenericType(String typeName);
public Set<Type> getAllTypes(String typeName);
public Set<Type> getAllTypesByName(String typeName);
}

View File

@ -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<Type, Node<Type>> inheritanceGraph;
private HashMap<String, HashSet<Node<Type>>> strInheritanceGraph;
public FiniteClosure() {
}
public FiniteClosure(Set<MPair> pairs) {
inheritanceGraph = new HashMap<Type, Node<Type>>();
@ -59,9 +65,27 @@ public class FiniteClosure implements IFiniteClosure {
*/
@Override
public Set<Type> smaller(Type type) {
// - if(T < T') then T <=* T'
Set<Type> 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<Node<Type>> candidateNodes = strInheritanceGraph.get(type.getName());
for(Node<Type> candidateNode : candidateNodes) {
Type theta2 = candidateNode.getContent();
Optional<Unifier> 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<Unifier> 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<Type> grArg(PlaceholderType type) {
return new HashSet<>();
HashSet<Type> 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<Type> smArg(PlaceholderType type) {
return new HashSet<>();
HashSet<Type> 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<Type> getAllTypes(String typeName) {
public Set<Type> getAllTypesByName(String typeName) {
if(!strInheritanceGraph.containsKey(typeName))
return new HashSet<>();
return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new));

View File

@ -5,7 +5,7 @@ import java.util.Map.Entry;
import java.util.Set;
import java.util.function.Function;
public class Unifier implements Function<Type, Type> {
public class Unifier implements Function<Type, Type> /*, Set<MPair>*/ { // TODO set implementieren
private HashMap<PlaceholderType, Type> substitutions = new HashMap<>();
public static Unifier IDENTITY = new Unifier();

View File

@ -101,12 +101,12 @@ public class MartelliMontanariUnify implements IUnify {
TypeParams rhsTypeParams = rhs.getTypeParams();
TypeParams lhsTypeParams = lhs.getTypeParams();
if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
return Optional.empty();
if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size())
return null; // conflict
if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
return Optional.empty();
for(int i = 0; i < rhsTypeParams.size(); i++)
result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));

View File

@ -227,18 +227,53 @@ public class Unify {
Type rhsType = pair.getRhsType();
// Case 1: (a <. Theta')
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
Type thetaPrime = pair.getRhsType();
Set<MPair> set = new HashSet<>();
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)
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)
result.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));
// Case 5: (Theta <. a)
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)
result.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));
// Case 8: (Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
}
return result;
}
protected Set<MPair> unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
Set<Type> cs = fc.getAllTypes(rhsType.getName());
Set<Type> thetaQs = cs.stream().flatMap(
x -> fc.smaller(x).stream().filter(y -> y.getTypeParams().arePlaceholders())
).collect(Collectors.toCollection(HashSet::new));
Set<Type> cs = fc.getAllTypesByName(thetaPrime.getName());
for(Type c : cs) {
// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
Set<Type> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
thetaQs.add(c); // reflexive
Set<Type> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
@ -247,85 +282,168 @@ public class Unify {
ArrayList<Set<Type>> candidateParams = new ArrayList<>();
for(Type param : cParams)
candidateParams.add(fc.grArg(param));
Set<TypeParams> permutations = new HashSet<TypeParams>();
permuteParams(candidateParams, 0, permutations, new Type[candidateParams.size()]);
for(TypeParams tp : permutations)
for(TypeParams tp : permuteParams(candidateParams))
thetaQPrimes.add(c.setTypeParams(tp));
}
for(Type tqp : thetaQPrimes) {
Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
if(opt.isPresent()) {
if (!opt.isPresent())
continue;
Unifier unifier = opt.get();
Set<Entry<PlaceholderType, Type>> substitutions = unifier.getSubstitutions();
for (Entry<PlaceholderType, Type> sigma : substitutions)
set.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
for (Type tq : thetaQs) {
Set<Type> smaller = fc.smaller(unifier.apply(tq));
smaller.stream().map(x -> new MPair(lhsType, x, PairOperator.EQUALSDOT)).forEach(x -> set.add(x));
}
}
}
smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
.forEach(x -> result.add(x));
}
result.add(set);
}
// Case 2: (a <.? ? ext Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){
throw new NotImplementedException(); // TODO
}
// Case 3: (a <.? ? sup Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) {
Set<MPair> set = new HashSet<>();
for(Type theta : fc.smArg(rhsType))
set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT));
result.add(set);
}
// Case 4: (a <.? Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT));
result.add(set);
}
// Case 5: (Theta <. a)
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.greater(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.add(set);
}
// Case 6: (? ext Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.grArg(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.add(set);
}
// Case 7: (? sup Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) {
throw new NotImplementedException(); // TODO
}
// Case 8: (Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.grArg(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.add(set);
}
}
return result;
}
protected void permuteParams(ArrayList<Set<Type>> candidates, int idx, Set<TypeParams> result, Type[] current) {
protected Set<MPair> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
Type thetaPrime = extThetaPrime.getExtendedType();
Set<Type> cs = fc.getAllTypesByName(thetaPrime.getName());
for(Type c : cs) {
// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
Set<Type> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
thetaQs.add(c); // reflexive
Set<Type> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
thetaQPrimes.add(c);
else {
ArrayList<Set<Type>> 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<Unifier> opt = unify.unify(tqp, thetaPrime);
if (!opt.isPresent())
continue;
Unifier unifier = opt.get();
Set<Entry<PlaceholderType, Type>> substitutions = unifier.getSubstitutions();
for (Entry<PlaceholderType, Type> sigma : substitutions)
result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
for (Type tq : thetaQs) {
ExtendsType extTq = new ExtendsType(tq);
Set<Type> 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<MPair> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
for(Type theta : fc.smArg(subThetaPrime))
result.add(new MPair(a, theta, PairOperator.EQUALSDOT));
return result;
}
protected Set<MPair> unifyCase4(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
result.add(new MPair(a, thetaPrime, PairOperator.EQUALSDOT));
return result;
}
protected Set<MPair> unifyCase5(Type theta, PlaceholderType a, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
for(Type thetaS : fc.greater(theta))
result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
return result;
}
protected Set<MPair> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
for(Type thetaS : fc.grArg(extTheta))
result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
return result;
}
protected Set<MPair> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
Type theta = supTheta.getSuperedType();
Set<Type> cs = fc.getAllTypesByName(theta.getName());
for(Type c : cs) {
// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
Set<Type> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
thetaQs.add(c); // reflexive
Set<Type> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
thetaQPrimes.add(c);
else {
ArrayList<Set<Type>> 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<Unifier> opt = unify.unify(tqp, theta);
if (!opt.isPresent())
continue;
Unifier unifier = opt.get();
Set<Entry<PlaceholderType, Type>> substitutions = unifier.getSubstitutions();
for (Entry<PlaceholderType, Type> sigma : substitutions)
result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
for (Type tq : thetaQs) {
Set<Type> 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<MPair> unifyCase8(Type theta, PlaceholderType a, IFiniteClosure fc) {
Set<MPair> result = new HashSet<>();
for(Type thetaS : fc.grArg(theta))
result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
return result;
}
protected Set<TypeParams> permuteParams(ArrayList<Set<Type>> candidates) {
Set<TypeParams> result = new HashSet<>();
permuteParams(candidates, 0, result, new Type[candidates.size()]);
return result;
}
private void permuteParams(ArrayList<Set<Type>> candidates, int idx, Set<TypeParams> result, Type[] current) {
if(candidates.size() == idx) {
result.add(new TypeParams(Arrays.copyOf(current, current.length)));
return;

View File

@ -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() {

View File

@ -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<TypeParams> result = new HashSet<>();
permuteParams(candidates, 0, result, new Type[candidates.size()]);
Set<TypeParams> result = permuteParams(candidates);
System.out.println(result);
}