The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Dear Pierre,

  Thank you very much for a quick and informative response.

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 [...]
 2) Improve extraction to allow on-the-fly conversion to the "true"
   ocaml structure [...]

  Great. For the moment I just wrote few simple conversion functions. If there was some coordinated effort at a development of such a library then I'd love to contribute. The second approach obviously sounds more attractive but I'm sure it's also more difficult one.

  For stuff like strings, it really look like the right way to go,

  Indeed. At the moment extracted strings are somewhat verbose and not exactly readable ;). And I dare say it's a rather important data-structure for every development (think of error messages).
 

 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.

2009/6/4 Stéphane Lescuyer <stephane.lescuyer AT inria.fr>:

Just to let you guys know, I've already developed such a library [...]

  Great! Looking forward to be able to get my hands on it :).

 2) In situation where we know on what we want to instantiate
   FSets/FMaps, it is possible to design a "de-functorizer" [...]

  I don't quite see how one would write such a de-functorizer. I have two data-structures that I need sets for and I could live with code-duplication. Both data-types are parametric and at the moment I pass those parameters as an argument to a functor; I could easily change my modules to sections but how would I instantiate FSet then? (as modules are not allowed in sections)?
 

>    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" ;-)

  Will do :)
 

?!?!
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.

  I'm sorry, my mistake. I was always using Coq's dont-load-proofs switch and didn't realize it doesn't go well with extraction. No axioms anymore :)

 

>    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) [...]

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. [...]

  Agreed. The only problem with this approach is performance as all the extracted constants will need to be evaluated upon running the code. Indeed I have a problem with that. I prove some expensive properties in Coq that ensure that the function I want to extract is correct but I don't want to repeat this check in the extracted code. I could solve that by turning constants into functions with an artificial unit argument (which will never be evaluated) but that seems like a hack that I'd rather avoid.

  Cheers,
  Adam

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski


The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================