coqffi

coqffi generates the necessary Coq boilerplate to use OCaml functions in a Coq development, and configures the Coq extraction mechanism accordingly.

Meta

• 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:
  • Cmdliner 1.0.4 or later
  • Sexplib 0.14 or later
  • Dune 2.5 or later
• Coq namespace: CoqFFI
• Related publication(s): none

Building and installation instructions

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-coqffi

Example

Suppose 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 -> unit

coqffi 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.