The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

Dear Benjamin,

On 07/25/2012 04:22 PM, 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)

As far as I know, this is the best you can do.  Instead of cribbing,
I'd just do

Require Import ExtrOcamlString.

(While you're at it, "Require Import ExtrOcamlBasic." is pretty nice too.)

With ExtrOcamlString, you get Caml's "char list" type for Coq's
"string" type.  You can then convert to/from real Caml strings using
"explode" and "implode" from Batteries, or just write your own.  For
CompCert, I use

let camlstring_of_coqstring (s: char list) : string =
  let r = String.create (List.length s) in
  let rec fill pos = function
  | [] -> r
  | c :: s -> r.[pos] <- c; fill (pos + 1) s
  in fill 0 s

and have no use for the reverse conversion...

> to get something minimally working, but the embedded comments
> suggest that there ought to be a better way.

The comments just tell you that once Coq's "ascii" type is mapped to
Caml's "char", your code is going to be pretty inefficient (but still
correct, I think) if, on the Coq side, you take advantage of the
definition of "ascii" as a 8-tuple of bools.

Idea for a collaborative project: a *Caml* library of useful functions
to interface with Coq-extracted code.  Besides the string <-> char list
conversions above, it could provide conversions between Coq's various
integer types (nat, Z, N, positive) and Caml's (big_int, int, int32, int64)
[with overflow checking, mind you].  Direct, exact conversions between
strings and Coq's integer types would also be nice.  Floats would be
next, using Flocq on Coq's side.  And in CompCert, I found it invaluable
to have a Lisp-like notion of "atoms": hash-consed Caml strings
represented as positive integers on Coq's side.

Cheers,

- Xavier (jetlagged)