The Coq mailing list

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

Stefan Karrmann wrote:
> > > 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 you use Extract files? I.e. files which define how the export constants
> to different target languages. They would need an import clause (preface)
> and some helper functions in an epilogue.

This does part of the job, but, especially for the example of 'nat', 
it's also necessary to translate Coq 'match' expressions in a different 
way.  I've actually hacked up the extraction source to do this, and I'm 
successfully running the resulting code.