The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Greg,

There are some optimizations in extraction plugin, which work on intermediate "MiniML" AST inside plugin. But I don't remember do these optimizations normalize terms or just scan let body for occurence of let variables.

Sincerely,
Kirill Taran

On Mon, Feb 10, 2014 at 10:29 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 10/02/2014 19:16, Greg Morrisett wrote:

I'm curious about the interaction of this feature with extraction.
In the example you gave:

Fixpoint f (x:nat) : nat := let y := f x in 0.

extraction to Ocaml yields:

   let rec f x = 0

This suggests that the body of a recursive function is
normalized before extraction.  But this example:

   Fixpoint g (x:nat) : nat :=
     let z1 := x * x in
     let z2 := z1 * z1 in
     let z3 := z2 * z2 in
     let z4 := g z3 * g z3 in
     z3 * z3.

yields the following Ocaml:

   let rec g x =
     let z1 = mult x x in
     let z2 = mult z1 z1 in
     let z3 = mult z2 z2 in
     mult z3 z3

so obviously, something more clever is happening.

I don't see any difference between your two examples: in both cases, unused let-bindings seem to be removed from the extracted code. Am I missing something?

Best regards,

Guillaume