Coq/Ocaml project using heuristic function written in C?

Using Coq
1

Hi,

I’m writing to seek some knowledge/suggestions about the building system of Coq/OCaml:

I’m implementing a compiler pass for CompCert. This pass uses a heuristic to optimize a program (which does not influence the correctness proof).

We have an existing implementation of this heuristic in C, but not in Coq. The specification of this heuristic is as simple a function from a list of numbers (positive type) (or pairs of numbers) to another number

One thing I learned is that there exists support to use a C function in an OCaml program. Since the CompCert project written in Coq will eventually be converted to an OCaml program, I believe this could be a way we can directly use that heuristic in the C version, instead of re-implementing it in Coq.

However, I barely have developing experience in OCaml projects and I’m not very familiar with its building system, and no idea how to actually implement an OCaml program that uses C function. (And I’m even doing this in a Coq project)

So I’m posting this to seek help and suggestions on where should I get started to learn so I can eventually connect my implementations and make them a compilable/executable project.

Thank you!

2

First thing, I would look at the following documentation: OCaml - Interfacing C with OCaml
Second thing, I would be careful that Coq-extracted programs may use they own notion of integers (Ocaml integers are 31-bit or 63-bit, bounded integers, while Coq sometimes unbounded integers, which would be extracted to Coq as a different datatype), you will need to pay attention to this when converting the integers from C to data that your version of CompCert can use.