Proposal to extend the Extraction Plugin with commands for synthesising externals and callbacks definitions for interfacing with C code more easily

[eladrion]

Dear Coq developers,

in my research and PhD project, I formalize software functionality in order to synthesize
certified code. But this (OCaml) code has to run in a framework, that is not implemented
in OCaml but in C/C++. So I use the OCaml FFI infrastructure to call the OCaml code as
callback and expose C functions to the synthesized code.

Obviously, it is possible to use Extract Constant for axiomatic function definitions to redirect
to a ML function and define that function to be an external somewhere else. But this can be
tedious and error prone since the correct types of the function have to be written by hand.
The latter problem is easily solved when doing this in Coq since the correct extraction types
are present. Also, in some cases it can be helpful to redirect the call to a defined (Coq) function to an alternative
implementation in C/C++ for testing purposes.
It is, as I see it, not possible to implement this functionality as an additional plugin.
The reason is, that the standard Extract Constant generates both a val declaration and let expression
which would collide with an additional external declaration during OCaml compilation.
One could merely redirect from the ML function call, generated from Extract Constant to the additional
definition. But this would make the synthesized code unnecessarily big.
Using Extract Inlined Constant would solve that. But the Synthesis of externals should happen
at the same time as synthesizing the rest of the code.

Furthermore, adding the callback registration for exposed ML functions can clearly
be done by hand. But this can be automatized and does not alter the rest of the synthesized code
but merely adds an additional function. Thus, I see no impact on type safety and correctness.

Thus, I adopted the current version of Coq for my purposes (including CoqIDE and documentation)
and it does the job quite well, so far. But I think, that there may be others, who can benefit from
that work and I would like to send in the changes for integration into Coq. Since this is not merely
a small change, I thought about creating a CEP, but according to the documentation, this should
be done before starting the implementation. So, it is obviously too late for that direction.

Thus, my question is: Should I nevertheless create a CEP or rather create a pull request
for the changes in my forked version of Coq (currently 1 commit ahead of coq/master)?

The branch is located under the extraction_extension
branch of my fork.

One side-note: I am aware, that it is possible to use CertiCoq for CLight extraction. But my projects include both OCaml and CLight synthesis.

Best regards,
Mario