string_dec and string in Ocaml library

Question

I have file:

• String0.ml extracted from String.v (It is from Coq library)

• String.ml : is a string library of Ocaml

After extracted my test file from Coq to Ocaml, I want to used String.ml in the library of Ocaml, so I write an replace command to replace all String0 to String.

The problem is in the file test.v, I used one of the definition:

Definition beq_string := beq_dec string_dec.

function string_dec is not occur in the library of Ocaml, but it has in the string library of Coq

So I have an error when I compile test.ml

open String
let beq_string = beq_dec string_dec

Error: Unbound value string_dec

I want to used the string library of Ocaml for all my extraction files. How can I able to compile string_dec ?

Answer 1

Extract the string_dec function as well.

If you're willing to trust the OCaml library a little, you'll get a lot better performance by extracting beq_string to use the built-in equality on strings:

Extract Constant beq_string => "((=) : string->string->bool)".

Answer 2

Create a MyString.ml module containing :

module String0 = struct
  include String
  let string_dec = function ... (* the definition of string_dec *)
end

and in all your files generated by Coq, start by

open MyString

Then, you don't need to rename String0 into String, and it will use the functions defined in the String module, plus the string_dec function that you have defined.