Chapter 18 Extraction of programs in Objective Caml and Haskell
JeanChristophe Filliātre and Pierre Letouzey
The status of extraction is experimental.
We present here the Coq extraction commands, used to build certified
and relatively efficient functional programs, extracting them from the
proofs of their specifications. The functional languages available as
output are currently Objective Caml, Haskell and Scheme.
In the following, ``ML'' will be used (abusively) to refer to any of
the three.
Differences with old versions.
The current extraction mechanism is new for version 7.0 of Coq.
In particular, the F_{omega} toplevel used as an intermediate step between
Coq and ML has been withdrawn. It is also not possible
any more to import ML objects in this F_{omega} toplevel.
The current mechanism also differs from
the one in previous versions of Coq: there is no more
an explicit toplevel for the language (formerly called Fml).
18.1 Generating ML code
The next two commands are meant to be used for rapid preview of
extraction. They both display extracted term(s) inside Coq.
 Extraction qualid.
Extracts one constant or module in the Coq toplevel.
 Recursive Extraction qualid_{1} ... qualid_{n}.
Recursive extraction of all the globals (or modules) qualid_{1} ...
qualid_{n} and all their dependencies in the Coq toplevel.
All the following commands produce real ML files. User can choose to produce
one monolithic file or one file per Coq library.
 Extraction "file"
qualid_{1} ... qualid_{n}.
Recursive extraction of all the globals (or modules) qualid_{1} ...
qualid_{n} and all their dependencies in one monolithic file file.
Global and local identifiers are renamed according to the choosen ML
language to fullfill its syntactic conventions, keeping original
names as much as possible.
 Extraction Library ident.
Extraction of the whole Coq library ident.v to an ML module
ident.ml. In case of name clash, identifiers are here renamed
using prefixes coq_
or Coq_
to ensure a
sessionindependent renaming.
 Recursive Extraction Library ident.
Extraction of the Coq library ident.v and all other modules
ident.v depends on.
The list of globals qualid_{i} does not need to be
exhaustive: it is automatically completed into a complete and minimal
environment.
18.2 Extraction options
18.2.1 Setting the target language
The ability to fix target language is the first and more important
of the extraction options. Default is Ocaml. Besides Haskell and
Scheme, another language called Toplevel is provided. It is a pseudoOcaml,
with no renaming on global names: so names are printed as in Coq.
This third language is available only at the Coq Toplevel.
 Extraction Language Ocaml.
 Extraction Language Haskell.
 Extraction Language Scheme.
 Extraction Language Toplevel.
18.2.2 Inlining and optimizations
Since Objective Caml is a strict language, the extracted
code has to be optimized in order to be efficient (for instance, when
using induction principles we do not want to compute all the recursive
calls but only the needed ones). So the extraction mechanism provides
an automatic optimization routine that will be
called each time the user want to generate Ocaml programs. Essentially,
it performs constants inlining and reductions. Therefore some
constants may not appear in resulting monolithic Ocaml program (a warning is
printed for each such constant). In the case of modular extraction,
even if some inlining is done, the inlined constant are nevertheless
printed, to ensure sessionindependent programs.
Concerning Haskell, such optimizations are less useful because of
lazyness. We still make some optimizations, for example in order to
produce more readable code.
All these optimizations are controled by the following Coq options:

Set Extraction Optimize.

Unset Extraction Optimize.
Default is Set. This control all optimizations made on the ML terms
(mostly reduction of dummy beta/iota redexes, but also simplications on
Cases, etc). Put this option to Unset if you want a ML term as close as
possible to the Coq term.

Set Extraction AutoInline.

Unset Extraction AutoInline.
Default is Set, so by default, the extraction mechanism feels free to
inline the bodies of some defined constants, according to some heuristics
like size of bodies, useness of some arguments, etc. Those heuristics are
not always perfect, you may want to disable this feature, do it by Unset.

Extraction Inline qualid_{1} ... qualid_{n}.

Extraction NoInline qualid_{1} ... qualid_{n}.
In addition to the automatic inline feature, you can now tell precisely to
inline some more constants by the Extraction Inline command. Conversely,
you can forbid the automatic inlining of some specific constants by
the Extraction NoInline command.
Those two commands enable a precise control of what is inlined and what is not.

Print Extraction Inline.
Prints the current state of the table recording the custom inlinings
declared by the two previous commands.

Reset Extraction Inline.
Puts the table recording the custom inlinings back to empty.
Inlining and printing of a constant declaration.
A user can explicitely asks a constant to be extracted by two means:

by mentioning it on the extraction command line
 by extracting the whole Coq module of this constant.
In both cases, the declaration of this constant will be present in the
produced file.
But this same constant may or may not be inlined in the following
terms, depending on the automatic/custom inlining mechanism.
For the constants nonexplicitely required but needed for dependancy
reasons, there are two cases:

If an inlining decision is taken, wether automatically or not,
all occurences of this constant are replaced by its extracted body, and
this constant is not declared in the generated file.
 If no inlining decision is taken, the constant is normally
declared in the produced file.
18.2.3 Realizing axioms
Extraction will fail if it encounters an informative
axiom not realized (see section 18.2.3).
A warning will be issued if it encounters an logical axiom, to remind
user that inconsistant logical axioms may lead to incorrect or
nonterminating extracted terms.
It is possible to assume some axioms while developing a proof. Since
these axioms can be any kind of proposition or object or type, they may
perfectly well have some computational content. But a program must be
a closed term, and of course the system cannot guess the program which
realizes an axiom. Therefore, it is possible to tell the system
what ML term corresponds to a given axiom.
 Extract Constant qualid => string.
Give an ML extraction for the given constant.
The string may be an identifier or a quoted string.
 Extract Inlined Constant qualid => string.
Same as the previous one, except that the given ML terms will
be inlined everywhere instead of being declared via a let.
Note that the Extract Inlined Constant command is sugar
for an Extract Constant followed by a Extraction Inline.
Hence a Reset Extraction Inline will have an effect on the
realized and inlined xaxiom.
Of course, it is the responsability 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 in the
extracted files. The extraction recognize whether the realized axiom
should become a ML type constant or a ML object declaration.
Example:
Coq < Axiom X:Set.
X is assumed
Coq < Axiom x:X.
x is assumed
Coq < Extract Constant X => "int".
Coq < Extract Constant x => "0".
Notice that in the case of type scheme axiom (i.e. whose type is an
arity, that is a sequence of product finished by a sort), then some type
variables has to be given. The syntax is then:
 Extract Constant qualid string_{1} ...string_{n} => string.
The number of type variable given is checked by the system.
Example:
Coq < Axiom Y : Set > Set > Set.
Y is assumed
Coq < Extract Constant Y "'a" "'b" => " 'a*'b ".
Realizing an axiom via Extract Constant is only useful in the
case of an informative axiom (of sort Type or Set). A logical axiom
have no computational content and hence will not appears in extracted
terms. But a warning is nonetheless issued if extraction encounters a
logical axiom. This warning reminds user that inconsistant logical
axioms may lead to incorrect or nonterminating extracted terms.
If an informative axiom has not been realized before an extraction, a
warning is also issued and the definition of the axiom is filled with
an exception labelled AXIOM TO BE REALIZED. The user must then
search these exceptions inside the extracted file and replace them by
real code.
The system also provides a mechanism to specify ML terms for inductive
types and constructors. For instance, the user may want to use the ML
native boolean type instead of Coq one. The syntax is the following:
 Extract Inductive qualid => string [ string ...string ].
Give an ML extraction for the given inductive type. You must specify
extractions for the type itself (first string) and all its
constructors (between square brackets). The ML extraction must be an
ML recursive datatype.
Example: Typical examples are the following:
Coq < Extract Inductive unit => "unit" [ "()" ].
Coq < Extract Inductive bool => "bool" [ "true" "false" ].
Coq < Extract Inductive sumbool => "bool" [ "true" "false" ].
18.3 Differences between Coq and ML type systems
Due to differences between Coq and ML type systems,
some extracted programs are not directly typable in ML.
We now solve this problem (at least in Ocaml) by adding
when needed some unsafe casting Obj.magic, which give
a generic type 'a to any term.
For example, Here are two kinds of problem that can occur:

If some part of the program is very polymorphic, there
may be no ML type for it. In that case the extraction to ML works
all right but the generated code may be refused by the ML
typechecker. A very well known example is the distrpair
function:
Definition dp :=
fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C>C) => (f A x, f B y).
In Ocaml, for instance, the direct extracted term would be:
let dp x y f = Pair((f () x),(f () y))
and would have type:
dp : 'a > 'a > (unit > 'a > 'b) > ('b,'b) prod
which is not its original type, but a restriction.
We now produce the following correct version:
let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y))
 Some definitions of Coq may have no counterpart in ML. This
happens when there is a quantification over types inside the type
of a constructor; for example:
Inductive anything : Set := dummy : forall A:Set, A > anything.
which corresponds to the definition of an ML dynamic type.
In Ocaml, we must cast any argument of the constructor dummy.
Even with those unsafe castings, you should never get error like
``segmentation fault''. In fact even if your program may seem
illtyped to the Ocaml typechecker, it can't go wrong: it comes
from a Coq welltyped terms, so for example inductives will always
have the correct number of arguments, etc.
More details about the correctness of the extracted programs can be
found in [84].
We have to say, though, that in most ``realistic'' programs, these
problems do not occur. For example all the programs of Coq library are
accepted by Caml typechecker without any Obj.magic (see examples below).
18.4 Some examples
We present here two examples of extractions, taken from the
Coq Standard Library. We choose Objective Caml as target language,
but all can be done in the other dialects with slight modifications.
We then indicate where to find other examples and tests of Extraction.
18.4.1 A detailed example: Euclidean division
The file Euclid contains the proof of Euclidean division
(theorem eucl_dev). The natural numbers defined in the example
files are unary integers defined by two constructors O and S:
Coq < Inductive nat : Set :=
Coq <  O : nat
Coq <  S : nat > nat.
This module contains a theorem eucl_dev, and its extracted term
is of type
forall b:nat, b > 0 > forall a:nat, diveucl a b
where diveucl is a type for the pair of the quotient and the modulo.
We can now extract this program to Objective Caml:
Coq < Require Import Euclid.
Coq < Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
Coq < Recursive Extraction eucl_dev.
type nat =
 O
 S of nat
type sumbool =
 Left
 Right
(** val minus : nat > nat > nat **)
let rec minus n m =
match n with
 O > O
 S k > (match m with
 O > S k
 S l > minus k l)
(** val le_lt_dec : nat > nat > sumbool **)
let rec le_lt_dec n m =
match n with
 O > Left
 S n0 > (match m with
 O > Right
 S n1 > le_lt_dec n0 n1)
(** val le_gt_dec : nat > nat > sumbool **)
let le_gt_dec n m =
le_lt_dec n m
type diveucl =
 Divex of nat * nat
(** val eucl_dev : nat > nat > diveucl **)
let rec eucl_dev b a =
match le_gt_dec b a with
 Left > let Divex (x, x0) = eucl_dev b (minus a b) in Divex ((S x), x0)
 Right > Divex (O, a)
The inlining of gt_wf_rec and lt_wf_rec is not
mandatory. It only enhances readability of extracted code.
You can then copypaste the output to a file euclid.ml or let
Coq do it for you with the following command:
Coq < Extraction "euclid" eucl_dev.
The file euclid.ml has been created by extraction.
The file euclid.mli has been created by extraction.
Let us play the resulting program:
# #use "euclid.ml";;
type sumbool = Left  Right
type nat = O  S of nat
type diveucl = Divex of nat * nat
val minus : nat > nat > nat = <fun>
val le_lt_dec : nat > nat > sumbool = <fun>
val le_gt_dec : nat > nat > sumbool = <fun>
val eucl_dev : nat > nat > diveucl = <fun>
# eucl_dev (S (S O)) (S (S (S (S (S O)))));;
 : diveucl = Divex (S (S O), S O)
It is easier to test on Objective Caml integers:
# let rec i2n = function 0 > O  n > S (i2n (n1));;
val i2n : int > nat = <fun>
# let rec n2i = function O > 0  S p > 1+(n2i p);;
val n2i : nat > int = <fun>
# let div a b =
let Divex (q,r) = eucl_dev (i2n b) (i2n a) in (n2i q, n2i r);;
div : int > int > int * int = <fun>
# div 173 15;;
 : int * int = 11, 8
18.4.2 Another detailed example: Heapsort
The file Heap.v
contains the proof of an efficient list sorting algorithm described by
Bjerner. Is is an adaptation of the wellknown heapsort
algorithm to functional languages. The main function is treesort, whose type is shown below:
Coq < Require Import Heap.
Coq < Check treesort.
treesort
: forall (A : Set) (leA eqA : relation A),
(forall x y : A, {leA x y} + {leA y x}) >
forall eqA_dec : forall x y : A, {eqA x y} + {~ eqA x y},
(forall x y z : A, leA x y > leA y z > leA x z) >
forall l : list A,
{m : list A  sort leA m & permutation eqA eqA_dec l m}
Let's now extract this function:
Coq < Extraction Inline sort_rec is_heap_rec.
Coq < Extraction NoInline list_to_heap.
Coq < Extraction "heapsort" treesort.
The file heapsort.ml has been created by extraction.
The file heapsort.mli has been created by extraction.
One more time, the Extraction Inline and NoInline
directives are cosmetic. Without it, everything goes right,
but the output is less readable.
Here is the produced file heapsort.ml:
type nat =
 O
 S of nat
type 'a sig2 =
'a
(* singleton inductive, whose constructor was exist2 *)
type sumbool =
 Left
 Right
type 'a list =
 Nil
 Cons of 'a * 'a list
type 'a multiset =
'a > nat
(* singleton inductive, whose constructor was Bag *)
type 'a merge_lem =
'a list
(* singleton inductive, whose constructor was merge_exist *)
(** val merge : ('a1 > 'a1 > sumbool) > ('a1 > 'a1 > sumbool) >
'a1 list > 'a1 list > 'a1 merge_lem **)
let rec merge leA_dec eqA_dec l1 l2 =
match l1 with
 Nil > l2
 Cons (a, l) >
let rec f = function
 Nil > Cons (a, l)
 Cons (a0, l3) >
(match leA_dec a a0 with
 Left > Cons (a,
(merge leA_dec eqA_dec l (Cons (a0, l3))))
 Right > Cons (a0, (f l3)))
in f l2
type 'a tree =
 Tree_Leaf
 Tree_Node of 'a * 'a tree * 'a tree
type 'a insert_spec =
'a tree
(* singleton inductive, whose constructor was insert_exist *)
(** val insert : ('a1 > 'a1 > sumbool) > ('a1 > 'a1 > sumbool) >
'a1 tree > 'a1 > 'a1 insert_spec **)
let rec insert leA_dec eqA_dec t a =
match t with
 Tree_Leaf > Tree_Node (a, Tree_Leaf, Tree_Leaf)
 Tree_Node (a0, t0, t1) >
let h3 = fun x > insert leA_dec eqA_dec t0 x in
(match leA_dec a0 a with
 Left > Tree_Node (a0, t1, (h3 a))
 Right > Tree_Node (a, t1, (h3 a0)))
type 'a build_heap =
'a tree
(* singleton inductive, whose constructor was heap_exist *)
(** val list_to_heap : ('a1 > 'a1 > sumbool) > ('a1 > 'a1 >
sumbool) > 'a1 list > 'a1 build_heap **)
let rec list_to_heap leA_dec eqA_dec = function
 Nil > Tree_Leaf
 Cons (a, l0) >
insert leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l0) a
type 'a flat_spec =
'a list
(* singleton inductive, whose constructor was flat_exist *)
(** val heap_to_list : ('a1 > 'a1 > sumbool) > ('a1 > 'a1 >
sumbool) > 'a1 tree > 'a1 flat_spec **)
let rec heap_to_list leA_dec eqA_dec = function
 Tree_Leaf > Nil
 Tree_Node (a, t0, t1) > Cons (a,
(merge leA_dec eqA_dec (heap_to_list leA_dec eqA_dec t0)
(heap_to_list leA_dec eqA_dec t1)))
(** val treesort : ('a1 > 'a1 > sumbool) > ('a1 > 'a1 > sumbool)
> 'a1 list > 'a1 list sig2 **)
let treesort leA_dec eqA_dec l =
heap_to_list leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l)
Let's test it:
# #use "heapsort.ml";;
type sumbool = Left  Right
type nat = O  S of nat
type 'a tree = Tree_Leaf  Tree_Node of 'a * 'a tree * 'a tree
type 'a list = Nil  Cons of 'a * 'a list
val merge :
('a > 'a > sumbool) > 'b > 'a list > 'a list > 'a list = <fun>
val heap_to_list :
('a > 'a > sumbool) > 'b > 'a tree > 'a list = <fun>
val insert :
('a > 'a > sumbool) > 'b > 'a tree > 'a > 'a tree = <fun>
val list_to_heap :
('a > 'a > sumbool) > 'b > 'a list > 'a tree = <fun>
val treesort :
('a > 'a > sumbool) > 'b > 'a list > 'a list = <fun>
One can remark that the argument of treesort corresponding to
eqAdec is never used in the informative part of the terms,
only in the logical parts. So the extracted treesort never use
it, hence this 'b argument. We will use () for this
argument. Only remains the leAdec
argument (of type 'a > 'a > sumbool) to really provide.
# let leAdec x y = if x <= y then Left else Right;;
val leAdec : 'a > 'a > sumbool = <fun>
# let rec listn = function 0 > Nil
 n > Cons(Random.int 10000,listn (n1));;
val listn : int > int list = <fun>
# treesort leAdec () (listn 9);;
 : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons
(5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil)))))))))
Some tests on longer lists (10000 elements) show that the program is
quite efficient for Caml code.
18.4.3 The Standard Library
As a test, we propose an automatic extraction of the
Standard Library of Coq. In particular, we will find back the
two previous examples, Euclid and Heapsort.
Go to directory contrib/extraction/test of the sources of Coq,
and run commands:
make tree; make
This will extract all Standard Library files and compile them.
It is done via many Extraction Module, with some customization
(see subdirectory custom).
The result of this extraction of the Standard Library can be browsed
at URL
http://www.lri.fr/~letouzey/extraction.
This test works also with Haskell. In the same directory, run:
make tree; make f Makefile.haskell
The haskell compiler currently used is hbc. Any other should
also work, just adapt the Makefile.haskell. In particular ghc is known to work.
18.4.4 Extraction's horror museum
Some pathological examples of extraction are grouped in the file
contrib/extraction/test_extraction.v
of the sources of Coq.
18.4.5 Users' Contributions
Several of the Coq Users' Contributions use extraction to produce
certified programs. In particular the following ones have an automatic
extraction test (just run make in those directories):

Bordeaux/Additions
 Bordeaux/EXCEPTIONS
 Bordeaux/SearchTrees
 Dyade/BDDS
 Lannion
 Lyon/CIRCUITS
 Lyon/FIRINGSQUAD
 Marseille/CIRCUITS
 Muenchen/Higman
 Nancy/FOUnify
 Rocq/ARITH/Chinese
 Rocq/COC
 Rocq/GRAPHS
 Rocq/HIGMAN
 SophiaAntipolis/Stalmarck
 Suresnes/BDD
Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are
the only examples of developments where Obj.magic are needed.
This is probably due to an heavy use of impredicativity.
After compilation those two examples run nonetheless,
thanks to the correction of the extraction [84].