The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

No that's the good way of extracting characters.
It is a hard-coded in the extraction plugin that if there is a binding from 
Coq ascii to OCaml char, then a Coq ascii like 
Ascii true false false false false true true false
will be extracted to the OCaml char 'a'.
Try it:

Require ExtrOcamlString.
Open Scope char_scope.
Definition a := "a".
Extraction a.

So the comments that bothered you won't appear by extraction, unless you do 
pattern matching on some asciis in your Coq code. 
That's for the character type. For the string type, it would be dangerous to 
extract it to OCaml strings, as these are mutable, so you should stick with 
the extraction to lists of chars.
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Wednesday 25 July 2012 16:23:07 Benjamin C. Pierce wrote:
> 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 => "(=)".