[Coq-Club] Redefinition of extracted parameter

[King, Oscar]

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

[Maximilian Wuttke]

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

Post by King, Oscar
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
*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
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