The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 25 Jul 2012 10:22:51 -0400,
"Benjamin C. Pierce" 
<bcpierce AT cis.upenn.edu>
 a écrit :

> Does someone have an example of an OCaml program extracted from Coq
> that illustrates the "correct" way to extract the Coq string type?
> I've been able to use the code below (cribbed from
> Coq.extraction.ExtrOcamlString) to get something minimally working,
> but the embedded comments suggest that there ought to be a better way.
> 
> Thanks,
> 
>    - Benjamin
> 
> 
> Require Import Ascii String.
> Extract Inductive ascii => char
> [
> "(* If this appears, you're using Ascii internals. Please don't *)
> (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> let f b i = if b then 1 lsl i else
> 0 in Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 +
> f b6 6 + f b7 7))" ] "(* If this appears, you're using Ascii
> internals. Please don't *) (fun f c -> let n = Char.code c in let h i
> = (n land (1 lsl i)) <> 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h
> 6) (h 7))". Extract Constant zero => "'\000'". Extract Constant one
> => "'\001'". Extract Constant shift => "fun b c -> Char.chr
> (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". Extract
> Inlined Constant ascii_dec => "(=)".
> 
> 

You may be interested in this bug report (or rather a feature request):
https://coq.inria.fr/bugs/show_bug.cgi?id=2747

For conversion to char you don’t have to do anything, importing
"ExtrOcamlString" (as it seems you did) is enough.

As far as I remember, there is no extraction to Ocaml strings,
although it would be possible (see the patch in the bug report) for
constant strings (so, remove your "Extract Inductive ascii => char."
as well as your "Extract Constant zero => '\000'.".).
Note however, that it wouldn't be very safe, as strings in Ocaml are
mutable.

In fact, I am the author of the suggested patch, but I do not remember
very well what I did, and on what version of Coq it could apply (I
guess the current trunk should work, as this patch is less than one
year old, and the extraction process does not seem to be very active
now, although I would really like to see GADT of Ocaml 4.0 and Haskell
being available for extraction).