#+TITLE: ~coqffi~ in a Nutshell

#+SERIES: ./Coqffi.html
#+SERIES_NEXT: ./CoqffiEcho.html

For each entry of a ~cmi~ file (a /compiled/ ~mli~ 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~.

#+BEGIN_EXPORT html
<nav id="generate-toc"></nav>
<div id="history">site/posts/CoqffiIntro.org</div>
#+END_EXPORT

* Getting Started

** Requirements

The latest version of ~coqffi~ (~1.0.0~beta7~ at the time of writing)
is compatible with OCaml ~4.08~ up to ~4.12~, and Coq ~8.12~ up top
~8.13~.  If you want to use ~coqffi~, but have incompatible
requirements of your own, feel free to
[[https://github.com/coq-community/coqffi/issues][submit an issue]].

** Installing ~coqffi~

The recommended way to install ~coqffi~ is through the
[[https://coq.inria.fr/opam/www][Opam Coq Archive]], in the ~released~
repository.  If you haven’t activated this repository yet, you can use
the following bash command.

#+BEGIN_SRC sh
opam repo add coq-released https://coq.inria.fr/opam/released
#+END_SRC

Then, installing ~coqffi~ is as simple as

#+BEGIN_SRC sh
opam install coq-coqffi
#+END_SRC

You can also get the source from
[[https://github.com/coq-community/coqffi][the upstream ~git~
repository]]. The ~README~ provides the necessary pieces of
information to build it from source.

** 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: [[https://github.com/Lysxia/coq-simple-io][~coq-simple-io~]] and [[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]]. It is
also possible to use it with [[https://github.com/DeepSpec/InteractionTrees][Interaction Trees]], albeit in a less
direct manner.

* 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 Seq.t=        | =CoqFFI.Data.Seq.t=           |
| ='a option=       | =Coq.Init.Datatypes.option a= |
| =('a, 'e) result= | =Coq.Init.Datatypes.sum=      |
| =string=          | =Coq.Strings.String.string=   |
| =unit=            | =Coq.Init.Datatypes.unit=     |
| =exn=             | =CoqFFI.Exn=                  |

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 [[https://github.com/coq/coq/pull/13559][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.

Sometimes, you may encounter a situation where you have two interface
modules ~b.mli~ and ~b.mli~, such that ~b.mli~ uses a type introduced
in ~a.mli~.  To deal with this scenario, you can use the ~--witness~
flag to generate ~A.v~.  This will tell ~coqffi~ to also generate
~A.ffi~; this file can then be used when generating ~B.v~ thanks to
the ~-I~ option.  Furthermore, for ~B.v~ to compile the ~--require~
option needs to be used to ensure the ~A~ Coq library (~A.v~) is
required.

To give a more concrete example, given ~a.mli~

#+BEGIN_SRC ocaml
type t
#+END_SRC

and ~b.mli~

#+BEGIN_SRC ocaml
type a = A.t
#+END_SRC

To generate ~A.v~, we can use the following commands:

#+BEGIN_SRC bash
ocamlc a.mli
coqffi --witness -o A.v a.cmi
#+END_SRC

Which would generate the following axiom for =t=.

#+BEGIN_SRC coq
Axiom t : Type.
#+END_SRC

Then, generating ~B.v~ can be achieved as follows:

#+BEGIN_SRC bash
ocamlc b.mli
coqffi -I A.ffi -ftransparent-types -r A -o B.v b.cmi
#+END_SRC

which results in the following output for =v=:

#+BEGIN_SRC coq
Require A.

Definition u : Type := A.t.
#+END_SRC

* Code Generation

~coqffi~ distinguishes five types of entries: types, pure values,
impure primitives, asynchronous primitives, exceptions, and
modules. We now discuss how each one of them is handled.

** Types

By default, ~coqffi~ generates axiomatized definitions for each type
defined in a ~.cmi~ file. This means that src_ocaml[:exports
code]{type t} becomes src_coq[:exports code]{Axiom t : Type}.
Polymorphism is supported, /i.e./, src_ocaml[:exports code]{type 'a t}
becomes src_coq[:exports code]{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=.

#+BEGIN_SRC ocaml
type 'a t [@@coq_model "list"]
#+END_SRC

This generates the following Coq definition.

#+BEGIN_SRC coq
Definition t : forall (a : Type), Type := list.
#+END_SRC

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.

Unamed polymorphic type parameters are also supported. In presence of
such parameters, ~coqffi~ will find it a name that is not already
used. For instance,

#+BEGIN_SRC ocaml
type (_, 'a) ast
#+END_SRC

becomes

#+BEGIN_SRC ocaml
Axiom ast : forall (b : Type) (a : Type), Type.
#+END_SRC

Finally, ~coqffi~ has got an experimental feature called
~transparent-types~ (enabled 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,

#+BEGIN_SRC ocaml
type 'a llist =
  | LCons of 'a * (unit -> 'a llist)
  | LNil
#+END_SRC

becomes

#+BEGIN_SRC coq
Inductive llist (a : Type) : Type :=
| LCons (x0 : a) (x1 : unit -> llist a) : llist a
| LNil : llist a.
#+END_SRC

Mutually recursive types are supported, so

#+BEGIN_SRC ocaml
type even = Zero | ESucc of odd
and odd = OSucc of even
#+END_SRC

becomes

#+BEGIN_SRC coq
Inductive odd : Type :=
| OSucc (x0 : even) : odd
with even : Type :=
| Zero : even
| ESucc (x0 : odd) : even.
#+END_SRC

Besides, ~coqffi~ supports alias types, as suggested in this write-up
when we discuss witness files.

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 [[https://coq.inria.fr/refman/language/core/inductive.html#positivity-condition][positivity condition]] is
satisfied.

** Pure values

~coqffi~ decides whether or not a given OCaml values is pure or impure
with the following heuristics:

- Constants are pure
- Functions are impure by default
- Functions with a =coq_model= annotation are pure
- Functions marked with the =pure= annotation are pure
- If the ~pure-module~ feature is enabled (~-fpure-module~),
  then synchronous functions (which do not live inside the [[https://ocsigen.org/lwt/5.3.0/manual/manual][~Lwt~]]
  monad) are pure

Similarly to types, ~coqffi~ generates axioms (or definitions, if the
~coq_model~ annotation is used) for pure values. Then,

#+BEGIN_SRC ocaml
val unpack : string -> (char * string) option [@@pure]
#+END_SRC

becomes

#+BEGIN_SRC coq
Axiom unpack : string -> option (ascii * string).
#+END_SRC

Polymorphic values are supported.

#+BEGIN_SRC ocaml
val map : ('a -> 'b) -> 'a list -> 'b list [@@pure]
#+END_SRC

becomes

#+BEGIN_SRC coq
Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b.
#+END_SRC

Again, unamed polymorphic type are supported, so

#+BEGIN_SRC ocaml
val ast_to_string : _ ast -> string [@@pure]
#+END_SRC

becomes

#+BEGIN_SRC coq
Axiom ast_to_string : forall (a : Type), string.
#+END_SRC

** Impure Primitives

~coqffi~ reserves a special treatment for /impure/ OCaml functions.
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) generate a typeclass which gathers these primitives,
and (2) generate instances of this typeclass for supported backends.

We illustrate the rest of this section with the following impure
primitives.

#+BEGIN_SRC ocaml
val echo : string -> unit
val scan : unit -> string
#+END_SRC

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.

#+BEGIN_SRC coq
Class MonadConsole (m : Type -> Type) := { echo : string -> m unit
                                         ; scan : unit -> m string
                                         }.
#+END_SRC

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.

#+BEGIN_SRC coq
Definition pipe `{Monad m, MonadConsole m} : m unit :=
  let* msg := scan () in
  echo msg.
#+END_SRC

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.

*** ~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

#+BEGIN_SRC coq
Axiom io_echo : string -> IO unit.
Axiom io_scan : unit -> IO string.

Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo
                                              ; scan := io_scan
                                              }.
#+END_SRC

It is enabled by default, but can be disabled using the
~-fno-simple-io~ command-line argument.

*** ~interface~

When this feature is enabled, ~coqffi~ generates an inductive type
which describes the set of primitives available, to be used with
frameworks like [[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]] or
[[https://github.com/DeepSpec/InteractionTrees][Interactions Trees]]

#+BEGIN_SRC coq
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
  }.
#+END_SRC

Providing an instance of the form src_coq[:exports code]{forall i,
Inject i M} is enough for your monad =M= to be compatible with this
feature (see for instance
[[https://github.com/ANSSI-FR/FreeSpec/blob/master/theories/FFI/FFI.v][how
FreeSpec implements it]]).

*** ~freespec~

When this feature in enabled, ~coqffi~ generates a semantics for the
inductive type generated by the ~interface~ feature.

#+BEGIN_SRC coq
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).
#+END_SRC

** Asynchronous Primitives

~coqffi~ also reserves a special treatment for /asynchronous/
primitives —/i.e./, functions which live inside the ~Lwt~ monad— when
the ~lwt~ feature is enabled.

The treatment is very analoguous to the one for impure primitives: (1)
a typeclass is generated (with the ~_Async~ suffix), and (2) an
instance for the ~Lwt~ monad is generated. Besides, an instance for
the “synchronous” primitives is also generated for ~Lwt~. If the
~interface~ feature is enabled, an interface datatype is generated,
which means you can potentially use Coq to reason about your
asynchronous programs (using FreeSpec and alike, although the
interleaving of asynchronous programs in not yet supported in
FreeSpec).

By default, the type of the ~Lwt~ monad is ~Lwt.t~. You can override
this setting using the ~--lwt-alias~ option.  This can be useful when
you are using an alias type in place of ~Lwt.t~.

** Exceptions

OCaml features an exception mechanism. Developers can define their
own exceptions using the ~exception~ keyword, whose syntax is similar
to constructors definition. For instance,

#+BEGIN_SRC ocaml
exception Foo of int * bool
#+END_SRC

introduces a new exception =Foo= which takes two parameters of type
=int= and =bool=. =Foo (x, y)= constructs of value of type =exn=.

For each new exceptions introduced in an OCaml module, ~coqffi~
generates (1) a so-called “proxy type,” and (2) conversion functions
to and from this type.

Coming back to our example, the “proxy type” generates by ~coqffi~ is

#+BEGIN_SRC coq
Inductive FooExn : Type :=
| MakeFooExn (x0 : i63) (x1 : bool) : FooExn.
#+END_SRC

Then, ~coqffi~ generates conversion functions.

#+BEGIN_SRC coq
Axiom exn_of_foo : FooExn -> exn.
Axiom foo_of_exn : exn -> option FooExn.
#+END_SRC

Besides, ~coqffi~ also generates an instance for the =Exn= typeclass
provided by the =CoqFFI= theory:

#+BEGIN_SRC coq
Instance FooExn_Exn : Exn FooExn :=
  { to_exn := exn_of_foo
  ; of_exn := foo_of_exn
  }.
#+END_SRC

Under the hood, =exn= is an [[https://caml.inria.fr/pub/docs/manual-ocaml/extensiblevariants.html][extensible datatype]], and how ~coqffi~
supports it will probably be generalized in future releases.

Finally, ~coqffi~ has a minimal support for functions which may raise
exceptions. Since OCaml type system does not allow to identify such
functions, they need to be annotated explicitely, using the
=may_raise= annotation. In such a case, ~coqffi~ will change the
return type of the function to use the =sum= Coq inductive type.

For instance,

#+BEGIN_SRC ocaml
val from_option : 'a option -> 'a [@@may_raise] [@@pure]
#+END_SRC

becomes

#+BEGIN_SRC coq
Axiom from_option : forall (a : Type), option a -> sum a exn.
#+END_SRC

** Modules

Lastly, ~coqffi~ supports OCaml modules described within ~mli~ files,
when they are specify as ~module T : sig ... end~. For instance,

#+BEGIN_SRC ocaml
module T : sig
  type t

  val to_string : t -> string [@@pure]
end
#+END_SRC

becomes

#+BEGIN_SRC coq
Module T.
  Axiom t : Type.

  Axiom to_string : t -> string.
End T.
#+END_SRC

As of now, the following construction is unfortunately *not*
supported, and will be ignored by ~coqffi~:

#+BEGIN_SRC coq
module S = sig
  type t

  val to_string : t -> string [@@pure]
end

module T : S
#+END_SRC

* 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 [[./CoqffiEcho.org][~coqffi~ can be used to easily implement an echo
server in Coq]].