Antal Spector-Zabusky

Can't build the runtime with gcc but no stdatomic.h

2

When I try to build the 4.12+domains branch on a system with gcc, but without the C11 `stdatomic.h` header, I get a build error in `runtime/major_gc.c` that shows up where...

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...

Automatically delete redundant cases/equations

5

Sometimes, when using `skip constructor`, we'll be left with redundant cases. For example: ``` hasSomeUnfolding :: Unfolding -> Bool hasSomeUnfolding NoUnfolding = False hasSomeUnfolding BootUnfolding = False hasSomeUnfolding _ =...

Create a way to axiomatize or skip top-level pattern bindings

1

As it stands, we always translate them in normal modules, and always throw an error in axiomatized modules

Better `rewrite` engine

2

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 need to be able to rewrite in types

Parameterized `order` edits

4

It might be nice to impose "default order" constraints, such as * For all types `T`, put `Semigroup` before `mappend` (i.e., `Semigroup__T` before `Monoid__T_mappend`) * For all types `T`, put...

Pull out uniform fixpoint arguments

2

Coq has an easier time doing termination proofs when we pull out fixpoint arguments that don't change. For instance, in GHC's `compiler/utils/Util.hs`, we find the function ```haskell -- Reformatted all2...

Right now, if we define a class `C` manually, we can never translate instances of `C` because the class info lookup fails. We need a way to provide the `h2ci`...

It seems like there's a lot of code lying around that isn't being run anymore. Someone who has some spare time should go through and delete it.