search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

skip constructor #130

Closed sweirich closed 5 years ago

sweirich commented 5 years ago

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.

antalsz commented 5 years ago

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.

antalsz commented 5 years ago

8180fd58fbed86c2dfad400af9c7c68f70cb9c9a 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.