The Coq mailing list

["King, Oscar" <oscar.king.16 AT ucl.ac.uk>]

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