Promote edit

[ericgiovannini]

Adds a new promote edit, which allows the user to specify that a definition that normally would be placed in the set of term-level definitions in the resulting Coq file should instead be "promoted" to the set of type-level definitions.

[lastland]

Does this change the way code is currently translated? The CI seems to suggest so, as the convenience copy of base, containers, ghc, and transformers seems to be different from what is generated with this patch. Can you try to rebuild the convenience copy? You should be able to do that by running make clean && make in their corresponding directories under examples (some of these may need you to rebuild base-thy as well, I don't remember exactly.) Let me know if you have any questions.

[lastland]

Oh I forgot, you can also simply run boot.sh from examples directory.

[ericgiovannini]

I tried running boot.sh, but it failed with the error can't find file: base/GHC/Base.hs. So I then tried to build the base library by running make -C base from the root, but this immediately failed with make: *** [all] Error 2. Any ideas as to why this could be happening?

[lastland]

I'm not sure why boot.sh goes wrong, but can you try going to examples/base-src and run make clean && make from there? What base contains is the generated Coq code translated from the Haskell code in examples/base-src.

[ericgiovannini]

Just tried this, and I get a similar error about being unable to find base/GHC/Base.hs. Here are the last few lines that were displayed:

....
stack exec hs-to-coq -- -e module-edits/GHC/Base/edits \
              \
             --midamble module-edits/GHC/Base/midamble.v \
         -e edits -N -i gen-files -I gen-files -i base -I base/include --iface-dir ../../base --dependency-dir deps --ghc -this-unit-id --ghc base -o ../../base \
         base/GHC/Base.hs
hs-to-coq: panic! (the 'impossible' happened)
  (GHC version 8.4.3 for x86_64-apple-darwin):
    can't find file: base/GHC/Base.hs

[lastland]

Uh sorry, I forget. The Haskell files are in submodules, you will need to run

git submodule update --init --recursive

The command will download all the submodules (some of them are from ghc).

[ericgiovannini]

Thanks, after running that, I was able to use make clean && make to rebuild the convenience copies for base (in examples/base-src), containers, and transfomers. But for ghc, the latter command failed with

make[2]: *** No rule to make target `../../containers/theories/MapProofs.vo', needed by `IntMap.vo'.  Stop.

[lastland]

It seems like you also need to compile examples/containers/theories to continue. The directory contains our theorems and proofs for the containers library, and it seems that our translation of ghc depends on it.

[ericgiovannini]

That seems to have fixed the error, but now a new error occurs:

File "./CoreFVs.v", line 132, characters 58-81:
Error: The reference bndrRuleAndUnfoldingFVs was not found in the current
environment.

However, I repeated the above steps on a fresh clone of the repository and this error did not occur, so I am assuming it has to do with a change I made.

[lastland]

I do not recall seeing this error message in the past, so it is possible to be introduced by a change you made. I can take a look at it later (I was going to say tomorrow, but I should probably say during the daytime).

[lastland]

Hi @ericgiovannini, I think I see what the problem is. Your PR somehow changes the order that translated definitions appear, and that causes certain function definitions to appear before the functions they use. For example, the error message you get is caused by expr_fvs appearing before bndrRuleAndUnfoldingFVs. There are two ways that you can fix this: (1) modify the code generation mechanisms to keep the original order; (2) use the order edit to guide hs-to-coq to generate code with the right dependency. I haven't taken a careful look at your code yet, so I am not certain which one would be a better design decision. What do you think?

[ericgiovannini]

Thanks for taking a look at this. In the latest commit on this branch, I did make a change that could possibly change the order of the translated definitions: In HsToCoq.ConvertHaskell.Module.convertHsGroup, I removed the code that uses topoSortEnvironment to order the named sentences. There was a comment below this line asking if it was really needed, because moduleDeclarations calls topoSortByVariablesBy later on. So it seemed that the line was redundant and I removed it; I will try putting it back and see if this makes a difference.

[ericgiovannini]

I made the change and it seems to have fixed the issue. I have made a commit with the change.

[ericgiovannini]

I've added two test cases, one (called Promote) that doesn't require recursive promotes, and the other (called Promote2) that does require them.

[lastland]

Thanks @ericgiovannini! It seems that these tests are a bit weak though, as they won't tell the promote edit from a no-op. I have added two midamble.v files to enhance the tests. midamble.v is inserted after type declarations but before value declarations, so it can be used to test if certain declarations have already appeared at this point.

[lastland]

This looks good. Thank you @ericgiovannini!