This commit includes a proposal for extending the OCaml part of the e…

…xtraction plugin. The new functionality includes:

1) Adding the command Extract Foreign Constant which marks a qualid as external. During extraction, instead of generating
   `val qualid : type` in mli and `let qualid = mlname` in the ml file, only the expression `external qualid : type = "external_fun_name"` is generated in the ml file. This way, the OCaml compiler knows that the function will be resolved by the C compiler/linker
2) Adding the command Extract Callback qualid which marks a qualid as external. During extraction, additionally to the synthesised function, an OCaml callback registraction function call is synthesised which exposes the function in order to be able to call it from C as closure.
3) Print and Reset commands to show and reset the currently defined externals and callbacks
4) Adoptions to CoqIDE in order to highlight the new commands
5) Adoptions to the Extraction Plugin documentation with the new section "Generating FFI Code" that describes the functionality in more detail.
6) Tests in the test suite

With contributions by jfehrle, SkySkimmer and silene

doc/changelog/13-extraction/18270-master+fix18212-extractio-ocaml-ffi-extension.rst

@@ -0,0 +1,8 @@
+- **Added:**
+  Extension for OCaml extraction:
+  Commands to extract foreign function calls to C (external)
+  and ML function exposition (Callback.register) for calling
+  being able to call them by C functions
+  (`#18270 <https://github.com/coq/coq/pull/18270>`_,
+  fixes `#18212 <https://github.com/coq/coq/issues/18212>`_,
+  by Mario Frank).

doc/sphinx/addendum/extraction.rst

@@ -303,11 +303,18 @@ what ML term corresponds to a given axiom.
       by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline`
       will have an effect on the realized and inlined axiom.
 
-.. caution:: It is the responsibility of the user to ensure that the ML
-   terms given to realize the axioms do have the expected types. In
-   fact, the strings containing realizing code are just copied to the
-   extracted files. The extraction recognizes whether the realized axiom
-   should become a ML type constant or a ML object declaration. For example:
+   .. caution:: It is the responsibility of the user to ensure that the ML
+      terms given to realize the axioms do have the expected types. In
+      fact, the strings containing realizing code are just copied to the
+      extracted files. The extraction recognizes whether the realized axiom
+      should become a ML type constant or a ML object declaration. For example:
+
+   .. exn:: The term @qualid is already defined as foreign custom constant.
+
+      The :n:`@qualid` was previously used in a
+      :cmd:`Extract Foreign Constant` command. Using :cmd:`Extract Inlined Constant`
+      for :n:`@qualid` would override this command.
+
 
 .. coqtop:: in
 
@@ -366,25 +373,25 @@ native boolean type instead of the Coq one. The syntax is the following:
      into OCaml ``int``, the code to be provided has type:
      ``(unit->'a)->(int->'a)->int->'a``.
 
-.. caution:: As for :cmd:`Extract Constant`, this command should be used with care:
+   .. caution:: As for :cmd:`Extract Constant`, this command should be used with care:
 
-  * The ML code provided by the user is currently **not** checked at all by
-    extraction, even for syntax errors.
+     * The ML code provided by the user is currently **not** checked at all by
+       extraction, even for syntax errors.
 
-  * Extracting an inductive type to a pre-existing ML inductive type
-    is quite sound. But extracting to a general type (by providing an
-    ad-hoc pattern matching) will often **not** be fully rigorously
-    correct. For instance, when extracting ``nat`` to OCaml ``int``,
-    it is theoretically possible to build ``nat`` values that are
-    larger than OCaml ``max_int``. It is the user's responsibility to
-    be sure that no overflow or other bad events occur in practice.
+     * Extracting an inductive type to a pre-existing ML inductive type
+       is quite sound. But extracting to a general type (by providing an
+       ad-hoc pattern matching) will often **not** be fully rigorously
+       correct. For instance, when extracting ``nat`` to OCaml ``int``,
+       it is theoretically possible to build ``nat`` values that are
+       larger than OCaml ``max_int``. It is the user's responsibility to
+       be sure that no overflow or other bad events occur in practice.
 
-  * Translating an inductive type to an arbitrary ML type does **not**
-    magically improve the asymptotic complexity of functions, even if the
-    ML type is an efficient representation. For instance, when extracting
-    ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic.
-    It might be interesting to associate this translation with
-    some specific :cmd:`Extract Constant` when primitive counterparts exist.
+     * Translating an inductive type to an arbitrary ML type does **not**
+       magically improve the asymptotic complexity of functions, even if the
+       ML type is an efficient representation. For instance, when extracting
+       ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic.
+       It might be interesting to associate this translation with
+       some specific :cmd:`Extract Constant` when primitive counterparts exist.
 
 Typical examples are the following:
 
@@ -413,6 +420,98 @@ As an example of translation to a non-inductive datatype, let's turn
 
    Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
 
+Generating FFI Code
+~~~~~~~~~~~~~~~~~~~
+
+The plugin provides mechanisms to generate only OCaml code to
+interface the generated OCaml code with C programs. In order to link compiled
+OCaml code with C code, the linker needs to know
+
+   * which C functions will be called by the ML code (external)
+   * which ML functions shall be accessible by the C code (callbacks)
+
+.. cmd:: Extract Foreign Constant @qualid => @string
+
+   Like :cmd:`Extract Constant`, except that the referenced ML terms
+   will be declared in the form
+
+   ``external @qualid : ML type = "@string"``.
+
+   .. caution::
+
+      * The external function name :n:`@string` is not checked in any way.
+
+      * The user must ensure that the C functions given to realize the axioms have
+        the expected or compatible types. In fact, the strings containing realizing
+        code are just copied to the extracted files.
+
+   .. exn:: Extract Foreign Constant is supported only for OCaml extraction.
+
+      Foreign function calls are only supported for OCaml.
+
+   .. exn:: Extract Foreign Constant is supported only for functions.
+
+      This error is thrown if @qualid is of sort ``Type`` and external functions only
+      work for functions.
+
+   .. exn:: The term @qualid is already defined as inline custom constant.
+
+      The :n:`@qualid` was previously used in a
+      :cmd:`Extract Inlined Constant` command. Using :cmd:`Extract Foreign Constant`
+      for :n:`@qualid` would override this command.
+
+.. cmd:: Extract Callback {? @string } @qualid
+
+   This command makes sure that after extracting the :term:`constants <constant>`
+   specified by :n:`@qualid`, a constant ML function will be generated that
+   registers :n:`@qualid` as callback, callable by :n:`@string`.
+   This is done by declaring a function
+   ``let _ = Callback.register "@string" @qualid``
+   This expression signals OCaml that the given ML function :n:`@qualid` shall be
+   accessible via the alias :n:`@string`, when calling from C/C++.
+   If no alias is specified, it is set to the string representation of :n:`@qualid`.
+
+   .. caution::
+      * The optional alias :n:`@string` is currently **not** checked in any way.
+
+      * The user must ensure that the callback aliases are
+        unique, i.e. when multiple modules expose a callback, the user should make
+        sure that no two :n:`@qualid` share the same alias.
+
+   .. note::
+      Using Extract Callback has no impact on the rest of the synthesised code since
+      it is an additional declaration. Thus, there is no impact on the correctness
+      and type safety of the generated code.
+
+   .. exn:: Extract Callback is supported only for OCaml extraction.
+
+      The callback registration mechanism ``Callback.register`` is specific
+      to OCaml. Thus, the command is only usable when extracting OCaml code.
+
+.. cmd:: Print Extraction Foreign
+
+   Prints the current set of custom foreign functions
+   declared by the command :cmd:`Extract Foreign Constant` together with its
+   associated foreign ML function name.
+
+.. .. cmd:: Reset Extraction Foreign
+
+..   Resets the set of custom externals
+..   declared by the command :cmd:`Extract Foreign Constant`.
+
+.. cmd:: Print Extraction Callback
+
+   Prints the map of callbacks
+   declared by the command :cmd:`Extract Callback`,
+   showing the :token:`qualid` and callback alias
+   :token:`string` (if specified) for each callback.
+
+.. cmd:: Reset Extraction Callback
+
+   Resets the the map recording the callbacks
+   declared by the command :cmd:`Extract Callback`.
+
+
 Avoiding conflicts with existing filenames
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

doc/tools/docgram/fullGrammar

@@ -578,7 +578,12 @@ command: [
 | "Extraction" "Blacklist" LIST1 preident      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Callback" OPT string global      (* extraction plugin *)
+| "Print" "Extraction" "Callback"      (* extraction plugin *)
+| "Reset" "Extraction" "Callback"      (* extraction plugin *)
+| "Print" "Extraction" "Foreign"      (* extraction plugin *)
 | "Extract" "Constant" global LIST0 string "=>" mlname      (* extraction plugin *)
+| "Extract" "Foreign" "Constant" global "=>" string      (* extraction plugin *)
 | "Extract" "Inlined" "Constant" global "=>" mlname      (* extraction plugin *)
 | "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)

doc/tools/docgram/orderedGrammar

@@ -796,7 +796,12 @@ command: [
 | "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Callback" OPT string qualid      (* extraction plugin *)
+| "Print" "Extraction" "Callback"      (* extraction plugin *)
+| "Reset" "Extraction" "Callback"      (* extraction plugin *)
+| "Print" "Extraction" "Foreign"      (* extraction plugin *)
 | "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Foreign" "Constant" qualid "=>" string      (* extraction plugin *)
 | "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
 | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)

ide/coqide/coq.lang

@@ -181,7 +181,8 @@
         <context id="toplevel-command" style-ref="vernac-keyword">
           <keyword>Add</keyword>
           <keyword>Load</keyword>
-          <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
+          <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist|Callback)</keyword>
+          <keyword>Print\%{space}+Extraction\%{space}+Foreign</keyword>
           <keyword>Comments</keyword>
           <keyword>Solve\%{space}Obligation</keyword>
           <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
@@ -222,6 +223,7 @@
           <keyword>Implicit\%{space}Arguments</keyword>
           <keyword>Include</keyword>
           <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
+          <keyword>Extract\%{space}Foreign\%{space}Constant</keyword>
           <include>
             <context sub-pattern="1" style-ref="vernac-keyword"/>
             <context sub-pattern="qua" style-ref="identifier"/>
@@ -235,6 +237,7 @@
           <keyword>Import</keyword>
           <keyword>Export</keyword>
           <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
+          <keyword>Extract\%{space}Callback</keyword>
           <include>
             <context sub-pattern="1" style-ref="vernac-keyword"/>
             <context sub-pattern="qua_list" style-ref="identifier"/>

ide/coqide/coq_commands.ml

@@ -43,6 +43,8 @@ let commands = [
    "End Silent.";
    "Eval";
    "Extract Constant";
+   "Extract Foreign Constant";
+   "Extract Callback";
    "Extract Inductive";
    "Extraction Inline";
    "Extraction Language";
@@ -99,6 +101,8 @@ let commands = [
    "Require Export";
    "Require Import";
    "Reset Extraction Inline";
+(*   "Reset Extraction Foreign";*)
+   "Reset Extraction Callback";
    ];
   [  "Scheme";
      "Section";
@@ -169,6 +173,8 @@ let state_preserving = [
   "Print Coercion Paths";
   "Print Coercions";
   "Print Extraction Inline";
+  "Print Extraction External";
+  "Print Extraction Callback";
   "Print Grammar";
   "Print Graph";
   "Print Hint";

plugins/extraction/g_extraction.mlg

@@ -152,13 +152,49 @@ VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
   -> { reset_extraction_blacklist () }
 END
 
+(* Commands for setting, printing and resetting callbacks extraction. *)
+
+(* Defining a Coq object as ML callback for FFI call target from C *)
+VERNAC COMMAND EXTEND ExtractionCallback CLASSIFIED AS SIDEFF
+| [ "Extract" "Callback" string_opt(o) global(x) ]
+  -> { extract_callback o x }
+END
+
+VERNAC COMMAND EXTEND PrintExtractionCallback CLASSIFIED AS QUERY
+| [ "Print" "Extraction" "Callback" ]
+  -> {Feedback.msg_notice (print_extraction_callback ()) }
+END
+
+VERNAC COMMAND EXTEND ResetExtractionCallback CLASSIFIED AS SIDEFF
+| [ "Reset" "Extraction" "Callback" ]
+  -> { reset_extraction_callback () }
+END
+
+(* Commands for printing and resetting foreigns extraction. *)
+VERNAC COMMAND EXTEND PrintExtractionForeign CLASSIFIED AS QUERY
+| [ "Print" "Extraction" "Foreign" ]
+  -> {Feedback.msg_notice (print_extraction_foreign ()) }
+END
+
+(*
+VERNAC COMMAND EXTEND ResetExtractionForeign CLASSIFIED AS SIDEFF
+| [ "Reset" "Extraction" "Foreign" ]
+  -> { reset_extraction_foreign () }
+END
+*)
 
 (* Overriding of a Coq object by an ML one *)
 VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
   -> { extract_constant_inline false x idl y }
 END
 
+(* Overriding of a Coq object by an ML one that will be a FFI call to C *)
+VERNAC COMMAND EXTEND ExtractionForeignConstant CLASSIFIED AS SIDEFF
+| [ "Extract" "Foreign" "Constant" global(x) "=>" string(y) ]
+  -> { extract_constant_foreign x y }
+END
+
 VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
   -> { extract_constant_inline true x [] y }

plugins/extraction/ocaml.ml

@@ -599,11 +599,30 @@ let pp_decl = function
         hov 2 (str "type " ++ ids ++ name ++ def)
     | Dterm (r, a, t) ->
         let def =
-          if is_custom r then str (" = " ^ find_custom r)
+          (* If it it is an foreign custom, set the def to ': type =  <quote>foreign_fun_name<quote> '.
+             TODO: I'm not sure, but could we use pp_native_string for quoting the custom name of r?
+          *)
+          if is_foreign_custom r then str ": " ++ pp_type false [] t ++ str " = \"" ++ str (find_custom r) ++ str "\""
+          (* Otherwise, check if it is a regular custom term. *)
+          else if is_custom r then str (" = " ^ find_custom r)
           else pp_function (empty_env ()) a
         in
         let name = pp_global_name Term r in
-        pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
+        (* If it is an foreign custom, begin the expression with 'external'/'foreign' instead of 'let' *)
+        let expr_begin = if is_foreign_custom r then str "external " else str "let " in
+        (* Make sure that a callback registration is synthesised, if specified for that term. *)
+        let callback_def =
+          try
+            let alias =
+              match find_callback r with
+                | Some s -> str s
+                | None   -> name (* No alias specified, use the qualid name. *)
+            in
+            cut2 () ++ hov 0 ((str "let () = Stdlib.Callback.register \"") ++ alias ++ (str "\" ") ++ name)
+          with Not_found -> (* No callback registration specified for qualid. *)
+            mt()
+        in pp_val name t ++ hov 0 (expr_begin ++ name ++ def ++ mt ()) ++ callback_def;
+
     | Dfix (rv,defs,typs) ->
         pp_Dfix (rv,defs,typs)