coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Nikita Karetnikov <nikita AT karetnikov.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Haskell extractor: imports, type parameters
Date: Fri, 04 Sep 2015 01:17:12 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nikita AT karetnikov.org; spf=Pass smtp.mailfrom=nikita AT karetnikov.org; spf=Pass smtp.helo=postmaster AT cooksoni.karetnikov.org
Ironport-phdr: 9a23:G5VavR0AI5Ky+XbbsmDT+DRfVm0co7zxezQtwd8ZsegSKPad9pjvdHbS+e9qxAeQG96Lt7Qc1qGO6OjJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZzqnLjps7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGC2O5XoAWy01mwBFHw7E7xbkFsP3syj7quNV2yCAMNHwTLMzR3Kl9ag9G0ygszsOKzNsqDKfscd3lq8O+B8=

I'm toying around with the Haskell extractor. Is there a way to alter
the Haskell module list? E.g., import Prelude without the qualified
keyword. Can I set the default parameter name for types like Maybe?
I'd like it to be a not a1.

Here is my attempt:

https://github.com/nkaretnikov/99-problems/commit/7b656c8347c91f36f669c21c2028e272c8c6aa9d

Can I make the generated Haskell code prettier without making the Coq
part look like Haskell as done in the following code?

https://github.com/jwiegley/coq-haskell/blob/6ca62bc51d2dcb09539211d62bbd46de71374941/src/Data/Maybe.v
https://github.com/jwiegley/coq-haskell/blob/a30a8975c524279a009625fd4a53e2fdb9d0b9dc/fixcode.pl

[Coq-Club] Haskell extractor: imports, type parameters, Nikita Karetnikov, 09/04/2015