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

Rename type doesn't affect signature when used with "in" #156

Closed ericgiovannini closed 4 years ago

ericgiovannini commented 4 years ago

Suppose we have

data Test = A Int | B String
        deriving Show

    test1 :: Test
    test1 = A 5

and our edit file looks like

in Test.test1 rename type Test.Test = Test.Bla

The resulting Coq code will look like

Definition test1 : Test := A #5.

Is this the intended behavior?

ericgiovannini commented 4 years ago

@lastland has said this is a bug (https://github.com/antalsz/hs-to-coq/pull/159#discussion_r436303763). I am looking into fixing this now.

Currently, the relevant functions used in converting signatures have a ConversionMonad constraint. I will try modifying these functions to have a LocalConvMonad constraint instead, so that we can obtain the local edit information pertaining to the definition whose signature we are translating. Where necessary, I will use withCurrentDefinition to switch from the global conversion monad to the local conversion monad.