The Coq mailing list

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

Hello David,

On Thu, 24 Feb 2005, David Monniaux wrote:

> I'm currently playing with Coq and extraction, and I'm having the 
> following problems:
> * Since the list constructor of standard OCaml (infix ::) is not (yet) 
> usable as a prefix ( :: ), I cannot just tell Coq to extract lists to 
> OCaml lists. (Future OCaml versions will allow prefix ( :: ), I'm told.)

Yes, Yves Bertot has come long ago with the same problem, and I remember 
having submitted a feature-wish to the Ocaml team.

> * OCaml compiles match e with true -> x1 | false -> x2 less efficiently 
> than if e then x1 else x2 (bug report filed, but not fixed so far).
>
> Unless I'm greatly mistaken, this can be fixed by a mere syntactic 
> transformation using Camlp4. I suppose I'm not the first person to have 
> encountered these problems... So has anybody done the necessary Camlp4 
> scripts? :-)

Indeed, I've got such a camlp4 translator. I do not advertize it much, 
because it's not very robust. In particular, if you have defined your own 
customized "list" datatype or reused any of the Coq standard library 
names, that will lead to problems. Nevertheless, in normal situation, it 
will do what you expect. The script (containing instructions) is:

http://www.lri.fr/~letouzey/download/pp_extract.ml

In particular, there is a portion to uncomment if you want the sumbool 
type (left|right) to be translated to boolean and hence take advantage
of "if ... then ... else" syntax.

Cheers,

Pierre