Como determinar se o seguinte bloco de switches é exaustivo?

sealed interface I permits A, B, C { }
final class A implements I { }
final class B implements I { }
record C(int j) implements I { } // Implicitly final
record Box(I i) { }
int testExhaustiveRecordPatterns(Box b) {
    return switch (b) { // Exhaustive!
        case Box(A a) -> 0;
        case Box(B b) -> 1;
        case Box(C c) -> 2;
    };
}

Este é um exemplo que aparece na especificação da linguagem Java 22 (14.11.1.1) .

Posteriormente, a especificação fornece algumas explicações:

Determinar se esse bloco de switch é exaustivo requer a análise da combinação dos padrões de registro. O conjunto que contém o padrão de registro Box(I i)cobre o tipo Box, e assim o conjunto que contém os padrões Box(A a), Box(B b), e Box(C c)pode ser reescrito para o conjunto que contém o padrão Box(I i). Isso ocorre porque o conjunto que contém os padrões A a, B b, C creduz-se ao padrão I i(porque o mesmo conjunto cobre o tipo I), e assim o conjunto que contém os padrões Box(A a), Box(B b), Box(C c)reduz-se ao padrão Box(I i).

No entanto, ainda não é detalhado o suficiente para mim. Posso ver que essas regras devem ser citadas ao determinar se o bloco switch é exaustivo (Algumas regras relevantes):

O bloco switch de uma expressão switch ou instrução switch é exaustivo para uma expressão seletora ese um dos seguintes casos se aplicar:

• O conjunto que contém todas as constantes de caso e padrões de caso que aparecem em um rótulo de caso desprotegido (conhecidos coletivamente como elementos de caso ) associado ao bloco switch não é vazio e cobre o tipo da expressão do seletor e.

Um conjunto de elementos de caso, P, cobre um tipo Tse um dos seguintes casos se aplicar:

• O tipo Tnomeia uma classe selada abstrata ou interface selada Ce para cada subclasse ou subinterface direta permitida Dde C, uma das duas condições a seguir é válida:

1. Não existe um tipo que nomeie De seja um subtipo de T, ou
2. Existe um tipo Uque nomeia De é um subtipo de T, e Pabrange U.

• P reescreve para um conjunto Qe Qcobre T.

Um conjunto de elementos de caso, P, é reescrito no conjunto Q, se um subconjunto de Pfor reduzido a um >padrão p, e Qconsiste nos elementos restantes de Pjunto com o padrão p.

Um conjunto não vazio de padrões, RP, reduz-se a um único padrão rpse uma das seguintes condições for válida:

– RPabrange algum tipo Ue rpé um padrão de tipo do tipo U.

– RPconsiste em padrões de registro cujos tipos apagam todos para a mesma classe de registro Rcom k(k≥1) componentes e há um componente distinto cr(1≤r≤k) de Rtal forma que para cada outro componente ci (1≤i≤k, i≠r) o conjunto contendo os padrões de componentes dos padrões de registro correspondentes ao componente cié equivalente a um único padrãoqi , o conjunto contendo os padrões de componentes dos padrões de registro correspondentes ao componente crreduz-se a um único padrãoq e rpé o padrão de registro do tipo Rcom uma lista de padrões consistindo nos padrões q1, ..., qr-1, q, qr+1, ..., qk.

Um conjunto não vazio de padrões EP é equivalente a um único padrão ep se uma das seguintes condições for válida: › EPconsiste em padrões de tipo cujos tipos têm todos a mesma eliminação T, e epé um padrão de tipo do tipo T. › EPconsiste em padrões de registro cujos tipos apagam todos para a mesma classe de registro Rcom k(k≥1) componentes e para cada componente de registro o conjunto contendo os padrões de componentes correspondentes dos padrões de registro é equivalente a um único padrão qj(1≤j≤k), e epé o padrão de registro do tipo Rcom uma lista de padrões de componentes consistindo nos padrões de componentes q1,...qk.

No entanto, tenho alguma dificuldade em entender essas regras, especialmente as partes em negrito. Por exemplo,O que significa " from the record patterns matching to component ci "," from the record patterns matching to the component cr "?Para ser mais preciso, acho que não entendi bem o significado de " matching to " aqui. De acordo com as explicações na especificação, acho que a frase "This is because the set containing the patterns A a, B b, C creduces to the pattern I i" deve ter usado as regras na parte em negrito.No entanto, não consigo descobrir como A a, B b, C csurgiu.

Você poderia me ajudar a analisar os regulamentos na especificação em combinação com os exemplos?Sei que não é uma tarefa fácil. Obrigado por ler e responder.