The Coq mailing list

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

On 12 Feb 2003, Giuseppe Castagna wrote:

> On Tue, 2003-02-11 at 16:47, Claudio Sacerdoti Coen wrote:
> >  Dear Serge,
> > 
> > On Tue, Feb 11, 2003 at 15:05:08 +0100, Serge Leblanc wrote:
> > > Hello, for my first contribution I wish to
> > > carry out a Coq->CDuce[1] extraction functionality.
> > 
> >  what do you want to extract exactly?
> > 
> Hello Serge,
> 
> I was asking myself exactly the same question. Do you want to extract
> XML transformations that you specify in Coq? I'm *very* curious to know
> why you chose CDuce as a target language (I'm not against it, on the
> contrary!... FYI I'm one of the persons working on the definition of
> CDuce). I see that the higher order functions of CDuce can be useful
> for that, but it seems a little bit hard to compensate the absence of
> polymorphic types (and I cannot promise you that we will come out with a
> satisfactory definition in short time).
> 
> All the best
> 
> ---Beppe---
> 

This is the right question. 

- If the goal is to translate complete Coq terms to other syntax, 
(for documentation purpose for example) then the XML output by Claudio
is what you need. 

- If the goal is to produce real programs and make fast computations, then
you should take advantage of the existing Coq extraction: 
 * parts that have no computational meaning (purely logical parts) are
   removed automatically.
 * I have already quite a experience in translating the so-complex Coq
   types to poor Ocaml types. This part is not yet well documented. 
   Basically I remove dependancy upon terms in types, and whenever there
   is no simple counterpart for a Coq type (for example "if b then nat
   else bool") then I use an "unknown" or "Top" type (Obj.t in Ocaml).
   And finally in the extracted terms, unsafe casts (Obj.magic:'a->'b) 
   are inserted wherever the Ocaml type-checker is not happy.

As I said to Serge in a previous answer to coq-club, I think this 
technology is adaptable to any ML dialect, including CDuse. 


Pierre Letouzey

PS: What about a meeting about this Coq->CDuse extraction ? I don't know 
where Serge is geographically located, but at least the database and
demons groups of LRI are not far away. And ENS Ulm isn't at the
antipodes...