coq-club AT inria.fr

Subject: The Coq mailing list

List archive

I've been trying to extract some CoRN functions to usable Haskell

code without any success. I'd be grateful if someone could help:

As an example, I tried to extract the following function which

computes e^1 * 10^3 rounded off to an integer:

(** assuming CoRN is in the loadpath*)

Require Import CRexp.

Extraction Language Haskell.

Definition answer (n:positive) (r:CR) : Z :=

let m := (iter_pos _ (Pmult 10) 1%positive n) in

let (a,b) := (approximate r (1#m)%Qpos)*m in

Zdiv a b.

Definition test := answer 3 (exp (1))%CR.

Eval vm_compute in test. (** immediately produces the correct answer (2718) *)

Recursive Extraction test.

Using Coq 8.5beta, the extracted Haskell code can be found at:

I manually added the last 9 lines of code so that I could see the

output of the test function (above). Other than that, I made no change.

Using ghci 7.6.3, it often prints 3 digits correctly, but segfaults the rest of the times.

Using ghc 7.6.3, running the compiled executable always segfaults.

Using ghci 7.8.3, it often prints 3 digits correctly, but prints 0 the rest of the times

Using ghc 7.8.3, running the compiled executable always prints 0.

I'm baffled by this wide range of behaviour.

Any advice for fixing this issue will be very much appreciated.

Also, note that Coq warned me about extracting opaque bodies.

I've included that warning at the top of the file linked above.

Could that be the problem? I'd guess not because I sometimes get the correct answer.

Is this a bug in GHC?

Thanks,

-- Abhishek