The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Thu, Jun 04, 2009 at 12:25:35PM +0200, Adam Koprowski wrote:
>    Dear all,
> 
>   Recently I'm experimenting quite a bit with Coq's extraction facility and
> I have a number of questions/problems that maybe some of you can shed some
> light on:
> 

Hi Adam,

For the moment, I'm afraid I'll only be able to give you short answers
to your points. Other tasks have kept me away from Coq development
recently, and this will continue for a few weeks.

As a general statement, I clearly acknowledge that most efforts
concerning extraction have been devoted to ensuring correctness, and
that usability/convenience for the user is still to be improved.

>    1. Extracted code is rarely used on its own; usually it will be
>    incorporated into a bigger program or at least there will be some 
> front-end
>    to it. That means that for data-structures that cannot be mapped 
> directly to
>    ocaml (think of characters, strings, numbers etc.) one needs to be able 
> to
>    translate back-and-forth between Coq's and ocaml's data-types. I'd 
> expect a
>    library to facilitate that. Is such a library available? If not, is there
>    any interest in creating one?
> 

That's precisely one of my goal for the next Coq version. Contribution(s)
welcome, by the way. Two possible directions (not at all exclusive): 

 1) Ocaml/Haskell libraries that can be linked with extracted code and provide
    conversion functions between Coq datatypes and ocaml ones.
    Bits and pieces already exist in some Users Contrib where I (and others)
    have already played with extraction.
 2) Improve extraction to allow on-the-fly conversion to the "true"
    ocaml structure, in the spirit of what can already be done for
    bool, lists and other inductive types with one-to-one mapping.
    For stuff like strings, it really look like the right way to go,
    in order to have nice readable messages directly in the ML source.
    This is no trivial work notheless (browse some earlier discussion about
    that on coq-club, around late december).

>    2. Extraction to Haskell does not support modules. That means that if one
>    want to use parts of standard library with modules (such as very useful
>    FSets/FMaps) then one basically has to give up the hope of extracting
>    Haskell code, right? Or are there any work-arounds possible?
> 

No hope for Haskell extraction of modules for the moment. But:

 1) Now that Coq provides Type Classes, we can imagine having a
    Type-Classes version of FSet/FMaps, it's somewhere on my TODO
    list.
 2) In situation where we know on what we want to instantiate
    FSets/FMaps, it is possible to design a "de-functorizer" 
    (either at the Coq level, or as a part of the extraction,
    or even as a kind of post-processor) that would produce code
    compatible with Haskell. This may lead to a *huge* amount of
    code duplication, though.


>    3. Extraction to a single file:
>    Extraction "*file*" *qualid*1 … *qualid**n*.
>    sometimes produces wrong signatures, resulting in a code that does not
>    compile. Is it a known bug?
> 

It is a bug I'm not aware of. As Coq says, "please report" ;-)


>    4. Extraction with one-ocaml-file-per-one-coq-file:
>    Recursive Extraction Library *ident*.
>    seems to be more robust in that respect but I have another problem with
>    it. It works with modules as basic units which means that some axioms 
> will
>    end up in the extracted code even if they are not needed for the 
> functions
>    that one really wants to extract (the standard library's Coq.Lists.List
>    module alone will give you 4 axioms). The axioms are translated to:
>    let *ident *= failwith "AXIOM TO BE REALIZED"
>    I don't want to realize those axioms since they are not needed and
>    shouldn't even end up in the extracted code in the first place, but since
>    they are extracted to constants those exceptions will be immediately 
> thrown.
>    What I do now is I patch the extracted files changing the above to:
>    let *ident *= *fun _ ->* failwith "AXIOM TO BE REALIZED"
>    which works just fine but for obvious reasons (tweaking extracted code)
>    does not seem to be a satisfactory solution.
> 

?!?!

Coq.Lists.List with axioms ? I really would like to see details of
that. I've quickly checked, I've nothing similar with a coq 8.2 here.

>    5. In fact it would be really great to have a combination of those two
>    types of extraction (4 & 5). I.e. to have the ability to extract only a
>    given set of functions with their dependencies (3) but to map a single 
> coq
>    file to a single ocaml file (4); which btw. also facilitiates writing
>    libraries to manipulate Coq's data-types in ocaml (1).
> 

Indeed, that would be nice, I'll try to allow that soon. The initial
idea of Extraction Library was ... extracting a library, for which
it's natural to incorporate as much as possible. It also have the nice
property of having a predictible content: two list.ml coming from two
different development should be identical. But ok, for a big
development, I acknowledge extracting *everything* isn't convenient,
nor is the extract-to-one-big-file approach. The only catch is to
check that a module-file M isn't used elsewhere, for instance as
argument of a functor. In this case, if you start removing part of the
content of M, bad things might happen. This was my (rather poor)
excuse for not having done that earlier, but the more I think of it,
the more I'm sure it can be handled.


Best regards,

Pierre Letouzey