Top-level Fixpoint Definitions

[euisuny]

Currently, we have DefinitionSentences at the top-level, even for recursive operators. Fixpoints are defined using inlined fix operators. However, it would be cleaner (i.e. Coq's unfolding through cbn or simpl will behave ""as expected"") if we had top-level fixpoint definitions using FixpointSentence.

This is implemented by slapping on an extra pattern match on a top level function in src/lib/HsToCoq/ConvertHaskell/Module.hs. Probably not the most robust way to add on this feature, but it works (passes examples/boot.sh).

Also deleted src/lib/HsToCoq/ConvertHaskell/Declaration/Value.hs, which isn't used anywhere and seems to be a deprecated version of ConvertHsGroup in src/lib/HsToCoq/ConvertHaskell/Module.hs.

Proposed fix to #140.

[lastland]

@antalsz @nomeata What do you think? Any special reasons that hs-to-coq prefers Definition and fix to Fixpoint?

[antalsz]

@euisuny I'll have to take a closer look at this, but this looks potentially promising! One thing I'm not certain about is what advantage we get – can you elaborate on how cbn/simpl work differently with Fixpoint vs. Definition := fix?

[euisuny]

Oops, I had thought that change made some difference in unfolding behavior, but I was wrong and can use fold to do what I wanted to do originally, anyways...

So, for now, the only selling point that remains for this change is aesthetics (and the marginal code cleanup on Value.hs).

[lastland]

The CI report seems to suggest that this is a nice aesthetic change that does not require extra editing on existing proofs.

[antalsz]

I like this change. I think there are two broader questions that go with it, though:

1. Does this change impact the question of what I've provisionally taken to calling “legibility”? That is, the does this disrupt the source-level similarity between the Haskell code and the Coq code that is our best argument for why you should trust hs-to-coq? On reflecting, I think the answer here is that this helps legibility, so I like it!

2. If we're going to do this, why not do it for Definitions too? It's a good change, and we can spread it further!

If you could look into point 2 and the small code changes I mentioned above, then let's merge this!

[lastland]

Thank you for including a troubleshooting section! Is this this really the best way to get lndir? It might be – I've certainly never checked why I have it – but that's a big install for a simple tool.

I can testify that installing xquartz is how I get lndir on my new Macbook. It may not be the only way to get lndir, but it's the easiest way after studying this a bit on Google.

[lastland]

I have just encountered an example that favors this change.

I have the following Haskell definition (please excuse me for not trying to minimize the example at this moment---I will do that later):

data SetExt :: * -> * where
  Empty :: SetExt a
  Singleton :: a -> SetExt a
  Add :: Eq a => a -> SetExt a -> SetExt a
  Union :: Eq a => SetExt a -> SetExt a -> SetExt a
  PowerSet :: SetExt a -> SetExt (MySet.Set a)

interp_ext :: SetExt a -> MySet.Set a
interp_ext Empty = MySet.empty
interp_ext (Singleton a) = MySet.singleton a
interp_ext (Add a s) = MySet.add a $ interp_ext s
interp_ext (Union s1 s2) = MySet.union (interp_ext s1) (interp_ext s2)
interp_ext (PowerSet s) = MySet.powerSet $ interp_ext s

The original hs-to-coq translation would give me a definition of interp_ext that cannot be type checked:

Error:
In environment
interp_ext : forall a : Type, SetExt a -> MySet.Set_ a
a : Type
interp_ext0 : SetExt a -> MySet.Set_ a
arg_0__ : SetExt a
T : Type
e : Base.Eq_ T
a0 : T
s : SetExt T
The term "s" has type "SetExt T" while it is expected to have type
 "SetExt a".

However, switching to this version with top-level fixpoint definitions solves the problem.

So, for now, the only selling point that remains for this change is aesthetics.

Not true! 🙂

[lastland]

I have manually merged this PR.