OCaml string and Coq string (Extraction from Coq to OCaml)

Question

I used the extraction from Coq to OCaml, where I have type Z, N, positive

I don't use to extract it in int of OCaml.

Then the type I have after the extraction is:

type positive =
| Coq_xI of positive
| Coq_xO of positive
| Coq_xH

type coq_N =
| N0
| Npos of positive

type coq_Z =
| Z0
| Zpos of positive
| Zneg of positive

I have a program in OCaml where some functions using the OCaml type string.

In my OCaml program, I need to write some functions convert the type: string -> coq_N, string -> coq_Z, string -> positive

I tried to write the functions in Coq and then used the extraction to get the OCaml type but Coq string is different from OCaml string.

For instance:

open Ascii
open BinNums
open Datatypes

type string =
| EmptyString
| String of ascii * string

let string_of_coqN (s: string): coq_N =
  match s with
    | EmptyString -> N0
    | String (a, _) -> (coq_N_of_ascii a);;

where coq_N_of_ascii is the extraction from coq function N_of_ascii.

When I applied the function string_of_coqN, for instance:

let test (x: string) = string_of_N x;;

I got the complain that

Error: This expression has type string but an expression was expected of type
         String0.string

Could you please help me to find a way to write the convert functions : string -> coq_N, string -> coq_Z and string -> positive?

score 4 · Accepted Answer · answered Sep 02 '14 at 12:15

For strings, the easiest thing to do is probably to import the standard library module ExtrOcamlString in your extraction file, which will cause Coq to extract them as a char list in OCaml. You can then convert between char list and native strings with custom code. Have a look for instance at file lib/Camlcoq.v in the CompCert distribution, functions camlstring_of_coqstring and coqstring_of_camlstring.

OCaml string and Coq string (Extraction from Coq to OCaml)

1 Answers1