diff --git a/pkg/kernel/lib/type_algebra.dart b/pkg/kernel/lib/type_algebra.dart index 4321badfa8c..4ec2480104a 100644 --- a/pkg/kernel/lib/type_algebra.dart +++ b/pkg/kernel/lib/type_algebra.dart @@ -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` with `List`, 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` cannot be unified with `Set`. -/// - infinite types: e.g. `T` cannot be unified with `List` because it -/// would create the infinite type `List>>`. -Map unifyTypes( - DartType type1, DartType type2, Set 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 substitution = {}; - - /// Variables that may be assigned freely in order to obtain unification. - /// - /// These are sometimes referred to as existentially quantified variables. - final Set 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, S) => E = (E, E) => E - /// - /// That is, we must choose `S` such that the generic function type - /// `(E, S) => E` becomes `(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 _universallyQuantifiedVariables = - new Set(); - - 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. (fn1) = (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 leftInstance = {}; - Map rightInstance = {}; - 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 { final Set variables; diff --git a/pkg/kernel/test/type_hashcode_test.dart b/pkg/kernel/test/type_hashcode_test.dart index 468deb6840a..b988507249b 100644 --- a/pkg/kernel/test/type_hashcode_test.dart +++ b/pkg/kernel/test/type_hashcode_test.dart @@ -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 testCases = [ + successCase('List', 'List', {'T': 'String'}), + successCase('List', 'List', {'T': 'String'}), + successCase('List', 'List', {'T': null}), + successCase('List', 'List', {'S': 'T'}), + successCase('List', 'List', {'T': 'S'}), + successCase( + 'List', 'List', {'S': 'T', 'T': null}), // Require left bias. + failureCase('List', 'List', []), + + failureCase('List', 'T', ['T']), + failureCase('List>', 'List', ['T']), + failureCase('Map', 'Map, List>', ['T', 'S']), + + failureCase('Map, Map>', + 'Map, Map>', ['S']), + successCase('Map, Map>', 'Map, Map>', + {'S': 'int'}), + successCase('Map, Map>', + 'Map, Map>', {'S': 'int', 'T': 'String'}), + + successCase('Map>', 'Map>', {'S': 'T'}), + successCase('Map', 'Map>', {'T': 'List'}), + successCase('Map', 'Map>', {'T': 'List', 'S': null}), + successCase('Map, T>', 'Map>', {'T': 'List'}), + successCase( + 'Map, T>', 'Map>', {'T': 'List', 'S': null}), + + successCase('(E) => E', '(T) => T', {}), + successCase('(E, S) => E', '(T, int) => T', {'S': 'int'}), + failureCase('(E, S) => E', '(T, T) => T', ['S']), + successCase( + '(E) => (T) => Map', '(E) => (T) => Map', {}), + successCase('(E,_) => E', '(T,_) => T', {}), + + successCase('(x:int,y:String) => int', '(y:String,x:int) => int', {}), + successCase('(x:S,y:T) => S', '(y:T,x:S) => S', {}), + successCase('(x:(T)=>T,y:(S)=>S) => int', + '(y:(S)=>S,x:(T)=>T) => int', {}), + successCase('(x:(T)=>T,y:(S,S,S)=>S) => int', + '(y:(S,S,S)=>S,x:(T)=>T) => int', {}), +]; + +class TestCase { + String type1; + String type2; + Iterable quantifiedVariables; + Map 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 expected, + {bool debug: false}) { + return new TestCase.success(type1, type2, expected); +} + +TestCase failureCase( + String type1, String type2, List 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'); diff --git a/pkg/kernel/test/type_substitution_identity_test.dart b/pkg/kernel/test/type_substitution_identity_test.dart index d07da2adc3c..d8fabbd1317 100644 --- a/pkg/kernel/test/type_substitution_identity_test.dart +++ b/pkg/kernel/test/type_substitution_identity_test.dart @@ -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) { diff --git a/pkg/kernel/test/type_unification_test.dart b/pkg/kernel/test/type_unification_test.dart deleted file mode 100644 index 2e79fdb59e3..00000000000 --- a/pkg/kernel/test/type_unification_test.dart +++ /dev/null @@ -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 testCases = [ - successCase('List', 'List', {'T': 'String'}), - successCase('List', 'List', {'T': 'String'}), - successCase('List', 'List', {'T': null}), - successCase('List', 'List', {'S': 'T'}), - successCase('List', 'List', {'T': 'S'}), - successCase( - 'List', 'List', {'S': 'T', 'T': null}), // Require left bias. - failureCase('List', 'List', []), - - failureCase('List', 'T', ['T']), - failureCase('List>', 'List', ['T']), - failureCase('Map', 'Map, List>', ['T', 'S']), - - failureCase('Map, Map>', - 'Map, Map>', ['S']), - successCase('Map, Map>', 'Map, Map>', - {'S': 'int'}), - successCase('Map, Map>', - 'Map, Map>', {'S': 'int', 'T': 'String'}), - - successCase('Map>', 'Map>', {'S': 'T'}), - successCase('Map', 'Map>', {'T': 'List'}), - successCase('Map', 'Map>', {'T': 'List', 'S': null}), - successCase('Map, T>', 'Map>', {'T': 'List'}), - successCase( - 'Map, T>', 'Map>', {'T': 'List', 'S': null}), - - successCase('(E) => E', '(T) => T', {}), - successCase('(E, S) => E', '(T, int) => T', {'S': 'int'}), - failureCase('(E, S) => E', '(T, T) => T', ['S']), - successCase( - '(E) => (T) => Map', '(E) => (T) => Map', {}), - successCase('(E,_) => E', '(T,_) => T', {}), - - successCase('(x:int,y:String) => int', '(y:String,x:int) => int', {}), - successCase('(x:S,y:T) => S', '(y:T,x:S) => S', {}), - successCase('(x:(T)=>T,y:(S)=>S) => int', - '(y:(S)=>S,x:(T)=>T) => int', {}), - successCase('(x:(T)=>T,y:(S,S,S)=>S) => int', - '(y:(S,S,S)=>S,x:(T)=>T) => int', {}), -]; - -class TestCase { - String type1; - String type2; - Iterable quantifiedVariables; - Map 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 expected, - {bool debug: false}) { - return new TestCase.success(type1, type2, expected); -} - -TestCase failureCase( - String type1, String type2, List 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); - } -}