The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

On Tue, Aug 17, 2010 at 2:16 PM, Pierre Letouzey
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> 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 defines almost all operations I wanted to extract from nat
to big_int. :) I think these were not included in 8.3-beta0-1 yet. But
I can still use these extractions if I can replace all functions that
pattern match nat in this way.

>
> 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.

I looked into 
https://gforge.inria.fr/scm/viewvc.php/*checkout*/trunk/plugins/extraction/ExtrOcamlNatInt.v?root=coq
It comments that

(*
  ...
    This file is hence provided mainly for testing / prototyping
    purpose. For serious use of numbers in extracted programs,
    you are advised to use either coq advanced representations
    (positive, Z, N, BigN, BigZ) or modular/axiomatic representation.
*)

To use positive, Z, N, BigN, BigZ, do we still do the similar
extractions ExtrOcamlNatInt.v does for nat? Because positive, Z, N,
BigN, BigZ are still inductively defined, and I also noticed that
https://gforge.inria.fr/scm/viewvc.php/*checkout*/trunk/plugins/extraction/big.ml?root=coq
defines pattern-matching extractions for them. Can we do anything
better with them than nat?

For 'modular/axiomatic representation', does that mean how
http://coq.inria.fr/stdlib/Coq.ZArith.Int.html works? I guess the idea
is to define an abstract datatype (assuming it can be realized into Z)
with axioms to describe behaviors of this abstract type, and
definitions that are eventually extracted into Big_int should use
these axioms with this abstract datatype. Am I correct? The relevant
question is how to ensure axioms are consistent if I am adding new
ones.

But I don't know which solution in these two ones is more convenient
in practice?


>
>
>> 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

Thanks.

>
>>
>> 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
>



-- 
Jianzhou