The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

Hi

On Thu, Sep 15, 2005 at 04:22:33PM -0700, Adam Chlipala wrote:
> I am interested in using Coq's extraction facilities to speed the 
> checking of proofs by reflection.  However, the very literal translation 
> that I get with commands like "Recursive Extraction" has some 
> opportunities for optimizations that lead to asymptotic improvements, 
> are easy to implement on typed OCaml ASTs, but that the OCaml compiler 
> is not smart enough to perform.

Some code optimizations are already there. They help removing some
obvious stupidities in the extracted code, but I'm far from pretending
these optims are always done in a rational way, so they may sometimes
introduce more problems that they solve. The most up-to-date document
about them is my PhD thesis, pages 127-139:
 http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz
Of course, the very brave can also have a look at the source code, in
contrib/extraction/mlutil.ml, around function simpl. Please feel free
to make suggestions about these optims.

> 
> For example, I would like to replace all uses of Coq's nat with uses of 
> OCaml's int, relying on dynamic checks to determine when the 
> representation is not precise enough and abort the execution.  I can 
> think of some simple type-directed syntactic rewrite rules that would 
> accomplish this, and there are a number of other basic but very 
> worthwhile optimizations of this kind.
> 
> Can anyone point me to an existing tool that performs such optimizations?

This kind of idea is somewhere in my TODO list, but doing it properly
isn't obvious. First, as you mention, using int may lead to overflows
that must be dealt with. Anyway, a nice alternative (although not as
fast) can be to use ocaml Bigint numbers. Then this translation
shouldn't be done naively, otherwise the time complexity won't change.
For instance, the usual extraction of the Peano.plus fonction is

let rec plus n m =
  match n with
    | O -> m
    | S p -> S (plus p m)

You can perfectly translate it into an int counterpart: 

let rec plus n m =
  match n with
    | 0 -> m
    | sp -> let p = sp-1 in 1+(plus p m)

But of course, this can't compete with the native (+) operation. So
the question isn't so much the change of datatype, but the change of 
basic operations coming along. This might be done using a "view"
mechanism, but isn't done yet. 

In the meantime, you can use "handwritten" solutions: use an
axiomatized datatype: 
 Parameter int:Set. 
 Parameter plus: int->int->int. 
 ...
And then realize this datatype with the ocaml int, by using Extract
Constant. Even better, you can now design a modular interface Int,
work with respect to this interface (in a functor), and plug later
your functorized extracted code with a concrete ocaml implementation.

Of course, there are some drawbacks to these "pedestrian" approaches:
you loose the existing librairies, as well as the ability to reduce
1+2 to 3 in Coq, and the ability to use tactics like omega, that
unlike the ring tactic, cannot (yet?) be used on user-defined
datatypes.

> 
> Also, the Coq'Art book mentions extraction optimizations that lead to 
> the removal of any 'sig0' types, the use of 'bool' instead of 'sumbool', 
> etc., in the extracted program.  These don't seem to be applied for 
> "Recursive Extraction" in my installation of Coq 8, even after I run 
> "Set Extraction Optimize.".  Is there some way I can enable them?
> 

The points you mention here aren't (speed) optimizations, but rather
better pretty printing. So the Extraction Optimize (that is "on" by
default anyway) has no effect on them.

Concerning the sig0 issue, I used to think that it was "pedagogical"
to leave them, since they show where a {..|..} used to be. Several
complains convinced me of the contrary, so the Coq CVS version now get
rid of sig0 during extraction. 

Turning sumbool into bool is really a matter of taste, and it's not so
clear that "Left" should be considered "true". Similarly, one may
expect extracted code to reuse ocaml lists instead of redefining
them. Such things that I'm slightly relucted to implement inside the
extraction can be done with a camlp4 pretty printer: see 
  http://www.pps.jussieu.fr/~letouzey/download/pp_extract.ml

Thanks for your interest in extraction, 
Pierre Letouzey