The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hi,

some 2 cents.

Pierre Letouzey (Fri, Sep 16, 2005 at 01:41:49PM +0200):
> On Thu, Sep 15, 2005 at 04:22:33PM -0700, Adam Chlipala 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.
> 
> 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
> 
> 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. 

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.
E.g.:

--- File Extract_Peano.v:
Section Ocaml.
Extraction Language Ocaml.
Extract Preface "#open Big_int;;".
Extract Constant nat => "big_int".
Extract Constant plus => "add_big_int".
Extract Constant O => "zero_big_int".
Extract Constant minus => "minus_nat".
Extract Epilogue
   "let minus_nat m n =
       if le_big_int m n
       then zero_big_int
       else minus_big_int m n;;".
End Ocaml.

Section Haskell.
Extraction Language Haskell.
Extract Preface "import Big_int".
Extract Constant nat => "Integer".
Extract Constant plus => "(+)".
Extract Constant O => "0".
...
End Haskell.
---

Regards,
-- 
Stefan Karrmann