coqffi
in a Nutshell
For each entry of a cmi
file, coqffi
tries to generate an
equivalent (from the extraction mechanism perspective) Coq
definition. In this article, we walk through how coqffi
works.
Note that we do not dive into the vernacular commands coqffi
generates. They are of no concern for users of coqffi
.
Revisions
This revisions table has been automatically generated
from the git
history
of this website repository, and the change
descriptions may not always be as useful as they
should.
You can consult the source of this file in its current version here.
2020-12-10 | Spellchecking and revisions table for the coqffi articles | 9098a01 |
2020-12-10 | Add a Series on coqffi, and the first literate program of this blog | 2706544 |
1 Getting Started
1.1 Requirements
The latest version of coqffi
(1.0.0~beta2
at the time of writing)
is compatible with OCaml 4.08
up to 4.11
, and Coq 8.12
. If you
want to use coqffi
, but have incompatible requirements of your own,
feel free to submit
an issue.
1.2 Installing coqffi
The recommended way to install coqffi
is through the
Opam Coq Archive, in the released
repository. If you haven’t activated this repository yet, you can use
the following bash command.
opam repo add coq-released https://coq.inria.fr/opam/released
Then, installing coqffi
is as simple as
opam install coq-coqffi
You can also get the source from
the upstream git
repository. The README
provides the necessary pieces of
information to build it from source.
1.3 Additional Dependencies
One major difference between Coq and OCaml is that the former is pure,
while the latter is not. Impurity can be modeled in pure languages,
and Coq does not lack of frameworks in this respect. coqffi
currently supports two of them:
coq-simple-io
and
FreeSpec. It is also
possible to use it with
Interaction Trees,
albeit in a less direct manner.
2 Primitive Types
coqffi
supports a set of primitive types, i.e., a set of OCaml
types for which it knows an equivalent type in Coq. The list is the
following (the Coq types are fully qualified in the table, but not in
the generated Coq module as the necessary Import
statement are
generated too).
OCaml type | Coq type |
---|---|
bool
|
Coq.Init.Datatypes.bool
|
char
|
Coq.Strings.Ascii.ascii
|
int
|
CoqFFI.Data.Int.i63
|
'a list
|
Coq.Init.Datatypes.list a
|
'a option
|
Coq.Init.Datatypes.option a
|
string
|
Coq.Strings.String.string
|
unit
|
Coq.Init.Datatypes.unit
|
The i63
type is introduced by the CoqFFI
theory to provide signed
primitive integers to Coq users. They are implemented on top of the
(sadly unsigned) Coq native integers introduced in Coq
8.10
. Hopefully, the i63
type will be deprecated once signed
primitive integers find their way to Coq upstream.
When processing the entries of a given interface model, coqffi
will
check that they only use these types, or types introduced by the
interface module itself.
3 Code Generation
coqffi
distinguishes three types of entries: types, pure functions,
and impure primitives. We now discuss how each one of them is handled.
3.1 Types
By default, coqffi
generates axiomatized definitions for each type
defined in a .cmi
file. This means that type t
becomes Axiom t : Type
.
Polymorphism is supported, i.e., type 'a t
becomes Axiom t : forall (a : Type), Type
.
It is possible to provide a “model” for a type using the coq_model
annotation, for instance for reasoning purposes. For instance,
we can specify that a type is equivalent to a list
.
type 'a t [@@coq_model "list"]
This generates the following Coq definition.
Definition t : forall (a : Type), Type := list.
It is important to be careful when using the coq_model
annotation.
More precisely, the fact that t
is a list
in the “Coq universe”
shall not be used while the implementation phase, only the
verification phase.
Finally, coqffi
has got an experimental feature called
transparent-types
(enable by using the -ftransparent-types
command-line argument). If the type definition is given in the module
interface, then coqffi
tries to generates an equivalent definition
in Coq. For instance,
type 'a llist = | LCons of 'a * (unit -> 'a llist) | LNil
becomes
Inductive llist (a : Type) : Type := | LCons (x0 : a) (x1 : unit -> llist a) : llist a | LNil : llist a.
Mutually recursive types are supported, so
type even = Zero | ESucc of odd and odd = OSucc of even
becomes
Inductive odd : Type := | OSucc (x0 : even) : odd with even : Type := | Zero : even | ESucc (x0 : odd) : even.
The transparent-types
feature is experimental, and is currently
limited to variant types. It notably does not support
records. Besides, it may generate incorrect Coq types, because it does
not check whether or not the
positivity
condition is satisfied.
3.2 Pure Functions
coqffi
assumes OCaml values are pure by default, and will generate
regular axiomatized Coq definitions for them. Similarly to type
entries, it is possible to provide a Coq model using the coq_module
annotation.
val unpack : string -> (char * string) option
becomes
Axiom unpack : string -> option (ascii * string).
Polymorphic functions are supported.
val map : ('a -> 'b) -> 'a list -> 'b list
becomes
Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b.
3.3 Impure Primitives
Finally, coqffi
reserves a special treatment for OCaml value
explicitly marked as impure, using the impure
annotation. Impurity
is usually handled in pure programming languages by means of monads,
and coqffi
is no exception to the rule.
Given the set of impure primitives declared in an interface module,
coqffi
will (1) generates a typeclass which gathers these
primitives, and (2) generates instances of this typeclass for
supported backends.
We illustrate the rest of this section with the following impure primitives.
val echo : string -> unit [@@impure] val scan : unit -> string [@@impure]
where echo
allows writing something the standard output, and scan
to read the standard input.
Assuming the processed module interface is named console.mli
, the
following Coq typeclass is generated.
Class MonadConsole (m : Type -> Type) := { echo : string -> m unit ; scan : unit -> m string }.
Using this typeclass and with the additional support of an additional
Monad
typeclass, we can specify impure computations which interacts
with the console. For instance, with the support of ExtLib
, one can
write.
Definition pipe `{Monad m, MonadConsole m} : m unit := let* msg := scan () in echo msg.
There is no canonical way to model impurity in Coq, but over the years several frameworks have been released to tackle this challenge.
coqffi
provides three features related to impure primitives.
3.3.1 simple-io
When this feature is enabled, coqffi
generates an instance of the
typeclass for the IO
monad introduced in the coq-simple-io
package
Axiom io_echo : string -> IO unit. Axiom io_scan : unit -> IO string. Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo ; scan := io_scan }.
It is enabled by default, but can be disabled using the
-fno-simple-io
command-line argument.
3.3.2 interface
When this feature is enabled, coqffi
generates an inductive type
which describes the set of primitives available, to be used with
frameworks like FreeSpec or
Interactions Trees
Inductive CONSOLE : Type -> Type := | Echo : string -> CONSOLE unit | Scan : unit -> CONSOLE string. Definition inj_echo `{Inject CONSOLE m} (x0 : string) : m unit := inject (Echo x0). Definition inj_scan `{Inject CONSOLE m} (x0 : unit) : m string := inject (Scan x0). Instance Inject_MonadConsole `{Inject CONSOLE m} : MonadConsole m := { echo := inj_echo ; scan := inj_scan }.
Providing an instance of the form forall i, Inject i M
is enough for your monad M
to be compatible with this
feature (see for instance
how
FreeSpec implements it).
3.3.3 freespec
When this feature in enabled, coqffi
generates a semantics for the
inductive type generated by the interface
feature.
Axiom unsafe_echo : string -> unit. Axiom unsafe_scan : uint -> string. Definition console_unsafe_semantics : semantics CONSOLE := bootstrap (fun a e => local match e in CONSOLE a return a with | Echo x0 => unsafe_echo x0 | Scan x0 => unsafe_scan x0 end).
4 Moving Forward
coqffi
comes with a comprehensive man page. In addition, the
interested reader can proceed to the next article of this series,
which explains how coqffi
can be used to easily
implement an echo server in Coq.