Java, typeres: partial resolution algorithm for type inference
This commit is contained in:
Bendegúz Nagy
@ -4,12 +4,17 @@
|
||||
|
||||
package net.sourceforge.pmd.lang.java.typeresolution.typeinference;
|
||||
|
||||
import net.sourceforge.pmd.lang.java.typeresolution.typedefinition.JavaTypeDefinition;
|
||||
|
||||
import static net.sourceforge.pmd.lang.java.typeresolution.typeinference.InferenceRuleType.EQUALITY;
|
||||
import static net.sourceforge.pmd.lang.java.typeresolution.typeinference.InferenceRuleType.SUBTYPE;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.BitSet;
|
||||
import java.util.Collections;
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.List;
|
||||
import java.util.Map;
|
||||
import java.util.Set;
|
||||
@ -21,11 +26,198 @@ public final class TypeInferenceResolver {
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
* Resolve unresolved variables in a list of bounds.
|
||||
*/
|
||||
public static Map<Variable, JavaTypeDefinition> resolveVariables(List<Bound> bounds) {
|
||||
Map<Variable, Set<Variable>> variableDependencies = getVariableDependencies(bounds);
|
||||
Map<Variable, JavaTypeDefinition> instantiations = getInstantiations(bounds);
|
||||
|
||||
List<Variable> uninstantiatedVariables = new ArrayList<>(getUninstantiatedVariables(bounds));
|
||||
|
||||
// If every variable in V has an instantiation, then resolution succeeds and this procedure terminates.
|
||||
while (!uninstantiatedVariables.isEmpty()) {
|
||||
// "... ii) there exists no non-empty proper subset of { α1, ..., αn } with this property. ..."
|
||||
|
||||
// Note: since the Combinations class enumerates the power set from least numerous to most numerous sets
|
||||
// the above requirement is satisfied
|
||||
for (List<Variable> variableSet : new Combinations(uninstantiatedVariables)) {
|
||||
if (isProperSubsetOfVariables(variableSet, instantiations, variableDependencies, bounds)) {
|
||||
// TODO: resolve variables
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
return instantiations;
|
||||
}
|
||||
|
||||
/**
|
||||
* Given a set of inference variables to resolve, let V be the union of this set and all variables upon which
|
||||
* the resolution of at least one variable in this set depends.
|
||||
* <p>
|
||||
* ...
|
||||
* <p>
|
||||
* Otherwise, let { α1, ..., αn } be a non-empty subset of uninstantiated variables in V such that i) for all
|
||||
* i (1 ≤ i ≤ n), if αi depends on the resolution of a variable β, then either β has an instantiation or
|
||||
* there is some j such that β = αj; and Resolution proceeds by generating an instantiation for each of α1,
|
||||
* ..., αn based on the bounds in the bound set:
|
||||
*
|
||||
* @return true, if 'variables' is a resolvable subset
|
||||
*/
|
||||
public static boolean isProperSubsetOfVariables(List<Variable> variables,
|
||||
Map<Variable, JavaTypeDefinition> instantiations,
|
||||
Map<Variable, Set<Variable>> dependencies,
|
||||
List<Bound> bounds) {
|
||||
|
||||
// search the bounds for an
|
||||
for (Variable unresolvedVariable : variables) {
|
||||
for (Variable dependency : dependencies.get(unresolvedVariable)) {
|
||||
if (!instantiations.containsKey(dependency)
|
||||
&& !boundsHaveAnEqualityBetween(variables, dependency, bounds)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return true, if 'bounds' contains an equality between 'second' and an element from 'firstList'
|
||||
*/
|
||||
public static boolean boundsHaveAnEqualityBetween(List<Variable> firstList, Variable second, List<Bound> bounds) {
|
||||
for (Bound bound : bounds) {
|
||||
for (Variable first : firstList) {
|
||||
if (bound.ruleType == EQUALITY
|
||||
&& ((bound.leftVariable() == first && bound.rightVariable() == second)
|
||||
|| (bound.leftVariable() == second && bound.rightVariable() == first))) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* Makes it possible to iterate over the power set of a List. The order is from the least numerous
|
||||
* to the most numerous.
|
||||
* Example list: ABC
|
||||
* Order: A, B, C, AB, AC, BC, ABC
|
||||
*/
|
||||
private static class Combinations implements Iterable<List<Variable>> {
|
||||
private int n;
|
||||
private int k;
|
||||
private List<Variable> permuteThis;
|
||||
private List<Variable> resultList = new ArrayList<>();
|
||||
private List<Variable> unmodifyableViewOfResult = Collections.unmodifiableList(resultList);
|
||||
|
||||
public Combinations(List<Variable> permuteThis) {
|
||||
this.permuteThis = permuteThis;
|
||||
this.n = permuteThis.size();
|
||||
this.k = 0;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Iterator<List<Variable>> iterator() {
|
||||
return new Iterator<List<Variable>>() {
|
||||
private BitSet nextBitSet = new BitSet(n);
|
||||
|
||||
{
|
||||
advanceToNextK();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void remove() {
|
||||
|
||||
}
|
||||
|
||||
private void advanceToNextK() {
|
||||
if (++k > n) {
|
||||
nextBitSet = null;
|
||||
} else {
|
||||
nextBitSet.clear();
|
||||
nextBitSet.set(0, k);
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasNext() {
|
||||
return nextBitSet != null;
|
||||
}
|
||||
|
||||
@Override
|
||||
public List<Variable> next() {
|
||||
BitSet resultBitSet = (BitSet) nextBitSet.clone();
|
||||
|
||||
int b = nextBitSet.previousClearBit(n - 1);
|
||||
int b1 = nextBitSet.previousSetBit(b);
|
||||
|
||||
if (b1 == -1) {
|
||||
advanceToNextK();
|
||||
} else {
|
||||
nextBitSet.clear(b1);
|
||||
nextBitSet.set(b1 + 1, b1 + (n - b) + 1);
|
||||
nextBitSet.clear(b1 + (n - b) + 1, n);
|
||||
}
|
||||
|
||||
resultList.clear();
|
||||
for (int i = 0; i < n; ++i) {
|
||||
if (resultBitSet.get(i)) {
|
||||
resultList.add(permuteThis.get(i));
|
||||
}
|
||||
}
|
||||
|
||||
return unmodifyableViewOfResult;
|
||||
}
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* @return A map of variable -> proper type produced by searching for α = T or T = α bounds
|
||||
*/
|
||||
public static Map<Variable, JavaTypeDefinition> getInstantiations(List<Bound> bounds) {
|
||||
Map<Variable, JavaTypeDefinition> result = new HashMap<>();
|
||||
|
||||
// The term "type" is used loosely in this chapter to include type-like syntax that contains inference
|
||||
// variables. The term proper type excludes such "types" that mention inference variables. Assertions that
|
||||
// involve inference variables are assertions about every proper type that can be produced by replacing each
|
||||
// inference variable with a proper type.
|
||||
|
||||
// Some bounds relate an inference variable to a proper type. Let T be a proper type. Given a bound of the
|
||||
// form α = T or T = α, we say T is an instantiation of α. Similarly, given a bound of the form α <: T, we
|
||||
// say T is a proper upper bound of α, and given a bound of the form T <: α, we say T is a proper lower bound
|
||||
// of α.
|
||||
for (Bound bound : bounds) {
|
||||
if (bound.ruleType() == EQUALITY) {
|
||||
// Note: JLS's wording is not clear, but proper type excludes arrays, nulls, primitives, etc.
|
||||
if (bound.isLeftVariable() && bound.isRightProper()) {
|
||||
result.put(bound.leftVariable(), bound.rightProper());
|
||||
} else if (bound.isLeftProper() && bound.isRightVariable()) {
|
||||
result.put(bound.rightVariable(), bound.leftProper());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return A list of variables which have no direct instantiations
|
||||
*/
|
||||
public static Set<Variable> getUninstantiatedVariables(List<Bound> bounds) {
|
||||
Set<Variable> result = getMentionedVariables(bounds);
|
||||
result.removeAll(getInstantiations(bounds).keySet());
|
||||
return result;
|
||||
}
|
||||
|
||||
public static Map<Variable, Set<Variable>> getVariableDependencies(List<Bound> bounds) {
|
||||
Set<Variable> variables = getMentionedVariables(bounds);
|
||||
Map<Variable, Set<Variable>> dependencies = new HashMap<>();
|
||||
|
||||
for (Variable mentionedVariable : variables) {
|
||||
for (Variable mentionedVariable : getMentionedVariables(bounds)) {
|
||||
Set<Variable> set = new HashSet<>();
|
||||
// An inference variable α depends on the resolution of itself.
|
||||
set.add(mentionedVariable);
|
||||
@ -64,14 +256,22 @@ public final class TypeInferenceResolver {
|
||||
// An inference variable α depends on the resolution of an inference variable β if there exists an inference
|
||||
// variable γ such that α depends on the resolution of γ and γ depends on the resolution of β.
|
||||
|
||||
for(int i = 0; i < variables.size(); ++i) { // do this n times, where n is the count of variables
|
||||
for (int i = 0; i < dependencies.size(); ++i) { // do this n times, where n is the count of variables
|
||||
boolean noMoreChanges = true;
|
||||
|
||||
for (Map.Entry<Variable, Set<Variable>> entry : dependencies.entrySet()) {
|
||||
// take the Variable's dependency list
|
||||
for(Variable variable : entry.getValue()) {
|
||||
for (Variable variable : entry.getValue()) {
|
||||
// add those variable's dependencies
|
||||
entry.getValue().addAll(dependencies.get(variable));
|
||||
if (entry.getValue().addAll(dependencies.get(variable))) {
|
||||
noMoreChanges = false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (noMoreChanges) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
return dependencies;
|
||||
|
||||
Reference in New Issue
Block a user