Automatically delete redundant cases/equations

[antalsz]

Sometimes, when using skip constructor, we'll be left with redundant cases. For example:

hasSomeUnfolding :: Unfolding -> Bool
hasSomeUnfolding NoUnfolding   = False
hasSomeUnfolding BootUnfolding = False
hasSomeUnfolding _             = True

If we skip every constructor except for NoUnfolding, the resulting Coq code is

Definition hasSomeUnfolding : Unfolding -> bool :=
  fun arg_0__ => match arg_0__ with | NoUnfolding => false | _ => true end.

But since our data type has only one constructor, Coq will reject this because the _ => true case is redundant. We can work around this with skip equation or skip case pattern, but could we instead infer this automatically?

(Examples and motivation from #130)

[nomeata]

I think this should be possible. We have code like isCompleteMultiPattern that checks if patterns are comple, and whether to add a catch-all case. I expect that the same or similar code can be used to check if an existing catch-call case can be dropped.

[antalsz]

I looked into using that, but the naïve way of reusing it produces quadratic code (check every prefix), and this solution seemed like it’d be quicker to pull together.

Although, if we only check the last case for redundancy, and then if that was redundant check the preceding case, we’d catch some of the problems – maybe enough?

[nomeata]

Yes, this might work:

1. split off a catch-all pattern in the original code, if it is there
2. check the other patterns for completeness
3. if not complete, add the existing catch-all. If there was none, add the default catch-call.

[antalsz]

We also have to handle each argument separately, but yeah, that seems like a good outline. Particularly if we assume that this is only introduced by skip constructor – otherwise the Haskell code probably doesn’t have redundant cases. And if it is, the redundancy is gonna be in the catch-all case. (If there was other redundancy, well, we still have skip equation and skip case pattern.)

[nomeata]

We also have to handle each argument separately

You mean in functions with multiple arguments? That’s taken care of, I believe, as isCompleteMultiPattern takes a multi-patern.

otherwise the Haskell code probably doesn’t have redundant cases.

surprisingly :-)

(I had a recollection that I had to prune redundant catch-all cases at the end, but looking at the code that does not seem to be true. Which is good.)