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

"Except in" edit #159

Closed ericgiovannini closed 4 years ago

ericgiovannini commented 4 years ago

Adds support for an "except in" edit, which allows the user to specify an edit and one or more identifiers, and applies the given edit everywhere except for within the definitions of the given identifiers.

Also adds an entry for this new edit to the documentation, and includes an example/test case illustrating the edit. Note that there are currently a couple of important caveats regarding the behavior of this edit.

  1. Type signatures are not subject to the exceptions specified by "except in" edits. For example, suppose we have a module MyModule with a type Ty1 and a function foo :: Ty1 -> Ty1. Suppose our edit file contains

    except in MyModule.foo rename type MyModule.Ty1 = MyModule.Ty2

    Then after running hs-to-coq, the signature of foo will be Ty2 -> Ty2, even though we excluded MyModule.foo when we specified the rename edit. This is not an issue with "except in" edits; it is a result of the fact that local edits are not taken into account when translating signatures. See issue #156 for more.

  2. Using an "except in" edit to rename a user-defined type will also rename the type in its original declaration and definition; this may not be what you want to do.

    For example, suppose we have a module MyModule with a user-defined type Ty1:

    data Ty1 = A Int | B String

    Without applying any edits, the resulting Coq file will contain the following declaration and definition:

    Inductive Ty1 : Type
  := | A : GHC.Num.Int -> Ty1
  |  B : GHC.Base.String -> Ty1.

    Suppose we apply the following edit:

    except in MyModule.foo rename type MyModule.Ty1 = MyModule.Ty2

    (where foo is a function in the Haskell module). In the resulting Coq file, Ty1 will be renamed to Ty2 in the declaration and definition of Ty1:

    Inductive Ty2 : Type
  := | A : GHC.Num.Int -> Ty2
  |  B : GHC.Base.String -> Ty2.

    This may be useful, but if the Haskell module already contains a type called Ty2, then hs-to-coq will simply discard Ty1. However, in this case, what we probably want is for the declaration and definition of Ty1 to remain, and in particular, to remain as Ty1. All other occurrences of Ty1, except for the ones in definitions given in the except in edit, should be renamed to Ty2.

    To try to exclude the declaration and definition of Ty1 from the renaming, we could try adding MyModule.Ty1 to the except in edit, but this does not seem to work (see examples/tests/ExceptIn/edits). Alternatively, it might make sense to consider the declaration to be part of the definition, so that we can prevent the name of the type in the declaration from being renamed. To do this, we would need to be able to apply rename edits locally within a declaration.

Both of these issues occur in the example I included, and they are discussed in the edits file (examples/tests/ExceptIn/edits).

lastland commented 4 years ago

Hi, is this PR ready to be merged, or is there something else blocking it? I notice that the ExceptIn test in currently under TODO_PASS. Is that intentional, or is that because of some other bug (perhaps #156 )?

ericgiovannini commented 4 years ago

There are two reasons why the ExceptIn test currently fails; the first is due to #156 (see also item (1.) on the list of caveats at the top of this pull request, as well as item 1 in the comments of tests/ExceptIn/edits). This issue has been fixed by another PR (#160), but that has not been merged into this branch. Once this PR is merged into master (which has #160 merged in), this issue should no longer be present. The second reason the test is failing is due to caveat (2.) at the top of this PR; more specifics are provided in item 2 in the comments of tests/ExceptIn/edits. Basically, in this example, Test1 is getting renamed to Test2 in Test1's declaration, leading to there being two Test2's, only one of which is included in the Coq file (which one it is depends on how the definitions of Test1 and Test2 are ordered). Thus, the constructors of the one that was removed are not defined, so when Coq encounters those constructor names later in the file, it gives an error saying that they are unknown.

The reason why Test1 is being renamed to Test2 is because currently, there is not a way to apply a local edit (in this case, an except in edit) when translating the name in a declaration. I'm not sure if fixing this issue lies within the scope of this PR, but until it is resolved, this test will fail.

lastland commented 4 years ago

Hi @ericgiovannini, thanks for the detailed explanation! I think what we can do is to separate the tests relevant to these two issues, and put the tests already been fixed by #160 in the PASS category. Considering that the fix by #160 is not present in this branch, I'm going to rebase and merge this PR now, and we can fix the tests later (either on master branch, or as a separate PR). In addition, I think it's worth documenting some of our discussions here in the documentation (edits.rst): in particular, the caveat (2) and what you find out in https://github.com/antalsz/hs-to-coq/pull/159/files#r469593097. I can do these myself, but let me know if you prefer to do them yourself. :)

And thanks again for adding this edit and the wonderful job you have done to document its behavior!

ericgiovannini commented 4 years ago

In addition, I think it's worth documenting some of our discussions here in the documentation (edits.rst): in particular, the caveat (2) and what you find out in https://github.com/antalsz/hs-to-coq/pull/159/files#r469593097. I can do these myself, but let me know if you prefer to do them yourself. :)

Feel free to add these to the documentation, and let me know if you have any questions.