Lift haskell record names to coq record names

[threonorm]

A very rough first try at #79 though it is not quite working because it ends up adding some stuff from GHC.Err for the default instances. In our case (riscv-coq) we exclude manually the Default instances in the .edits file which is kind of hacky.

In our case this lifting is very convenient to clarify the code produced, where name are fairly important, for example:

Inductive InstructionM64 : Type
-  := Mulw : Register -> Register -> Register -> InstructionM64
-  |  Divw : Register -> Register -> Register -> InstructionM64
-  |  Divuw : Register -> Register -> Register -> InstructionM64
-  |  Remw : Register -> Register -> Register -> InstructionM64
-  |  Remuw : Register -> Register -> Register -> InstructionM64
+  := Mulw (rd : Register) (rs1 : Register) (rs2 : Register) : InstructionM64
+  |  Divw (rd : Register) (rs1 : Register) (rs2 : Register) : InstructionM64
+  |  Divuw (rd : Register) (rs1 : Register) (rs2 : Register) : InstructionM64
+  |  Remw (rd : Register) (rs1 : Register) (rs2 : Register) : InstructionM64
+  |  Remuw (rd : Register) (rs1 : Register) (rs2 : Register) : InstructionM64
   |  InvalidM64 : InstructionM64.

At some level just lifting the names should not necessarily require any extra definitions (like argument specifiers, default instances and selectors), if one does not use those instances and selectors.

So I tried completely silencing the Default instances for constructors directly in TyCl.hs, and it seems to pass all the example/tests, but that does not seem a reasonable thing to do because I guess this Default instance generation code is here for a good reason, that I did not quite understand.

So I am wondering, what are those Default Instances with GHC.Err for? (Because I guess they don't actually allow partial definition of a value, because it's Coq)

[sweirich]

Hi,

Thanks for the pull request!

The Default instances are necessary to support partial functions in our translation. If there is a pattern match failure, then instead of throwing an exception, the translation returns an arbitrary (opaque) member of the type.

For our uses of hs-to-coq on ghc, we need the automatic generation of Default instances because this codebase both defines many types and a lot of partial record selectors.

However, that may not be the case for all examples. Perhaps we can add an edit that will add Defaults or remove Defaults wholesale? @antalsz , @nomeata , what do you think?

[nomeata]

You can already skip them manually, as done for example in this project: https://github.com/samuelgruetter/riscv-coq/blob/master/convert-hs-to-coq/Decode.edits#L30

Disabling it completely is of course possible; I am not too keen on adding too many very specialized edits or flags when the goal can already be achieved using the existing edits.

[threonorm]

Yes, that is exactly what I do right now (same project, riscv-coq that I am working on with @samuelgruetter ), but that means that all the existing code would likely need corresponding skip of the instances, or would need to be always linked with GHC.Err. But I guessed it is not a problem.

But that means that examples/tests/Records.hs will either need to be linked with base, or will need skips. Is that fine?

In the meantime I will try fixing a typing bug in the instance Default that are generated right now.

[threonorm]

Note: Currently the heuristic is to generate default instance only for things that have known names for the arguments of the constructors.

Then I fill the arguments with default. The problem is that nothing ensures that all the arguments have defaults. That is why I ended needing to skip some instances in examples/ghc. (Some are skipped because they were double defined, some because an underlying member default did not exist).

There is likely a better way to do that, maybe the right thing would be a lazy creation of the default instances, when required, simultaneously keeping track of the dependent default instances not yet created.

[samuelgruetter]

Dear hs-to-coq developers, For the riscv-coq project (and even more so for the riscv specs in other languages we want to derive from riscv-coq) it would be really useful to have this feature in hs-to-coq. Could one of you please have a look at this PR and let us know what needs to be done to make it mergeable? Thank you so much :) Sam

[sweirich]

Hi, Thanks for this pull request. It looks awesome!

The only difficulty I see is that we have two different places for tests. Those in the test do not have any reliance on the base libraries; those in base-test do. As you've updated the record test, can you move it to the base-test subdirectory?

I'm not sure what the best approach to generating the default instances is. Perhaps we need to keep better track of what types have defaults available? I don't think generating the instances lazily will work as it is often code in a different module that needs the instance.

[antalsz]

This looks awesome – merged!

[antalsz]

I didn't want to let the Default stuff block the merge, but I've created an issue (#102) to record how we plan to deal with that in the future :-)

[threonorm]

Thanks a lot!