|
|
|
@@ -410,8 +410,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
// 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);
|
|
|
|
|
else {
|
|
|
|
|
// If a pair is not defined, the unificiation will fail, so the loop can be stopped here.
|
|
|
|
|
undefined.add(pair);
|
|
|
|
|
break;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Filter empty sets or sets that only contain an empty set.
|
|
|
|
@@ -425,9 +428,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
|
|
|
|
|
boolean allGen = true;
|
|
|
|
|
boolean allGen = thetaPrime.getTypeParams().size() > 0;
|
|
|
|
|
for(UnifyType t : thetaPrime.getTypeParams())
|
|
|
|
|
if(t instanceof PlaceholderType && !((PlaceholderType) t).isGenerated()) {
|
|
|
|
|
if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
|
|
|
|
|
allGen = false;
|
|
|
|
|
break;
|
|
|
|
|
}
|
|
|
|
@@ -437,7 +440,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
|
|
|
|
|
for(UnifyType c : cs) {
|
|
|
|
|
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
|
|
|
|
|
thetaQs.add(thetaPrime);
|
|
|
|
|
//thetaQs.add(thetaPrime);
|
|
|
|
|
Set<UnifyType> thetaQPrimes = new HashSet<>();
|
|
|
|
|
TypeParams cParams = c.getTypeParams();
|
|
|
|
|
if(cParams.size() == 0)
|
|
|
|
@@ -493,7 +496,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
/**
|
|
|
|
|
* Cartesian Product Case 2: (a <.? ? ext Theta')
|
|
|
|
|
*/
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
|
|
|
|
|
private Set<Set<UnifyPair>> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
|
|
|
|
|
UnifyType aPrime = PlaceholderType.freshPlaceholder();
|
|
|
|
@@ -513,7 +516,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
/**
|
|
|
|
|
* Cartesian Product Case 3: (a <.? ? sup Theta')
|
|
|
|
|
*/
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
|
|
|
|
|
private Set<Set<UnifyPair>> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
|
|
|
|
|
UnifyType aPrime = PlaceholderType.freshPlaceholder();
|
|
|
|
@@ -531,27 +534,15 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
return result;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Cartesian Product Case 4: (a <.? Theta')
|
|
|
|
|
*/
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
Set<UnifyPair> resultPrime = new HashSet<>();
|
|
|
|
|
resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.EQUALSDOT));
|
|
|
|
|
result.add(resultPrime);
|
|
|
|
|
|
|
|
|
|
return result;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Cartesian Product Case 5: (Theta <. a)
|
|
|
|
|
*/
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
private Set<Set<UnifyPair>> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
|
|
|
|
|
boolean allGen = true;
|
|
|
|
|
boolean allGen = theta.getTypeParams().size() > 0;
|
|
|
|
|
for(UnifyType t : theta.getTypeParams())
|
|
|
|
|
if(t instanceof PlaceholderType && !((PlaceholderType) t).isGenerated()) {
|
|
|
|
|
if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
|
|
|
|
|
allGen = false;
|
|
|
|
|
break;
|
|
|
|
|
}
|
|
|
|
@@ -574,44 +565,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
|
|
|
|
|
return result;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Cartesian Product Case 6: (? ext Theta <.? a)
|
|
|
|
|
*/
|
|
|
|
|
protected Set<Set<UnifyPair>> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
UnifyType freshTph = PlaceholderType.freshPlaceholder();
|
|
|
|
|
UnifyType extFreshTph = new ExtendsType(freshTph);
|
|
|
|
|
|
|
|
|
|
Set<UnifyPair> 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<Set<UnifyPair>> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
|
|
|
|
|
UnifyType aPrime = PlaceholderType.freshPlaceholder();
|
|
|
|
|
UnifyType supAPrime = new SuperType(aPrime);
|
|
|
|
|
UnifyType theta = supTheta.getSuperedType();
|
|
|
|
|
Set<UnifyPair> 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<Set<UnifyPair>> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
private Set<Set<UnifyPair>> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
|
|
|
|
|
Set<Set<UnifyPair>> result = new HashSet<>();
|
|
|
|
|
//for(UnifyType thetaS : fc.grArg(theta)) {
|
|
|
|
|
Set<UnifyPair> resultPrime = new HashSet<>();
|
|
|
|
|