coqffi generates the necessary Coq boilerplate to use OCaml functions in a
Coq development, and configures the Coq extraction mechanism accordingly.
- Author(s):
- Thomas Letan
- Li-yao Xia
- Yann Régis-Gianas
- Yannick Zakowski
- Coq-community maintainer(s):
- Thomas Letan (@lthms)
- License: MIT License
- Compatible Coq versions: 8.12 or later
- Compatible OCaml versions: 4.08 or later
- Additional dependencies:
- Coq namespace:
CoqFFI - Related publication(s): none
Make sure your OPAM installation points to the official Coq repository as documented here, and then, the following should work:
git clone https://github.com/coq-community/coqffi.git
cd coqffi
opam install .Alternatively, you can install coqffi’s dependencies (as listed in
the Meta section of the README), then build it.
git clone https://github.com/coq-community/coqffi.git
cd coqffi
./src-prepare.sh
dune build -p coq-coqffiSuppose the following OCaml header file (file.mli) is given:
type fd
val std_out : fd
val fd_equal : fd -> fd -> bool [@@pure]
val openfile : string -> fd
val closefile : fd -> unit
val read_all : fd -> string
val write : fd -> string -> unitcoqffi then generates the necessary Coq boilerplate to use these
functions in a Coq development:
(* This file has been generated by coqffi. *)
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.
From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.
From CoqFFI Require Import Interface.
(** * Types *)
Axiom fd : Type.
Extract Constant fd => "Examples.File.fd".
(** * Pure functions *)
Axiom std_out : fd.
Axiom fd_equal : fd -> fd -> bool.
Extract Constant std_out => "Examples.File.std_out".
Extract Constant fd_equal => "Examples.File.fd_equal".
(** * Impure Primitives *)
(** ** Monad Definition *)
Class MonadFile (m : Type -> Type) : Type :=
{ openfile : string -> m fd
; closefile : fd -> m unit
; read_all : fd -> m string
; write : fd -> string -> m unit
}.
(** ** [IO] Instance *)
Axiom io_openfile : string -> IO fd.
Axiom io_closefile : fd -> IO unit.
Axiom io_read_all : fd -> IO string.
Axiom io_write : fd -> string -> IO unit.
Extract Constant io_openfile
=> "(fun x0 k__ -> k__ (Examples.File.openfile x0))".
Extract Constant io_closefile
=> "(fun x0 k__ -> k__ (Examples.File.closefile x0))".
Extract Constant io_read_all
=> "(fun x0 k__ -> k__ (Examples.File.read_all x0))".
Extract Constant io_write
=> "(fun x0 x1 k__ -> k__ (Examples.File.write x0 x1))".
Instance IO_MonadFile : MonadFile IO :=
{ openfile := io_openfile
; closefile := io_closefile
; read_all := io_read_all
; write := io_write
}.
(* The generated file ends here. *)The generated module may introduce additional dependency to your
project. For instance, the simple-io feature (enabled by default)
generates the necessary boilerplate to use the impure primitives of
the input module within the IO monad introduced by the
coq-simple-io package.
See the coqffi man pages for more information on how to use it.