Automatically delete redundant cases/equations

[lastland]

Issue by antalsz
Friday Jun 28, 2019 at 05:33 GMT
Originally opened as antalsz/hs-to-coq#135

---

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)

[lastland]

Comment by nomeata
Friday Jun 28, 2019 at 08:45 GMT

---

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.

[lastland]

Comment by antalsz
Friday Jun 28, 2019 at 15:44 GMT

---

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?

[lastland]

Comment by nomeata
Friday Jun 28, 2019 at 16:40 GMT

---

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.

[lastland]

Comment by antalsz
Friday Jun 28, 2019 at 16:43 GMT

---

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.)

[lastland]

Comment by nomeata
Friday Jun 28, 2019 at 17:06 GMT

---

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.)