hs-to-coq
hs-to-coq copied to clipboard
antalsz
Convert Haskell source code to Coq source code
There are several places in ghc that I'd like to be able to rewrite definitions to include a `{Default a}` constraint. For example: `VarEnv.lookupVarEnv_NF` Also: `Util.foldl2`, `Util.mapAccumL2`, `Util.only` (not sure...
Sometimes, when using `skip constructor`, we'll be left with redundant cases. For example: ``` hasSomeUnfolding :: Unfolding -> Bool hasSomeUnfolding NoUnfolding = False hasSomeUnfolding BootUnfolding = False hasSomeUnfolding _ =...
Processing this code fails when DFunUnfolding and CoreUnfolding constructors are skipped (working around by redefining the function). ``` substUnfolding subst df@(DFunUnfolding { df_bndrs = bndrs, df_args = args }) =...
As it stands, we always translate them in normal modules, and always throw an error in axiomatized modules
Now that we have an edit to change the type of a definition to include a "Default" constraint, we have to think about the interaction with termination edits. In particular,...
It would be good if hs-to-coq could help distinguish whether added axioms are trivially safe or not. i.e. ```Axiom bad : forall {a}, a.``` vs ``` Axiom ok: forall {a},...
When building the base library I get this error, I've followed the instructions of the README.md, any idea on how to make this work? I paste the output of the...
Our `rewrite` engine is a bare-bones version of something more honest. For example, what about real support for variable binding, or handling nonlinear patterns gracefully?
We have to do a topological sort to mix instance declarations and value declarations, and also to get instance declarations in the right order. Currently, this uses `topoSortSentences`. I want...
Hello, I am currently building a translation from Cryptol to Coq, and Jennifer Paikin mentioned hs-to-coq. Like in your project, we have developed a tiny Coq AST and pretty-printer. It...
