hs-to-coq
hs-to-coq copied to clipboard
antalsz
Convert Haskell source code to Coq source code
Some edits should be local (renames), some should not be local (renames for other reasons). This should be expanded on.
see examples/tests/Arrow.hs Shows up in CallArity.hs. Workaround is to use a let to name the argument of Arrow.first instead of providing a lambda expression.
I have put a minimal example in `examples/tests`. In summary, if you have the following functions: ```Haskell comp :: (b -> c) -> (a -> b) -> a -> c...
`Semigroup.hs` used the `DefaultSignatures` extension to define the `Semigroup` type class: ```Haskell class Semigroup a where () :: a -> a -> a default () :: Monoid a => a...
Many base module edit files include this for newtype coercions ``` add Data.Monoid Instance Unpeel_Dual a : Unpeel (Dual a) a := Build_Unpeel _ _ getDual Mk_Dual. ``` We shouldn't...
If type class instances use scoped type variables, they will fail. There is an explicit comment in the function HsToCoq.ConvertHaskell.Declarations.Instances.topoSortInstance: -- ASSUMPTION: type variables don't show up in terms. Broken...
When I convert GHC.Base using the -N flag, with the following skipped modules skip module GHC.Arr skip module GHC.Generics skip module GHC.Types skip module GHC.CString skip module GHC.Classes skip module...
There's a lot going on in this repository: 1. The `hs-to-coq` conversion tool itself 2. An abandoned GHC plugin that enables converting between structurally isomorphic types 3. The converted parts...
``` data Width = W8 | W16 | W32 | W64 | W80 -- Extended double-precision float, -- used in x86 native codegen only. -- (we use Ord, so it'd...
It would be convenient to be able to say ``` skip type Outputable.SDoc ``` and have it skip all functions that use that type. This would replace individual skips of...