[kernel] Remove unification code
Change-Id: I1e5d8196839c3e0b54c7ad9aca1cdb41ca3aecbe Reviewed-on: https://dart-review.googlesource.com/c/sdk/+/171582 Reviewed-by: Jens Johansen <jensj@google.com> Commit-Queue: Johnni Winther <johnniwinther@google.com>
This commit is contained in:
Johnni Winther
committed by
commit-bot@chromium.org
commit-bot@chromium.org
parent
b38821f39d
commit
13dfd58ac2
@@ -93,28 +93,6 @@ bool containsFreeFunctionTypeVariables(DartType type) {
|
||||
return new _FreeFunctionTypeVariableVisitor().visit(type);
|
||||
}
|
||||
|
||||
/// Given a set of type variables, finds a substitution of those variables such
|
||||
/// that the two given types becomes equal, or returns `null` if no such
|
||||
/// substitution exists.
|
||||
///
|
||||
/// For example, unifying `List<T>` with `List<String>`, where `T` is a
|
||||
/// quantified variable, yields the substitution `T = String`.
|
||||
///
|
||||
/// If successful, this equation holds:
|
||||
///
|
||||
/// substitute(type1, substitution) == substitute(type2, substitution)
|
||||
///
|
||||
/// The unification can fail for two reasons:
|
||||
/// - incompatible types, e.g. `List<T>` cannot be unified with `Set<T>`.
|
||||
/// - infinite types: e.g. `T` cannot be unified with `List<T>` because it
|
||||
/// would create the infinite type `List<List<List<...>>>`.
|
||||
Map<TypeParameter, DartType> unifyTypes(
|
||||
DartType type1, DartType type2, Set<TypeParameter> quantifiedVariables) {
|
||||
_TypeUnification unifier =
|
||||
new _TypeUnification(type1, type2, quantifiedVariables);
|
||||
return unifier.success ? unifier.substitution : null;
|
||||
}
|
||||
|
||||
/// Generates a fresh copy of the given type parameters, with their bounds
|
||||
/// substituted to reference the new parameters.
|
||||
///
|
||||
@@ -649,175 +627,6 @@ class _DeepTypeSubstitutor extends _InnerTypeSubstitutor {
|
||||
}
|
||||
}
|
||||
|
||||
class _TypeUnification {
|
||||
// Acyclic invariant: There are no cycles in the map, that is, all types can
|
||||
// be resolved to finite types by substituting all contained type variables.
|
||||
//
|
||||
// The acyclic invariant holds everywhere except during cycle detection.
|
||||
//
|
||||
// It is not checked that the substitution satisfies the bound on the type
|
||||
// parameter.
|
||||
final Map<TypeParameter, DartType> substitution = <TypeParameter, DartType>{};
|
||||
|
||||
/// Variables that may be assigned freely in order to obtain unification.
|
||||
///
|
||||
/// These are sometimes referred to as existentially quantified variables.
|
||||
final Set<TypeParameter> quantifiedVariables;
|
||||
|
||||
/// Variables that are bound by a function type inside one of the types.
|
||||
/// These may not occur in a substitution, because these variables are not in
|
||||
/// scope at the existentially quantified variables.
|
||||
///
|
||||
/// For example, suppose we are trying to satisfy the equation:
|
||||
///
|
||||
/// ∃S. <E>(E, S) => E = <E>(E, E) => E
|
||||
///
|
||||
/// That is, we must choose `S` such that the generic function type
|
||||
/// `<E>(E, S) => E` becomes `<E>(E, E) => E`. Choosing `S = E` is not a
|
||||
/// valid solution, because `E` is not in scope where `S` is quantified.
|
||||
/// The two function types cannot be unified.
|
||||
final Set<TypeParameter> _universallyQuantifiedVariables =
|
||||
new Set<TypeParameter>();
|
||||
|
||||
bool success = true;
|
||||
|
||||
_TypeUnification(DartType type1, DartType type2, this.quantifiedVariables) {
|
||||
_unify(type1, type2);
|
||||
if (success && substitution.length >= 2) {
|
||||
for (TypeParameter key in substitution.keys) {
|
||||
substitution[key] = substituteDeep(substitution[key], substitution);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
DartType _substituteHead(TypeParameterType type) {
|
||||
for (int i = 0; i <= substitution.length; ++i) {
|
||||
DartType nextType = substitution[type.parameter];
|
||||
if (nextType == null) return type;
|
||||
if (nextType is TypeParameterType) {
|
||||
type = nextType;
|
||||
} else {
|
||||
return nextType;
|
||||
}
|
||||
}
|
||||
// The cycle should have been found by _trySubstitution when the cycle
|
||||
// was created.
|
||||
throw 'Unexpected cycle found during unification';
|
||||
}
|
||||
|
||||
bool _unify(DartType type1, DartType type2) {
|
||||
if (!success) return false;
|
||||
type1 = type1 is TypeParameterType ? _substituteHead(type1) : type1;
|
||||
type2 = type2 is TypeParameterType ? _substituteHead(type2) : type2;
|
||||
if (type1 is DynamicType && type2 is DynamicType) return true;
|
||||
if (type1 is VoidType && type2 is VoidType) return true;
|
||||
if (type1 is InvalidType && type2 is InvalidType) return true;
|
||||
if (type1 is BottomType && type2 is BottomType) return true;
|
||||
if (type1 is InterfaceType && type2 is InterfaceType) {
|
||||
if (type1.classNode != type2.classNode ||
|
||||
type1.nullability != type2.nullability) {
|
||||
return _fail();
|
||||
}
|
||||
assert(type1.typeArguments.length == type2.typeArguments.length);
|
||||
for (int i = 0; i < type1.typeArguments.length; ++i) {
|
||||
if (!_unify(type1.typeArguments[i], type2.typeArguments[i])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
if (type1 is FunctionType && type2 is FunctionType) {
|
||||
if (type1.typeParameters.length != type2.typeParameters.length ||
|
||||
type1.positionalParameters.length !=
|
||||
type2.positionalParameters.length ||
|
||||
type1.namedParameters.length != type2.namedParameters.length ||
|
||||
type1.requiredParameterCount != type2.requiredParameterCount ||
|
||||
type1.nullability != type2.nullability) {
|
||||
return _fail();
|
||||
}
|
||||
// When unifying two generic functions, transform the equation like this:
|
||||
//
|
||||
// ∃S. <E>(fn1) = <T>(fn2)
|
||||
// ==>
|
||||
// ∃S. ∀G. fn1[G/E] = fn2[G/T]
|
||||
//
|
||||
// That is, assume some fixed identical choice of type parameters for both
|
||||
// functions and try to unify the instantiated function types.
|
||||
assert(!type1.typeParameters.any(quantifiedVariables.contains));
|
||||
assert(!type2.typeParameters.any(quantifiedVariables.contains));
|
||||
Map<TypeParameter, DartType> leftInstance = <TypeParameter, DartType>{};
|
||||
Map<TypeParameter, DartType> rightInstance = <TypeParameter, DartType>{};
|
||||
for (int i = 0; i < type1.typeParameters.length; ++i) {
|
||||
TypeParameter instantiator =
|
||||
new TypeParameter(type1.typeParameters[i].name);
|
||||
TypeParameterType instantiatorType =
|
||||
new TypeParameterType.forAlphaRenaming(
|
||||
type1.typeParameters[i], instantiator);
|
||||
leftInstance[type1.typeParameters[i]] = instantiatorType;
|
||||
rightInstance[type2.typeParameters[i]] = instantiatorType;
|
||||
_universallyQuantifiedVariables.add(instantiator);
|
||||
}
|
||||
for (int i = 0; i < type1.typeParameters.length; ++i) {
|
||||
DartType left = substitute(type1.typeParameters[i].bound, leftInstance);
|
||||
DartType right =
|
||||
substitute(type2.typeParameters[i].bound, rightInstance);
|
||||
if (!_unify(left, right)) return false;
|
||||
}
|
||||
for (int i = 0; i < type1.positionalParameters.length; ++i) {
|
||||
DartType left = substitute(type1.positionalParameters[i], leftInstance);
|
||||
DartType right =
|
||||
substitute(type2.positionalParameters[i], rightInstance);
|
||||
if (!_unify(left, right)) return false;
|
||||
}
|
||||
for (int i = 0; i < type1.namedParameters.length; ++i) {
|
||||
if (type1.namedParameters[i].name != type2.namedParameters[i].name) {
|
||||
return false;
|
||||
}
|
||||
DartType left = substitute(type1.namedParameters[i].type, leftInstance);
|
||||
DartType right =
|
||||
substitute(type2.namedParameters[i].type, rightInstance);
|
||||
if (!_unify(left, right)) return false;
|
||||
}
|
||||
DartType leftReturn = substitute(type1.returnType, leftInstance);
|
||||
DartType rightReturn = substitute(type2.returnType, rightInstance);
|
||||
if (!_unify(leftReturn, rightReturn)) return false;
|
||||
return true;
|
||||
}
|
||||
if (type1 is TypeParameterType &&
|
||||
type2 is TypeParameterType &&
|
||||
type1.parameter == type2.parameter &&
|
||||
type1.declaredNullability == type2.declaredNullability) {
|
||||
return true;
|
||||
}
|
||||
if (type1 is TypeParameterType &&
|
||||
quantifiedVariables.contains(type1.parameter)) {
|
||||
return _trySubstitution(type1.parameter, type2);
|
||||
}
|
||||
if (type2 is TypeParameterType &&
|
||||
quantifiedVariables.contains(type2.parameter)) {
|
||||
return _trySubstitution(type2.parameter, type1);
|
||||
}
|
||||
return _fail();
|
||||
}
|
||||
|
||||
bool _trySubstitution(TypeParameter variable, DartType type) {
|
||||
if (containsTypeVariable(type, _universallyQuantifiedVariables)) {
|
||||
return _fail();
|
||||
}
|
||||
// Set the plain substitution first and then generate the deep
|
||||
// substitution to detect cycles.
|
||||
substitution[variable] = type;
|
||||
DartType deepSubstitute = substituteDeep(type, substitution);
|
||||
if (deepSubstitute == null) return _fail();
|
||||
substitution[variable] = deepSubstitute;
|
||||
return true;
|
||||
}
|
||||
|
||||
bool _fail() {
|
||||
return success = false;
|
||||
}
|
||||
}
|
||||
|
||||
class _OccurrenceVisitor implements DartTypeVisitor<bool> {
|
||||
final Set<TypeParameter> variables;
|
||||
|
||||
|
||||
@@ -3,9 +3,79 @@
|
||||
// BSD-style license that can be found in the LICENSE file.
|
||||
import 'package:kernel/kernel.dart';
|
||||
import 'type_parser.dart';
|
||||
import 'type_unification_test.dart' show testCases;
|
||||
import 'package:test/test.dart';
|
||||
|
||||
final List<TestCase> testCases = <TestCase>[
|
||||
successCase('List<T>', 'List<String>', {'T': 'String'}),
|
||||
successCase('List<String>', 'List<T>', {'T': 'String'}),
|
||||
successCase('List<T>', 'List<T>', {'T': null}),
|
||||
successCase('List<S>', 'List<T>', {'S': 'T'}),
|
||||
successCase('List<S>', 'List<T>', {'T': 'S'}),
|
||||
successCase(
|
||||
'List<S>', 'List<T>', {'S': 'T', 'T': null}), // Require left bias.
|
||||
failureCase('List<S>', 'List<T>', []),
|
||||
|
||||
failureCase('List<T>', 'T', ['T']),
|
||||
failureCase('List<List<T>>', 'List<T>', ['T']),
|
||||
failureCase('Map<S, T>', 'Map<List<T>, List<S>>', ['T', 'S']),
|
||||
|
||||
failureCase('Map<Map<S,String>, Map<int,S>>',
|
||||
'Map<Map<int, S>, Map<S, String>>', ['S']),
|
||||
successCase('Map<Map<S, int>, Map<int, S>>', 'Map<Map<int, S>, Map<S, int>>',
|
||||
{'S': 'int'}),
|
||||
successCase('Map<Map<S, String>, Map<int, T>>',
|
||||
'Map<Map<int, T>, Map<S, String>>', {'S': 'int', 'T': 'String'}),
|
||||
|
||||
successCase('Map<S, List<T>>', 'Map<T, List<S>>', {'S': 'T'}),
|
||||
successCase('Map<S, T>', 'Map<S, List<S>>', {'T': 'List<S>'}),
|
||||
successCase('Map<S, T>', 'Map<S, List<S>>', {'T': 'List<S>', 'S': null}),
|
||||
successCase('Map<List<S>, T>', 'Map<T, List<S>>', {'T': 'List<S>'}),
|
||||
successCase(
|
||||
'Map<List<S>, T>', 'Map<T, List<S>>', {'T': 'List<S>', 'S': null}),
|
||||
|
||||
successCase('<E>(E) => E', '<T>(T) => T', {}),
|
||||
successCase('<E>(E, S) => E', '<T>(T, int) => T', {'S': 'int'}),
|
||||
failureCase('<E>(E, S) => E', '<T>(T, T) => T', ['S']),
|
||||
successCase(
|
||||
'<E>(E) => <T>(T) => Map<E,T>', '<E>(E) => <T>(T) => Map<E,T>', {}),
|
||||
successCase('<E>(E,_) => E', '<T>(T,_) => T', {}),
|
||||
|
||||
successCase('(x:int,y:String) => int', '(y:String,x:int) => int', {}),
|
||||
successCase('<S,T>(x:S,y:T) => S', '<S,T>(y:T,x:S) => S', {}),
|
||||
successCase('(x:<T>(T)=>T,y:<S>(S)=>S) => int',
|
||||
'(y:<S>(S)=>S,x:<T>(T)=>T) => int', {}),
|
||||
successCase('(x:<T>(T)=>T,y:<S>(S,S,S)=>S) => int',
|
||||
'(y:<S>(S,S,S)=>S,x:<T>(T)=>T) => int', {}),
|
||||
];
|
||||
|
||||
class TestCase {
|
||||
String type1;
|
||||
String type2;
|
||||
Iterable<String> quantifiedVariables;
|
||||
Map<String, String> expectedSubstitution; // Null if unification should fail.
|
||||
|
||||
TestCase.success(this.type1, this.type2, this.expectedSubstitution) {
|
||||
quantifiedVariables = expectedSubstitution.keys;
|
||||
}
|
||||
|
||||
TestCase.fail(this.type1, this.type2, this.quantifiedVariables);
|
||||
|
||||
bool get shouldSucceed => expectedSubstitution != null;
|
||||
|
||||
String toString() => '∃ ${quantifiedVariables.join(',')}. $type1 = $type2';
|
||||
}
|
||||
|
||||
TestCase successCase(String type1, String type2, Map<String, String> expected,
|
||||
{bool debug: false}) {
|
||||
return new TestCase.success(type1, type2, expected);
|
||||
}
|
||||
|
||||
TestCase failureCase(
|
||||
String type1, String type2, List<String> quantifiedVariables,
|
||||
{bool debug: false}) {
|
||||
return new TestCase.fail(type1, type2, quantifiedVariables);
|
||||
}
|
||||
|
||||
void checkHashCodeEquality(DartType type1, DartType type2) {
|
||||
if (type1 == type2 && type1.hashCode != type2.hashCode) {
|
||||
fail('Equal types with different hash codes: $type1 and $type2');
|
||||
|
||||
@@ -1,10 +1,11 @@
|
||||
// Copyright (c) 2016, the Dart project authors. Please see the AUTHORS file
|
||||
// for details. All rights reserved. Use of this source code is governed by a
|
||||
// BSD-style license that can be found in the LICENSE file.
|
||||
|
||||
import 'package:kernel/kernel.dart';
|
||||
import 'package:kernel/type_algebra.dart';
|
||||
import 'type_parser.dart';
|
||||
import 'type_unification_test.dart' show testCases;
|
||||
import 'type_hashcode_test.dart' show testCases;
|
||||
import 'package:test/test.dart';
|
||||
|
||||
checkType(DartType type) {
|
||||
|
||||
@@ -1,140 +0,0 @@
|
||||
// Copyright (c) 2016, the Dart project authors. Please see the AUTHORS file
|
||||
// for details. All rights reserved. Use of this source code is governed by a
|
||||
// BSD-style license that can be found in the LICENSE file.
|
||||
import 'package:kernel/type_algebra.dart';
|
||||
import 'package:test/test.dart';
|
||||
import 'type_parser.dart';
|
||||
import 'dart:io';
|
||||
|
||||
final List<TestCase> testCases = <TestCase>[
|
||||
successCase('List<T>', 'List<String>', {'T': 'String'}),
|
||||
successCase('List<String>', 'List<T>', {'T': 'String'}),
|
||||
successCase('List<T>', 'List<T>', {'T': null}),
|
||||
successCase('List<S>', 'List<T>', {'S': 'T'}),
|
||||
successCase('List<S>', 'List<T>', {'T': 'S'}),
|
||||
successCase(
|
||||
'List<S>', 'List<T>', {'S': 'T', 'T': null}), // Require left bias.
|
||||
failureCase('List<S>', 'List<T>', []),
|
||||
|
||||
failureCase('List<T>', 'T', ['T']),
|
||||
failureCase('List<List<T>>', 'List<T>', ['T']),
|
||||
failureCase('Map<S, T>', 'Map<List<T>, List<S>>', ['T', 'S']),
|
||||
|
||||
failureCase('Map<Map<S,String>, Map<int,S>>',
|
||||
'Map<Map<int, S>, Map<S, String>>', ['S']),
|
||||
successCase('Map<Map<S, int>, Map<int, S>>', 'Map<Map<int, S>, Map<S, int>>',
|
||||
{'S': 'int'}),
|
||||
successCase('Map<Map<S, String>, Map<int, T>>',
|
||||
'Map<Map<int, T>, Map<S, String>>', {'S': 'int', 'T': 'String'}),
|
||||
|
||||
successCase('Map<S, List<T>>', 'Map<T, List<S>>', {'S': 'T'}),
|
||||
successCase('Map<S, T>', 'Map<S, List<S>>', {'T': 'List<S>'}),
|
||||
successCase('Map<S, T>', 'Map<S, List<S>>', {'T': 'List<S>', 'S': null}),
|
||||
successCase('Map<List<S>, T>', 'Map<T, List<S>>', {'T': 'List<S>'}),
|
||||
successCase(
|
||||
'Map<List<S>, T>', 'Map<T, List<S>>', {'T': 'List<S>', 'S': null}),
|
||||
|
||||
successCase('<E>(E) => E', '<T>(T) => T', {}),
|
||||
successCase('<E>(E, S) => E', '<T>(T, int) => T', {'S': 'int'}),
|
||||
failureCase('<E>(E, S) => E', '<T>(T, T) => T', ['S']),
|
||||
successCase(
|
||||
'<E>(E) => <T>(T) => Map<E,T>', '<E>(E) => <T>(T) => Map<E,T>', {}),
|
||||
successCase('<E>(E,_) => E', '<T>(T,_) => T', {}),
|
||||
|
||||
successCase('(x:int,y:String) => int', '(y:String,x:int) => int', {}),
|
||||
successCase('<S,T>(x:S,y:T) => S', '<S,T>(y:T,x:S) => S', {}),
|
||||
successCase('(x:<T>(T)=>T,y:<S>(S)=>S) => int',
|
||||
'(y:<S>(S)=>S,x:<T>(T)=>T) => int', {}),
|
||||
successCase('(x:<T>(T)=>T,y:<S>(S,S,S)=>S) => int',
|
||||
'(y:<S>(S,S,S)=>S,x:<T>(T)=>T) => int', {}),
|
||||
];
|
||||
|
||||
class TestCase {
|
||||
String type1;
|
||||
String type2;
|
||||
Iterable<String> quantifiedVariables;
|
||||
Map<String, String> expectedSubstitution; // Null if unification should fail.
|
||||
|
||||
TestCase.success(this.type1, this.type2, this.expectedSubstitution) {
|
||||
quantifiedVariables = expectedSubstitution.keys;
|
||||
}
|
||||
|
||||
TestCase.fail(this.type1, this.type2, this.quantifiedVariables);
|
||||
|
||||
bool get shouldSucceed => expectedSubstitution != null;
|
||||
|
||||
String toString() => '∃ ${quantifiedVariables.join(',')}. $type1 = $type2';
|
||||
}
|
||||
|
||||
TestCase successCase(String type1, String type2, Map<String, String> expected,
|
||||
{bool debug: false}) {
|
||||
return new TestCase.success(type1, type2, expected);
|
||||
}
|
||||
|
||||
TestCase failureCase(
|
||||
String type1, String type2, List<String> quantifiedVariables,
|
||||
{bool debug: false}) {
|
||||
return new TestCase.fail(type1, type2, quantifiedVariables);
|
||||
}
|
||||
|
||||
int numFailures = 0;
|
||||
|
||||
void reportFailure(TestCase testCase, String message) {
|
||||
++numFailures;
|
||||
fail('$message in `$testCase`');
|
||||
}
|
||||
|
||||
main() {
|
||||
for (TestCase testCase in testCases) {
|
||||
test('$testCase', () {
|
||||
var env = new LazyTypeEnvironment();
|
||||
var type1 = env.parse(testCase.type1);
|
||||
var type2 = env.parse(testCase.type2);
|
||||
var quantifiedVariables =
|
||||
testCase.quantifiedVariables.map(env.getTypeParameter).toSet();
|
||||
var substitution = unifyTypes(type1, type2, quantifiedVariables);
|
||||
if (testCase.shouldSucceed) {
|
||||
if (substitution == null) {
|
||||
reportFailure(testCase, 'Unification failed');
|
||||
} else {
|
||||
for (var key in testCase.expectedSubstitution.keys) {
|
||||
var typeParameter = env.getTypeParameter(key);
|
||||
if (testCase.expectedSubstitution[key] == null) {
|
||||
if (substitution.containsKey(key)) {
|
||||
var actualType = substitution[typeParameter];
|
||||
reportFailure(
|
||||
testCase,
|
||||
'Incorrect substitution '
|
||||
'`$key = $actualType` should be unbound');
|
||||
}
|
||||
} else {
|
||||
var expectedType = env.parse(testCase.expectedSubstitution[key]);
|
||||
var actualType = substitution[typeParameter];
|
||||
if (actualType != expectedType) {
|
||||
reportFailure(
|
||||
testCase,
|
||||
'Incorrect substitution '
|
||||
'`$key = $actualType` should be `$key = $expectedType`');
|
||||
}
|
||||
}
|
||||
}
|
||||
var boundTypeVariables = testCase.expectedSubstitution.keys
|
||||
.where((name) => testCase.expectedSubstitution[name] != null);
|
||||
if (substitution.length != boundTypeVariables.length) {
|
||||
reportFailure(
|
||||
testCase,
|
||||
'Substituted `${substitution.keys.join(',')}` '
|
||||
'but should only substitute `${boundTypeVariables.join(',')}`');
|
||||
}
|
||||
}
|
||||
} else {
|
||||
if (substitution != null) {
|
||||
reportFailure(testCase, 'Unification was supposed to fail');
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
if (numFailures > 0) {
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user