From c94bb39352d86de0378eb7c3d7eab72d67f5e094 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bendeg=C3=BAz=20Nagy?= Date: Fri, 4 Aug 2017 16:32:27 +0200 Subject: [PATCH] Java, typeres: partial resolution algorithm for type inference --- .../typeinference/TypeInferenceResolver.java | 210 +++++++++++++++++- 1 file changed, 205 insertions(+), 5 deletions(-) diff --git a/pmd-java/src/main/java/net/sourceforge/pmd/lang/java/typeresolution/typeinference/TypeInferenceResolver.java b/pmd-java/src/main/java/net/sourceforge/pmd/lang/java/typeresolution/typeinference/TypeInferenceResolver.java index 081f00f329..b4deb26c1b 100644 --- a/pmd-java/src/main/java/net/sourceforge/pmd/lang/java/typeresolution/typeinference/TypeInferenceResolver.java +++ b/pmd-java/src/main/java/net/sourceforge/pmd/lang/java/typeresolution/typeinference/TypeInferenceResolver.java @@ -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 resolveVariables(List bounds) { + Map> variableDependencies = getVariableDependencies(bounds); + Map instantiations = getInstantiations(bounds); + + List 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 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. + *

+ * ... + *

+ * 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 variables, + Map instantiations, + Map> dependencies, + List 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 firstList, Variable second, List 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> { + private int n; + private int k; + private List permuteThis; + private List resultList = new ArrayList<>(); + private List unmodifyableViewOfResult = Collections.unmodifiableList(resultList); + + public Combinations(List permuteThis) { + this.permuteThis = permuteThis; + this.n = permuteThis.size(); + this.k = 0; + } + + @Override + public Iterator> iterator() { + return new Iterator>() { + 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 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 getInstantiations(List bounds) { + Map 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 getUninstantiatedVariables(List bounds) { + Set result = getMentionedVariables(bounds); + result.removeAll(getInstantiations(bounds).keySet()); + return result; + } + public static Map> getVariableDependencies(List bounds) { - Set variables = getMentionedVariables(bounds); Map> dependencies = new HashMap<>(); - for (Variable mentionedVariable : variables) { + for (Variable mentionedVariable : getMentionedVariables(bounds)) { Set 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> 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;