big refactoring of smaller and greater
This commit is contained in:
Florian Steurer
parent
b39dedb9aa
commit
4f265b56a4
@ -81,85 +81,56 @@ public class FiniteClosure implements IFiniteClosure {
|
||||
if(type instanceof FunNType)
|
||||
return computeSmallerFunN((FunNType) type);
|
||||
|
||||
return computeSmaller(type);
|
||||
Set<UnifyType> ts = new HashSet<>();
|
||||
ts.add(type);
|
||||
return computeSmaller(ts);
|
||||
}
|
||||
|
||||
/**
|
||||
* Computes the smaller functions for every type except FunNTypes.
|
||||
*/
|
||||
private Set<UnifyType> computeSmaller(UnifyType type) {
|
||||
// Base Case: The type is in the inheritance tree. Add all children.
|
||||
// This is Case 1 in the definition of the subtyping relation.
|
||||
if(inheritanceGraph.containsKey(type)) {
|
||||
Set<UnifyType> result = new HashSet<>();
|
||||
result.add(type);
|
||||
result.addAll(inheritanceGraph.get(type).getContentOfDescendants());
|
||||
return result;
|
||||
}
|
||||
|
||||
private Set<UnifyType> computeSmaller(Set<UnifyType> types) {
|
||||
HashSet<UnifyType> result = new HashSet<>();
|
||||
|
||||
IUnify unify = new MartelliMontanariUnify();
|
||||
Set<UnifyType> result1 = new HashSet<>();
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result1.add(type);
|
||||
|
||||
// Permute all params with values that are in smArg() of that type.
|
||||
// This corresponds to Case 3 in the definition of the subtyping relation.
|
||||
/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (UnifyType param : type.getTypeParams())
|
||||
paramCandidates.add(smArg(param));
|
||||
permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
|
||||
|
||||
// This is case 2 of the definition of the subtyping relation.
|
||||
Set<UnifyType> result2 = new HashSet<>();
|
||||
if (strInheritanceGraph.containsKey(type.getName())) {
|
||||
HashSet<UnifyType> candidates = new HashSet<>();
|
||||
// All types with the same name
|
||||
strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
|
||||
//for(UnifyType typePrime : result1) {
|
||||
for (UnifyType theta2 : candidates) {
|
||||
// Find the substitution
|
||||
Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
|
||||
if (!sigma2Opt.isPresent())
|
||||
continue;
|
||||
Unifier sigma2 = sigma2Opt.get();
|
||||
if(sigma2.size() == 0)
|
||||
continue;
|
||||
sigma2.swapPlaceholderSubstitutions(type.getTypeParams());
|
||||
//if(type.equals(theta2))
|
||||
// continue;
|
||||
Set<UnifyType> theta1s = smaller(theta2);
|
||||
for (UnifyType theta1 : theta1s) {
|
||||
// Because only the most general type is calculated, sigma1 = sigma2
|
||||
UnifyType sigma1Theta1 = sigma2.apply(theta1);
|
||||
result2.add(sigma1Theta1);
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
result2 = result1;
|
||||
|
||||
// Permute the params again.
|
||||
// This corresponds again to Case 3 of the definition of the subtyping relation.
|
||||
Set<UnifyType> result3 = new HashSet<>();
|
||||
for(UnifyType t : result2) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (UnifyType param : t.getTypeParams())
|
||||
paramCandidates.add(smArg(param));
|
||||
|
||||
Set<TypeParams> permResult = permuteParams(paramCandidates);
|
||||
|
||||
for (TypeParams newParams : permResult) {
|
||||
UnifyType tPrime = t.setTypeParams(newParams);
|
||||
if(tPrime.equals(t))
|
||||
result3.add(t);
|
||||
else
|
||||
result3.addAll(smaller(tPrime));
|
||||
for(UnifyType t : types) {
|
||||
|
||||
// if T = T' then T <* T'
|
||||
result.add(t);
|
||||
|
||||
// if C<...> <* C<...> then ... (third case in definition of <*)
|
||||
if(t.getTypeParams().size() > 0) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (int i = 0; i < t.getTypeParams().size(); i++)
|
||||
paramCandidates.add(smArg(t.getTypeParams().get(i)));
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x)));
|
||||
}
|
||||
|
||||
}
|
||||
if(!strInheritanceGraph.containsKey(t.getName()))
|
||||
continue;
|
||||
|
||||
// if T <* T' then sigma(T) <* sigma(T')
|
||||
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
|
||||
for(Node<UnifyType> candidate : candidates) {
|
||||
UnifyType theta2 = candidate.getContent();
|
||||
Optional<Unifier> optSigma = unify.unify(theta2, t);
|
||||
if(!optSigma.isPresent())
|
||||
continue;
|
||||
|
||||
Unifier sigma = optSigma.get();
|
||||
sigma.swapPlaceholderSubstitutions(t.getTypeParams());
|
||||
|
||||
Set<UnifyType> theta1Set = candidate.getContentOfDescendants();
|
||||
|
||||
for(UnifyType theta1 : theta1Set)
|
||||
result.add(theta1.apply(sigma));
|
||||
}
|
||||
}
|
||||
|
||||
return result3;
|
||||
if(result.equals(types))
|
||||
return result;
|
||||
return computeSmaller(result);
|
||||
}
|
||||
|
||||
/**
|
||||
@ -190,82 +161,58 @@ public class FiniteClosure implements IFiniteClosure {
|
||||
public Set<UnifyType> greater(UnifyType type) {
|
||||
if(type instanceof FunNType)
|
||||
return computeGreaterFunN((FunNType) type);
|
||||
return computeGreater(type);
|
||||
|
||||
Set<UnifyType> ts = new HashSet<>();
|
||||
ts.add(type);
|
||||
return computeGreater(ts);
|
||||
}
|
||||
|
||||
/**
|
||||
* Computes the greater function for all types except function types.
|
||||
*/
|
||||
protected Set<UnifyType> computeGreater(UnifyType type) {
|
||||
protected Set<UnifyType> computeGreater(Set<UnifyType> types) {
|
||||
HashSet<UnifyType> result = new HashSet<>();
|
||||
|
||||
IUnify unify = new MartelliMontanariUnify();
|
||||
Set<UnifyType> result1 = new HashSet<>();
|
||||
|
||||
// The type is in the inheritance tree. Add all children.
|
||||
// This is Case 1 in the definition of the subtyping relation.
|
||||
if(inheritanceGraph.containsKey(type))
|
||||
result1.addAll(inheritanceGraph.get(type).getContentOfPredecessors());
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result1.add(type);
|
||||
|
||||
// Permute all params with values that are in smArg() of that type.
|
||||
// This corresponds to Case 3 in the definition of the subtyping relation.
|
||||
/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (UnifyType param : type.getTypeParams())
|
||||
paramCandidates.add(grArg(param));
|
||||
permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
|
||||
|
||||
// This is case 2 of the definition of the subtyping relation.
|
||||
Set<UnifyType> result2 = new HashSet<>();
|
||||
if (strInheritanceGraph.containsKey(type.getName()) && !inheritanceGraph.containsKey(type)) {
|
||||
HashSet<UnifyType> candidates = new HashSet<>();
|
||||
// All types with the same name
|
||||
strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
|
||||
|
||||
// for(UnifyType typePrime : result1)
|
||||
for (UnifyType theta2 : candidates) {
|
||||
// Find the substitution
|
||||
Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
|
||||
if (!sigma2Opt.isPresent())
|
||||
continue;
|
||||
//if (type.equals(theta2))
|
||||
// continue;
|
||||
Unifier sigma2 = sigma2Opt.get();
|
||||
if(sigma2.size() == 0) // type.equals(theta2)
|
||||
continue;
|
||||
sigma2.swapPlaceholderSubstitutionsReverse(type.getTypeParams());
|
||||
Set<UnifyType> theta1s = greater(theta2);
|
||||
for (UnifyType theta1 : theta1s) {
|
||||
// Because only the most general type is calculated, sigma1
|
||||
// = sigma2
|
||||
UnifyType sigma1Theta1 = sigma2.apply(theta1);
|
||||
result2.add(sigma1Theta1);
|
||||
}
|
||||
// }
|
||||
}
|
||||
}
|
||||
|
||||
result2.addAll(result1);
|
||||
|
||||
// Permute the params again.
|
||||
// This corresponds again to Case 3 of the definition of the subtyping relation.
|
||||
Set<UnifyType> result3 = new HashSet<>();
|
||||
for(UnifyType t : result2) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (UnifyType param : t.getTypeParams())
|
||||
paramCandidates.add(grArg(param));
|
||||
|
||||
for (TypeParams newParams : permuteParams(paramCandidates)) {
|
||||
UnifyType tPrime = t.setTypeParams(newParams);
|
||||
if(tPrime.equals(t))
|
||||
result3.add(t);
|
||||
else
|
||||
result3.addAll(greater(tPrime));
|
||||
for(UnifyType t : types) {
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result.add(t);
|
||||
|
||||
// if C<...> <* C<...> then ... (third case in definition of <*)
|
||||
if(t.getTypeParams().size() > 0) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (int i = 0; i < t.getTypeParams().size(); i++)
|
||||
paramCandidates.add(grArg(t.getTypeParams().get(i)));
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x)));
|
||||
}
|
||||
|
||||
}
|
||||
if(!strInheritanceGraph.containsKey(t.getName()))
|
||||
continue;
|
||||
|
||||
// if T <* T' then sigma(T) <* sigma(T')
|
||||
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
|
||||
for(Node<UnifyType> candidate : candidates) {
|
||||
UnifyType theta1 = candidate.getContent();
|
||||
Optional<Unifier> optSigma = unify.unify(theta1, t);
|
||||
if(!optSigma.isPresent())
|
||||
continue;
|
||||
|
||||
Unifier sigma = optSigma.get();
|
||||
sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams());
|
||||
|
||||
Set<UnifyType> theta2Set = candidate.getContentOfPredecessors();
|
||||
|
||||
for(UnifyType theta2 : theta2Set)
|
||||
result.add(theta2.apply(sigma));
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
return result3;
|
||||
if(result.equals(types))
|
||||
return result;
|
||||
return computeGreater(result);
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
Loading…
Reference in New Issue
Block a user