The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Mon, Aug 16, 2010 at 06:06:25PM -0400, Jianzhou Zhao wrote:
> On Mon, Aug 16, 2010 at 4:23 PM, Evgeny Makarov 
> <emakarov AT gmail.com>
>  wrote:
> > Jianzhou,
> >
> >> I think Coq extraction
> >> (http://coq.inria.fr/refman/Reference-Manual027.html#toc139) only
> >> allows to realize inductive Coq types into inductive OCaml types.  But
> >> OCaml's int or big_bit is only primitive.
> >
> > The Reference Manual section 21.2.4 (at least after trunk 13264) has
> > an example of extracting the inductive Coq type nat to OCaml type int.
> > The command is "Extract Inductive". You can also probably use "Extract
> > Constant" to map functions on a Coq type into built-in OCaml
> > functions.
> 

Hi

Indeed, I've recently extended the Extract Inductive to support
extraction to non-inductive types. In addition to current trunk,
this is also part of 8.3 branch, and hence will be available in the
forthcoming release. You can indeed have a look at the documentation,
or directly inspect new files like plugins/extraction/ExtrOcamlNatBigInt.v.
Direct access:

https://gforge.inria.fr/scm/viewvc.php/*checkout*/trunk/plugins/extraction/ExtrOcamlNatBigInt.v?root=coq

This file and a few others at the same location illustrate various
advanced things you can do with extraction. There are nonetheless a
few caveats (mentionned in these files) : for instance the ocaml code
given to coq by the user is simply *not* check at all for the moment,
just copy-pasted somewhere in the extracted file. Moreover, algorithms
using nat have most of the time an inherently *bad* complexity, it's
quite tricky (or even impossible) to change that with only a few Extract
Inductive/Constant commands.


> Thanks. This works.
> 
> Extract Inductive nat => "int" [ "0" "succ" ].

Well, I haven't thought of this one. The extension I'm mentionning
above expects a last string to be passed to Extract Inductive,
in order to know how to translate pattern matching. For instance:

Extract Inductive nat => int [ "0" "succ" ]
 "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

More details in the documentation. But the command you propose isn't
strictly speaking wrong, since this last string is optional. It just
works only as long as you don't have pattern matching in your
extracted code. For nat for instance, you won't go very far, unless
you make an intensive usage of Extract Constant.
A nice point is that you can use your command even with Coq < 8.3 :-).
As I said above, the strings are not checked, hence Coq 8.2 is quite
happy with your command.


> I had assumed that "Extract Constant" only works for Axioms.

No, you can indeed "overload" full definitions of Coq this way.
As said above, use with care, it's quite easy to break things this
way. 

> The reference also gives such syntax to extract constant:
>   Coq < Extract Constant plus "’a" "’b" => " ’a*’b"
> What is the symbol before a and b, I tried ' and `, it extracted
>   let rec plus -> ’a*’b
> I might use a wrong symbol.

This syntax shouldn't be used for functions, but only for type
declarations. For instance, if you have a type parameter
mytype : Type -> Type, you can extract it to some known ocaml type:

Extract Constant mytype "'a" => "'a list".

Gives in the extracted code:

type 'a mytype = 'a list

> 
> If the extracted type, say 'big_int', is not in a module opened by
> default, can we also specify OCaml dependencies, adding 'open Big_int'
> before extracted code?
> 

As you said in your next mail, the solution is to use Big_int.big_int
and so on. I acknowledge this isn't pretty. Anyway, the Big_int module
of ocaml is already _so_ ugly: with all operators starting with big_int_...
what's the use of having them in a module, then ??. I suggest using
my small wrapper big.ml:

https://gforge.inria.fr/scm/viewvc.php/*checkout*/trunk/plugins/extraction/big.ml?root=coq

I might add someday a command to tell Coq to glue a particular
header such that "open Foo" or some conclusion to the extracted file...

Best regards,

Pierre Letouzey