Simplify the exhaustiveness prototype some.

munificent · munificent · commit 0cee6c52a191 · 2022-03-25T19:31:58.000-07:00
Instead of fully defining intersection, just define whether the
intersection is empty, which is all we need.
diff --git a/working/0546-patterns/exhaustiveness_prototype/lib/intersect_empty.dart b/working/0546-patterns/exhaustiveness_prototype/lib/intersect_empty.dart
@@ -0,0 +1,59 @@
+// Copyright (c) 2022, 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:exhaustiveness_prototype/static_type.dart';
+
+import 'space.dart';
+
+/// Calculates whether the intersection of [left] and [right] is empty.
+///
+/// This is used to tell if two field spaces on a pair of spaces being
+/// subtracted have no common values.
+bool intersectEmpty(Space left, Space right) {
+  // The intersection with an empty space is always empty.
+  if (left == Space.empty) return true;
+  if (right == Space.empty) return true;
+
+  // The intersection of a union is empty if all of the arms are.
+  if (left is UnionSpace) {
+    return left.arms.every((arm) => intersectEmpty(arm, right));
+  }
+
+  if (right is UnionSpace) {
+    return right.arms.every((arm) => intersectEmpty(left, arm));
+  }
+
+  // Otherwise, we're intersecting two [ExtractSpaces].
+  return _intersectExtracts(left as ExtractSpace, right as ExtractSpace);
+}
+
+/// Returns the interaction of extract spaces [left] and [right].
+bool _intersectExtracts(ExtractSpace left, ExtractSpace right) {
+  if (intersectTypes(left.type, right.type)) return true;
+
+  // Recursively intersect the fields.
+  var fieldNames = {...left.fields.keys, ...right.fields.keys}.toList();
+  for (var name in fieldNames) {
+    // If the fields are disjoint, then the entire space will have no values.
+    if (_intersectFields(left.fields[name], right.fields[name])) return true;
+  }
+
+  return false;
+}
+
+bool _intersectFields(Space? left, Space? right) {
+  if (left == null) return right! == Space.empty;
+  if (right == null) return left == Space.empty;
+  return intersectEmpty(left, right);
+}
+
+/// Returns true if the intersection of two static types [left] and [right] is
+/// empty.
+bool intersectTypes(StaticType left, StaticType right) {
+  // If one type is a subtype, the subtype is the intersection.
+  if (left.isSubtypeOf(right)) return false;
+  if (right.isSubtypeOf(left)) return false;
+
+  // Unrelated types.
+  return true;
+}
diff --git a/working/0546-patterns/exhaustiveness_prototype/lib/space.dart b/working/0546-patterns/exhaustiveness_prototype/lib/space.dart
@@ -9,6 +9,7 @@ import 'static_type.dart';
 
 abstract class Space {
   static final empty = _EmptySpace._();
+  static final top = Space(StaticType.top);
 
   factory Space.union(List<Space> arms) {
     // Simplify the arms if possible.
@@ -100,7 +101,7 @@ class ExtractSpace extends Space {
 
   @override
   String toString() {
-    if (fields.isEmpty && type == StaticType.top) return '()';
+    if (isTop) return '()';
 
     // If there are no fields, just show the type.
     if (fields.isEmpty) return type.name;
diff --git a/working/0546-patterns/exhaustiveness_prototype/lib/subtract.dart b/working/0546-patterns/exhaustiveness_prototype/lib/subtract.dart
@@ -1,7 +1,7 @@
 // Copyright (c) 2022, 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:exhaustiveness_prototype/intersect.dart';
+import 'package:exhaustiveness_prototype/intersect_empty.dart';
 import 'package:exhaustiveness_prototype/static_type.dart';
 
 import 'space.dart';
@@ -61,62 +61,55 @@ List<Space> _subtractExtractAtType(StaticType type, ExtractSpace left,
   // and keep all of the current fields.
   if (!type.isSubtypeOf(right.type)) return [Space(type, left.fields)];
 
+  // Infer any fields that appear in one space and not the other.
+  var leftFields = <String, Space>{};
+  var rightFields = <String, Space>{};
+  for (var name in fieldNames) {
+    // If the right space matches on a field that the left doesn't have, infer
+    // it from the static type of the field. That contains the same set of
+    // values as having no field at all.
+    leftFields[name] = left.fields[name] ?? Space(type.fields[name]!);
+
+    // If the left matches on a field that the right doesn't have, infer top
+    // for the right field since the right will accept any of left's values for
+    // that field.
+    rightFields[name] = right.fields[name] ?? Space.top;
+  }
+
   // If any pair of fields have no overlapping values, then no overall value
   // that matches the left space will also match the right space. So the right
   // space doesn't subtract anything and we keep the left space as-is.
   for (var name in fieldNames) {
-    var leftField = left.fields[name];
-    var rightField = right.fields[name];
-
-    if (leftField != null &&
-        rightField != null &&
-        intersect(leftField, rightField) == Space.empty) {
+    if (intersectEmpty(leftFields[name]!, rightFields[name]!)) {
       return [Space(type, left.fields)];
     }
   }
 
   // If all the right's fields strictly cover all of the left's, then the
   // right completely subtracts this type and nothing remains.
-  if (_isLeftSubspace(type, fieldNames, left.fields, right.fields)) {
+  if (_isLeftSubspace(type, fieldNames, leftFields, rightFields)) {
     return const [];
   }
 
   // The right side is a supertype but its fields don't totally cover, so
-  // handle each of them individually. This is equation 8.3 but more complex
-  // to handle the fact that records may choose to match arbitrary subsets of
-  // the available fields.
+  // handle each of them individually.
 
   // Walk the fields and see which ones are modified by the right-hand fields.
   var fixed = <String, Space>{};
   var changedLeft = <String, Space>{};
   var changedDifference = <String, Space>{};
   for (var name in fieldNames) {
-    var leftField = left.fields[name];
-    var rightField = right.fields[name];
-
-    // To subtract a right field, we need a baseline left field to compare
-    // it to. If there isn't one, infer a left field that matches all values
-    // of its type.
-    leftField ??= Space(type.fields[name]!);
-
-    if (rightField == null) {
-      // If we have a left field that constrains but aren't subtracting
-      // anything from it, just keep the constraint.
-      fixed[name] = leftField;
+    var difference = subtract(leftFields[name]!, rightFields[name]!);
+    if (difference == Space.empty) {
+      // The right field accepts all the values that the left field accepts, so
+      // keep the left field as it is.
+      fixed[name] = leftFields[name]!;
+    } else if (difference.isTop) {
+      // If the resulting field matches everything, simply discard it since
+      // it's equivalent to omitting the field.
     } else {
-      var difference = subtract(leftField, rightField);
-      if (difference == Space.empty) {
-        // TODO: This comment isn't right.
-        // The left and right fields don't overlap, so there's no need to
-        // consider this empty case since it will match nothing.
-        fixed[name] = leftField;
-      } else if (difference.isTop) {
-        // Don't bother keeping a field that matches everything.
-        // TODO: When does this get reached?
-      } else {
-        changedLeft[name] = leftField;
-        changedDifference[name] = difference;
-      }
+      changedLeft[name] = leftFields[name]!;
+      changedDifference[name] = difference;
     }
   }
 
@@ -150,23 +143,10 @@ List<Space> _subtractExtractAtType(StaticType type, ExtractSpace left,
 /// corresponding field in [rightFields].
 bool _isLeftSubspace(StaticType leftType, List<String> fieldNames,
     Map<String, Space> leftFields, Map<String, Space> rightFields) {
-  // 8.1: If this type is a subtype of the right type, and all of the fields
-  // on the left are covered by the fields on the right, then the right hand
-  // space covers the left space entirely.
   for (var name in fieldNames) {
-    var leftField = leftFields[name];
-    var rightField = rightFields[name];
-
-    // If there is no right field, it definitely covers all values matched
-    // by the left field.
-    if (rightField == null) continue;
-
-    // If there is no left field, infer it from the type on the left. This is
-    // safe to do because we know the left type is a subtype of the right and
-    // thus the field will exist.
-    leftField ??= Space(leftType.fields[name]!);
-
-    if (subtract(leftField, rightField) != Space.empty) return false;
+    if (subtract(leftFields[name]!, rightFields[name]!) != Space.empty) {
+      return false;
+    }
   }
 
   // If we get here, every field covered.
@@ -176,28 +156,13 @@ bool _isLeftSubspace(StaticType leftType, List<String> fieldNames,
 /// Recursively replaces [left] with a union of its sealed subtypes as long as
 /// doing so enables it to more precisely match against [right].
 List<StaticType> expandType(StaticType left, StaticType right) {
-  // If we've reached the type, stop.
-  if (left.isSubtypeOf(right)) return [left];
-
-  if (!left.isSealed) return [left];
-
-  // If expanding left into its subtypes won't get closer to right, then don't.
-  if (!right.isSubtypeOf(left)) return [left];
-
-  // If we remove the restriction that a type can only be a direct subtype of
-  // one sealed supertype, then the above check needs to be smarter. Consider:
-  //     (A)
-  //     / \
-  //   (B) (C)
-  //   / \ / \
-  //  D   E   F
-  //
-  // Here, `expandType(B, F)` should return [D, E, F] because even though B and
-  // F aren't supertypes of each other, they have a shared supertype in a sealed
-  // family.
-
-  // Expand [left] recursively to reach down to right.
-  return {
-    for (var subtype in left.subtypes) ...expandType(subtype, right),
-  }.toList();
+  // If [left] is a sealed supertype and [right] is in its subtype hierarchy,
+  // then expand out the subtypes (recursively) to more precisely match [right].
+  if (left.isSealed && left != right && right.isSubtypeOf(left)) {
+    return {
+      for (var subtype in left.subtypes) ...expandType(subtype, right),
+    }.toList();
+  }
+
+  return [left];
 }
diff --git a/working/0546-patterns/exhaustiveness_prototype/test/intersect_empty_test.dart b/working/0546-patterns/exhaustiveness_prototype/test/intersect_empty_test.dart
@@ -0,0 +1,78 @@
+// Copyright (c) 2022, 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:exhaustiveness_prototype/intersect_empty.dart';
+import 'package:exhaustiveness_prototype/space.dart';
+import 'package:exhaustiveness_prototype/static_type.dart';
+import 'package:test/test.dart';
+
+import 'utils.dart';
+
+void main() {
+  //   (A)
+  //   / \
+  //  B   C
+  var a = StaticType('A', isSealed: true);
+  var b = StaticType('B', inherits: [a]);
+  var c = StaticType('C', inherits: [a]);
+
+  Space A({StaticType? x, StaticType? y, StaticType? z}) => ty(
+      a, {if (x != null) 'x': x, if (y != null) 'y': y, if (z != null) 'z': z});
+  Space B({StaticType? x, StaticType? y, StaticType? z}) => ty(
+      b, {if (x != null) 'x': x, if (y != null) 'y': y, if (z != null) 'z': z});
+  Space C({StaticType? x, StaticType? y, StaticType? z}) => ty(
+      c, {if (x != null) 'x': x, if (y != null) 'y': y, if (z != null) 'z': z});
+
+  test('records', () {
+    expectIntersectEmpty(rec(x: a, y: a), rec(x: a, y: a), isFalse);
+    expectIntersectEmpty(rec(x: a, y: a), rec(x: a), isFalse);
+    expectIntersectEmpty(
+        rec(w: a, x: a), rec(y: a, z: a), isFalse);
+    expectIntersectEmpty(rec(w: a, x: a, y: a), rec(x: a, y: a, z: a),
+        isFalse);
+  });
+
+  test('types', () {
+    // Note: More comprehensive tests under intersect_types_test.dart.
+    expectIntersectEmpty(a, a, isFalse);
+    expectIntersectEmpty(a, b, isFalse);
+    expectIntersectEmpty(a, c, isFalse);
+    expectIntersectEmpty(b, c, isTrue);
+  });
+
+  test('field types', () {
+    expectIntersectEmpty(rec(x: a, y: b), rec(x: b, y: a), isFalse);
+    expectIntersectEmpty(rec(x: b), rec(x: c), isTrue);
+  });
+
+  test('types and fields', () {
+    expectIntersectEmpty(A(x: a), A(x: a), isFalse);
+    expectIntersectEmpty(A(x: a), A(x: b), isFalse);
+    expectIntersectEmpty(A(x: b), A(x: c), isTrue);
+
+    expectIntersectEmpty(A(x: a), B(x: a), isFalse);
+    expectIntersectEmpty(A(x: a), B(x: b), isFalse);
+    expectIntersectEmpty(A(x: b), B(x: c), isTrue);
+
+    expectIntersectEmpty(B(x: a), A(x: a), isFalse);
+    expectIntersectEmpty(B(x: a), A(x: b), isFalse);
+    expectIntersectEmpty(B(x: b), A(x: c), isTrue);
+
+    expectIntersectEmpty(B(x: a), B(x: a), isFalse);
+    expectIntersectEmpty(B(x: a), B(x: b), isFalse);
+    expectIntersectEmpty(B(x: b), B(x: c), isTrue);
+
+    expectIntersectEmpty(B(x: a), C(x: a), isTrue);
+    expectIntersectEmpty(B(x: a), C(x: b), isTrue);
+    expectIntersectEmpty(B(x: b), C(x: c), isTrue);
+  });
+}
+
+void expectIntersectEmpty(Object left, Object right, Matcher expected) {
+  var leftSpace = parseSpace(left);
+  var rightSpace = parseSpace(right);
+
+  // Intersection is symmetric so try both directions.
+  expect(intersectEmpty(leftSpace, rightSpace), expected);
+  expect(intersectEmpty(rightSpace, leftSpace), expected);
+}
