fn compute_exhaustiveness_and_usefulness<'a, 'p, Cx: PatCx>(
mcx: &mut UsefulnessCtxt<'a, 'p, Cx>,
matrix: &mut Matrix<'p, Cx>,
) -> Result<WitnessMatrix<Cx>, Cx::Error>
Expand description
The core of the algorithm.
This recursively computes witnesses of the non-exhaustiveness of matrix
(if any). Also tracks
usefulness of each row in the matrix (in row.useful
). We track usefulness of subpatterns in
mcx.branch_usefulness
.
The input Matrix
and the output WitnessMatrix
together match the type exhaustively.
The key steps are:
- specialization, where we dig into the rows that have a specific constructor and call ourselves recursively;
- unspecialization, where we lift the results from the previous step into results for this step
(using
apply_constructor
and by updatingrow.useful
for each parent row). This is all explained at the top of the file.