hs-to-coq
hs-to-coq copied to clipboard
antalsz
Convert Haskell source code to Coq source code
Input: ``` data F a = G a a deriving (Eq, Ord) ``` In the definition of `( F inst_a -> comparison := fun a b => let 'G a1...
Trying to translate `base-4.14`, some modules (like `Data.Foldable`) mention types from skipped modules (like `GHC.Generics.UWord`), which causes the translation to fail. ~~In particular, in this case the type is mentioned...
Is there an edit to skip `pattern` declarations? hs-to-coq just chokes on them: ``` non-function top level bindings: pattern Em = () unsupported [in module A] ``` Context: there are...
When translating mutually recursive functions hs-to-coq generates one `Definition`, which contains a `fix`, for each of the mutually recursive functions. Each of those definitions must contain code for all functions...
Currently, hs-to-coq uses Program Fixpoint to deal with more complex termination arguments. However, this makes it extremely hard to work with the resulting code, since Program Fixpoint creates huge proof...
Right now the Coq code is compiled with `-R base/ ""`, which causes warnings because these modules have the same names as those under `base-thy/`.
The problem with this is that it regenerates itself, and it will be different if you don't use the exact same version of Coq, so that adds noise to `git...
We provide some new machinery in, for example, `GHC.DeferredFix` and `GHC.Nat`. But these aren't GHC modules, they're ours! We should move them to `HsToCoq.DeferredFix` or `H2C.DeferredFix` or `HsToCoq.Translation.DeferredFix` or something...
It seems that an edit that makes a definition polymorphic would be helpful. I know that Eric has already been working on this, and I am opening this issue to...
It seems that ``` hs-to-coq --ghc -package-env=hs-to-coq.env ``` doesn’t work the way it should, but ``` GHC_ENVIRONMENT=hs-to-coq.env hs-to-coq ``` does. Some wild guess: We need to extract the `--ghc` flags...
