The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Many thanks!  

One follow-up question: If I do

   Require ExtrOcamlString.

I get an error like this when compiling the generated OCaml code:

       Error: This expression has type 'a list/9
       but an expression was expected of type char list/1045

On the other hand, if I inline the contents of ExtrOcamlString, this error 
disappears and things work perfectly. 

Any idea why?

    - Benjamin


On Jul 25, 2012, at 11:02 AM, Paolo Herms wrote:

> 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 => "(=)".