Automatic generation of OCaml FFI code
- Dominant language
- C++
- Stars
- 165
- Forks
- 10
- PR merge metrics
- No merged PRs in 30d
Description
**Is your feature request related to a problem? Please describe.**
I have some first-order Rocq code that essentially manipulates records of integer values (i32,i64) and perform integer operation on them, which is not the best fit for OCaml's value representation. One nice feature would be to generate this code to C or C++, and then use the OCaml FFI to use this code from OCaml, so as to improve performance. I could be implementing this FFI code manually, but I was wondering if Crane could be generating it automatically instead? Is this something that you have considered? One benefit could be differential testing between the C++ and OCaml extraction, for instance.
**Describe the solution you'd like**
I think, we would extract a Rocq module M to three files:
- A file M.cpp corresponding to the current crane extraction;
- A file M_ffi.cpp that generates the OCaml <-> C++ glue;
- A file M.ml with the external definitions, to make it available to OCaml
**Describe alternatives you've considered**
Writing the glue code manually. The main issue is keeping this glue code in sync with Crane's output, especially if the generated C++ API changes.
Contributor guide
Research direction
Start by reading Crane’s current extraction behavior and the generated C++ API, then compare it with the proposed M.cpp, M_ffi.cpp, and M.ml outputs. Done would mean a defined generation path for all three files that keeps the OCaml glue synchronized with the C++ output and supports the suggested differential testing.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp, ocaml
- Domain
- compilers
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Quiet
- Clarity
- Needs clarification
- Newbie friendliness
- 30/100