The Coq mailing list

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

On Mon, Aug 16, 2010 at 6:06 PM, Jianzhou Zhao 
<jianzhou AT seas.upenn.edu>
 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.
>
> Thanks. This works.
>
> Extract Inductive nat => "int" [ "0" "succ" ].
> Extract Constant plus => "fun a b -> a + b ".
> Definition _plus (a b:nat) := plus a b.
> Extraction "test" _plus.
>
> I had assumed that "Extract Constant" only works for Axioms.  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.
>
> 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?

This is not a question. It can extract to "Big_int.big_int" directly.

>
>>
>> Evgeny
>>
>>
>
>
>
> --
> Jianzhou
>



-- 
Jianzhou