The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

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.

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?

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?

Thanks!