[patterns] Add prototype exhaustiveness checker.

Author: munificent

working/0546-patterns/exhaustiveness_prototype/README.md

@@ -0,0 +1 @@
+This is a prototype implementation of the exhaustiveness checking algorithm.

working/0546-patterns/exhaustiveness_prototype/analysis_options.yaml

@@ -0,0 +1,31 @@
+include: package:lints/recommended.yaml
+linter:
+  rules:
+  - avoid_null_checks_in_equality_operators
+  - avoid_unused_constructor_parameters
+  - await_only_futures
+  - camel_case_types
+  - cancel_subscriptions
+  - comment_references
+  - constant_identifier_names
+  - control_flow_in_finally
+  - directives_ordering
+  - empty_statements
+  - hash_and_equals
+  - implementation_imports
+  - iterable_contains_unrelated_type
+  - library_names
+  - library_prefixes
+  - list_remove_unrelated_type
+  - non_constant_identifier_names
+  - overridden_fields
+  - package_api_docs
+  - package_names
+  - package_prefixed_library_names
+  - prefer_final_fields
+  - prefer_generic_function_type_aliases
+  - prefer_typing_uninitialized_variables
+  - test_types_in_equals
+  - throw_in_finally
+  - unnecessary_brace_in_string_interps
+  - unrelated_type_equality_checks

working/0546-patterns/exhaustiveness_prototype/lib/equal.dart

@@ -0,0 +1,65 @@
+// 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 'space.dart';
+
+/// Returns `true` if [left] and [right] are equivalent spaces.
+///
+/// Equality is defined purely structurally/syntactically.
+bool equal(Space left, Space right) {
+  if (left == right) return true;
+
+  // Empty is only equal to itself (and will get caught by the previous check).
+  if (left == Space.empty) return false;
+  if (right == Space.empty) return false;
+
+  if (left is UnionSpace && right is UnionSpace) {
+    return _equalUnions(left, right);
+  }
+
+  if (left is ExtractSpace && right is ExtractSpace) {
+    return _equalExtracts(left, right);
+  }
+
+  // If we get here, one is a union and one is an extract.
+  return false;
+}
+
+/// Returns `true` if [left] and [right] contain equal arms in any order.
+///
+/// Assumes that all duplicates have already been removed from each union.
+bool _equalUnions(UnionSpace left, UnionSpace right) {
+  if (left.arms.length != right.arms.length) return false;
+
+  /// For each left arm, should find an equal right arm.
+  for (var leftArm in left.arms) {
+    var found = false;
+    for (var rightArm in right.arms) {
+      if (equal(leftArm, rightArm)) {
+        found = true;
+        break;
+      }
+    }
+    if (!found) return false;
+  }
+
+  return true;
+}
+
+/// Returns `true` if [left] and [right] have the same type and the same fields
+/// with equal subspaces.
+bool _equalExtracts(ExtractSpace left, ExtractSpace right) {
+  // Must have the same type.
+  if (left.type != right.type) return false;
+
+  // And the same fields.
+  var fields = {...left.fields.keys, ...right.fields.keys};
+  if (left.fields.length != fields.length) return false;
+  if (right.fields.length != fields.length) return false;
+
+  for (var field in fields) {
+    if (!equal(left.fields[field]!, right.fields[field]!)) return false;
+  }
+
+  return true;
+}

working/0546-patterns/exhaustiveness_prototype/lib/exhaustive.dart

@@ -0,0 +1,48 @@
+// 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 'space.dart';
+import 'static_type.dart';
+import 'subtract.dart';
+
+/// Returns `true` if [cases] exhaustively covers all possible values of
+/// [value].
+///
+/// This is defined simply in terms of subtraction and unions: [cases] is a
+/// union space, and it's exhaustive if subtracting it from [value] leaves
+/// nothing.
+bool isExhaustive(Space value, List<Space> cases) {
+  return subtract(value, Space.union(cases)) == Space.empty;
+}
+
+/// Checks the [cases] representing a series of switch cases to see if they
+/// exhaustively cover all possible values of the matched [valueType]. Also
+/// checks to see if any case can't be matched because it's covered by previous
+/// cases.
+///
+/// Returns a string containing any unreachable case or non-exhaustive match
+/// errors. Returns an empty string if all cases are reachable and the cases
+/// are exhaustive.
+String reportErrors(StaticType valueType, List<Space> cases) {
+  var errors = <String>[];
+
+  var remaining = Space(valueType);
+  for (var i = 0; i < cases.length; i++) {
+    // See if this case is covered by previous ones.
+    if (i > 0) {
+      var previous = Space.union(cases.sublist(0, i));
+      if (subtract(cases[i], previous) == Space.empty) {
+        errors.add('Case #${i + 1} ${cases[i]} is covered by $previous.');
+      }
+    }
+
+    remaining = subtract(remaining, cases[i]);
+  }
+
+  if (remaining != Space.empty) {
+    errors.add(
+        '$valueType is not exhaustively matched by ${Space.union(cases)}.');
+  }
+
+  return errors.join('\n');
+}

working/0546-patterns/exhaustiveness_prototype/lib/intersect.dart

@@ -0,0 +1,88 @@
+// 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 the intersection of [left] and [right].
+///
+/// This is used to tell if two field spaces on a pair of spaces being
+/// subtracted have no common values.
+Space intersect(Space left, Space right) {
+  // The intersection with an empty space is always empty.
+  if (left == Space.empty) return Space.empty;
+  if (right == Space.empty) return Space.empty;
+
+  // The intersection of a union is the union of the intersections of its arms.
+  if (left is UnionSpace) {
+    return Space.union(left.arms.map((arm) => intersect(arm, right)).toList());
+  }
+
+  if (right is UnionSpace) {
+    return Space.union(right.arms.map((arm) => intersect(left, arm)).toList());
+  }
+
+  // Otherwise, we're intersecting two [ExtractSpaces].
+  return _intersectExtracts(left as ExtractSpace, right as ExtractSpace);
+}
+
+/// Returns the interaction of extract spaces [left] and [right].
+Space _intersectExtracts(ExtractSpace left, ExtractSpace right) {
+  var type = intersectTypes(left.type, right.type);
+
+  // If the types are disjoint, the intersection is empty.
+  if (type == null) return Space.empty;
+
+  // Recursively intersect the fields.
+  var fieldNames = {...left.fields.keys, ...right.fields.keys}.toList();
+
+  // Sorting isn't needed for correctness, just to make the tests less brittle.
+  fieldNames.sort();
+
+  var fields = <String, Space>{};
+  for (var name in fieldNames) {
+    var field = _intersectFields(left.fields[name], right.fields[name]);
+
+    // If the fields are disjoint, then the entire space will have no values.
+    if (field == Space.empty) return Space.empty;
+    fields[name] = field;
+  }
+
+  return Space(type, fields);
+}
+
+Space _intersectFields(Space? left, Space? right) {
+  if (left == null) return right!;
+  if (right == null) return left;
+  return intersect(left, right);
+}
+
+/// Returns the intersection of two static types [left] and [right].
+///
+/// Returns `null` if the intersection is empty.
+StaticType? intersectTypes(StaticType left, StaticType right) {
+  // If one type is a subtype, the subtype is the intersection.
+  if (left.isSubtypeOf(right)) return left;
+  if (right.isSubtypeOf(left)) return right;
+
+  // If we allow sealed types to share subtypes, then this will need to be more
+  // sophisticated. Here:
+  //
+  //   (A) (B)
+  //   / \ / \
+  //  C   D   E
+  //
+  // The intersection of A and B should be D. Here:
+  //
+  //  (A)   (B)
+  //   | \  / |
+  //   |\ \/ /|
+  //   | \/\/ |
+  //   C D  E F
+  //
+  // It should be D, E.
+
+  // Unrelated types.
+  return null;
+}

working/0546-patterns/exhaustiveness_prototype/lib/space.dart

@@ -0,0 +1,147 @@
+// 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/equal.dart';
+
+import 'static_type.dart';
+
+// TODO: List spaces.
+
+abstract class Space {
+  static final empty = _EmptySpace._();
+
+  factory Space.union(List<Space> arms) {
+    // Simplify the arms if possible.
+    var allArms = <Space>[];
+
+    void addSpace(Space space) {
+      // Discard duplicate arms. Duplicates can appear when working through a
+      // series of cases that destructure multiple fields with different types.
+      // Discarding the duplicates isn't necessary for correctness (a union with
+      // redundant arms contains the same set of values), but improves
+      // performance greatly. In the "sealed subtypes large T with all cases"
+      // test, you end up with a union containing 2520 arms, 2488 are
+      // duplicates. With this check, the largest union has only 5 arms.
+      //
+      // This is O(n^2) since we define only equality on spaces, but a real
+      // implementation would likely define hash code too and then simply
+      // create a hash set to merge duplicates in O(n) time.
+      for (var existing in allArms) {
+        if (equal(existing, space)) return;
+      }
+
+      allArms.add(space);
+    }
+
+    for (var space in arms) {
+      // Discard empty arms.
+      if (space == empty) continue;
+
+      // Flatten unions. We don't need to flatten recursively since we always
+      // go through this constructor to create unions. A UnionSpace will never
+      // contain UnionSpaces.
+      if (space is UnionSpace) {
+        for (var arm in space.arms) addSpace(arm);
+      } else {
+        addSpace(space);
+      }
+    }
+
+    if (allArms.isEmpty) return empty;
+    if (allArms.length == 1) return allArms.first;
+    return UnionSpace._(allArms);
+  }
+
+  factory Space(StaticType type, [Map<String, Space> fields = const {}]) =>
+      ExtractSpace._(type, fields);
+
+  factory Space.record([Map<String, Space> fields = const {}]) =>
+      Space(StaticType.top, fields);
+
+  Space._();
+
+  /// An untyped record space with no fields matches all values and thus isn't
+  /// very useful.
+  bool get isTop => false;
+}
+
+/// A union of spaces. The space A|B contains all of the values of A and B.
+class UnionSpace extends Space {
+  final List<Space> arms;
+
+  UnionSpace._(this.arms) : super._() {
+    assert(arms.length > 1);
+  }
+
+  @override
+  String toString() => arms.join('|');
+}
+
+/// The main space for matching types and destructuring.
+///
+/// It has a type which determines the type of values it contains. The type may
+/// be [StaticType.top] to indicate that it doesn't filter by type.
+///
+/// It may also contain zero or more named fields. The space then only contains
+/// values where the field values are contained by the corresponding field
+/// spaces.
+class ExtractSpace extends Space {
+  /// The type of values the space matches.
+  final StaticType type;
+
+  /// Any field subspaces the space matches.
+  final Map<String, Space> fields;
+
+  ExtractSpace._(this.type, [this.fields = const {}]) : super._();
+
+  /// An [ExtractSpace] with no type and no fields contains all values.
+  @override
+  bool get isTop => type == StaticType.top && fields.isEmpty;
+
+  @override
+  String toString() {
+    if (fields.isEmpty && type == StaticType.top) return '()';
+
+    // If there are no fields, just show the type.
+    if (fields.isEmpty) return type.name;
+
+    var buffer = StringBuffer();
+
+    // We model a bare record pattern by treating it like an extractor on top.
+    if (type != StaticType.top) buffer.write(type.name);
+
+    buffer.write('(');
+    var first = true;
+
+    // Positional fields have stringified number names.
+    for (var i = 0;; i++) {
+      var pattern = fields[i.toString()];
+      if (pattern == null) break;
+
+      if (!first) buffer.write(', ');
+      buffer.write(pattern);
+      first = false;
+    }
+
+    fields.forEach((name, pattern) {
+      // Skip positional fields.
+      if (int.tryParse(name) != null) return;
+
+      if (!first) buffer.write(', ');
+      buffer.write('$name: $pattern');
+      first = false;
+    });
+
+    buffer.write(')');
+
+    return buffer.toString();
+  }
+}
+
+/// The uninhabited space.
+class _EmptySpace extends Space {
+  _EmptySpace._() : super._();
+
+  @override
+  String toString() => '∅';
+}