[CLOSED] skip constructor

[lastland]

Issue by sweirich
Thursday Jun 27, 2019 at 18:23 GMT
Originally opened as antalsz/hs-to-coq#130

---

When I skip all except for the NoUnfolding constructor of the Unfolding data type, hs-to-coq produces the wrong output for this input.

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

Specifically, the result is:

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

which Coq rejects because of the redundant pattern.

I'm currently working around by skipping this function.

[lastland]

Comment by antalsz
Thursday Jun 27, 2019 at 18:30 GMT

---

Ah, the expected edge cases. This may be tricky to eliminate algorithmically – would a

skip equation Core.hasSomeUnfolding _

edit work instead? That might be simpler.

[lastland]

Comment by antalsz
Friday Jun 28, 2019 at 06:04 GMT

---

8180fd5 adds the aforementioned skip equation edit, which was much simpler to add than a pattern redundancy checker. I'm closing this, but I've created #135 to remind us to consider adding automatic redundancy checking.