The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

Hi Oscar,

I think the command `Extract Constant foo => "foo"` is what you seek.
This extracts the Coq axiom `foo` with the OCaml code "foo".
This way you can implement `foo` as a OCaml function instead of a Coq
function.

See the documentation at:
<https://coq.inria.fr/distrib/current/refman/addendum/extraction.html#realizing-axioms>


Sincerely
Maximilian

On 9/26/18 5:59 PM, King, Oscar wrote:
> Hi again,
> 
> 
> Sorry I should have been a little more specific. If I have the following
> code. In file 2 I then try to mask the definition of foo in file 1. This
> is not going to work because file1 still uses the definition of foo in
> file 1. It will compile but will fail when you try to run it. Say I have
> other files and use foo elsewhere. It may occur that I use file2.foo
> whilst it expects file1.foo or vice versa, which can be an issue. 
> 
> 
> In my case I want to declare a hashing function as a parameter call it
> "hash_x" and defer implementation to OCaml. It will extract as foo does.
> 
> 
> Is there a way of doing this or do I need to define everything in coq?
> 
> 
> Thanks,
> 
> 
> Oscar
> 
> 
> Parameter foo: nat -> nat -> nat.
> Definition bar x y:= foo x y.
> Require Extraction.
> Recursive Extraction bar.
> 
> (* Extracted Code *)
> type nat =
> | O
> | S of nat
> 
> (** val foo : nat -> nat -> nat **)
> 
> let foo =
>   failwith "AXIOM TO BE REALIZED"
> 
> (** val bar : nat -> nat -> nat **)
> 
> let bar =
>   foo
> 
> (* File 2 *)
> 
> let foo = x + y
> 
> 
> 
> ------------------------------------------------------------------------
> *From:* King, Oscar
> *Sent:* Friday, September 21, 2018 3:44:59 PM
> *To:* 
> coq-club AT inria.fr
> *Subject:* Redefinition of extracted parameter
>  
> Hi,
> 
> I’m trying to extract some code with parameters that I want to define in
> OCaml however when I extract and try to redefine by defining function or
> type with the same name I get type conflicts between files. I have
> constructed an example below:
> 
> How would I redefine foo in the extracted code properly?
> 
> Thanks in advance,
> 
> Oscar
> 
> Parameter foo: nat -> nat -> nat.
> 
> Definition bar x := foo x.
> 
> Require Extraction.
> 
> Recursive Extraction bar.
> 
> (* Extracted Code *)
> type nat =
> | O
> | S of nat
> 
> (** val foo : nat -> nat -> nat **)
> 
> let foo =
>   failwith "AXIOM TO BE REALIZED"
> 
> (** val bar : nat -> nat -> nat **)
> 
> let bar =
>   foo
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature