The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Tue, 11 Feb 2003, Serge Leblanc wrote:

> Hello, for my first contribution I wish to
> carry out a Coq->CDuce[1] extraction functionality.
>
> Before starting I would like to know if somebody does not
> already carry out this.
>
> I would not wish to waste my time to remake an already existing
> functionality.
>
> [1] http://www.cduce.org/
>

Being the current maintainer of the Coq extraction mechanism,
I am not aware of any existing Coq->CDuce extraction (to tell the
truth, I was not aware of the existence of CDuce before your mail...)

In Coq version 7.4 there are three available output languages for
the extraction:

Objective Caml
Haskell
Scheme (experimental)

Normally, adding a new output language is fairly simple, due to the design
of the extraction: in fact we first extract to a generic Mini-ML language,
(see in sources contrib/extraction/miniml.mli) and then we pretty-print
these Mini-ML terms to concrete syntax (see for example the ocaml
pretty-printer in contrib/extraction/ocaml.ml).

But in the case of CDuse, it seems to be more difficult:
from what I've read in the CDuse web-site, types of arguments
must be written, rather than infered. But since these types aren't
needed in any of the current output languages, I do not store them in
Mini-ML terms. That can probably be patched, but isn't trivial.

So a CDuse extraction based on the current extraction is certainly doable,
but probably involves more work than just adding a printer as I did for
Scheme.

Please feel free to contact me if you need more details on the current
extraction design. And of course I would be glad to integrate your
Coq->CDuse extraction in the Coq official distribution when it will be
ready.

Pierre Letouzey