17.2 Extraction options

17.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, another language called Toplevel is provided. It is a pseudo-Ocaml, 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 Toplevel.

17.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 session-independent 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 qualid1 ... qualidn.  

Extraction NoInline qualid1 ... qualidn.  

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: 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 non-explicitely required but needed for dependancy reasons, there are two cases:

17.2.3 Realizing axioms

It is possible to assume some axioms while developing a proof. Since these axioms can be any kind of proposition or object 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. 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.

The system actually provides a more general mechanism to specify ML terms even for defined constants, 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 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.
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.

Remarks:
  1. The extraction of a module depending on axioms from another module will not fail. It is the responsability of the ``extractor'' of that other module to realize the given axioms.
  2. Note that now, the Extract Inlined Constant command is sugar for an Extract Constant followed by a Extraction Inline. So be careful with Reset Extraction Inline.

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