The Coq mailing list

[Giuseppe Castagna <Giuseppe.Castagna AT ens.fr>]

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

> > Before starting I would like to know if somebody does not 
> > already carry out this.
> 
>  Depending on what do you want to extract, it may be a good
>  idea to either:
> 
>  1. start from the extracted XML files.
>     [The extraction module to XML is already part of the standard
>      distribution of Coq, but it is undocumented. (Some small
>      parts will change again in a few monthes. Other are really
>      stable.) Feel free to ask me more infos about that.]
>  2. modify the extraction module for XML files.
>     [More difficult than 1, IMHO.]
>  3. restart from scratch if the information you need is not there.
>     [In this case I would be interested in privately know what
>      is the missing information.]
> 
>                                       Regards,
>                                       C.S.C.