How to extract Coq's Z into Haskell's Integer

Question

I'm trying to extract to Haskell a program in Coq that uses Z numbers. I want to map Coq's Z to Haskell's Integer.

I found some libraries for doing that aiming OCaml, but not aiming Haskell. There is no library for that?

I need the extractions (found here):

Extract Inductive positive => "Big.big_int"
 [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".

Extract Inductive Z => "Big.big_int"
 [ "Big.zero" "" "Big.opp" ] "Big.z_case".

Extract Inductive N => "Big.big_int"
 [ "Big.zero" "" ] "Big.n_case".

but aiming Haskell.

I'll just ask: how to do it?.

But secondly, I should say why I couldn't do it myself:

I guess I can't come up with that myself possibly because I'm misunderstanding somethings, for example: why there is a empty string in the second definition? The definition of Z has three constructors: Z0, Zpos and Zneg. I don't see how "Big.zero" "" "Big.opp" is related with this.

Also, I didn't understand how the last string works: "...a final extra string that indicates how to perform pattern-matching over this inductive type." (found in documentation).

The chapter Extraction of S.F. says that "we give an OCaml expression that can be used as a "recursor" over elements of the type. (Think Church numerals.)".

How the code bellow is a recursor or does pattern-maching?

  "(fun zero succ n →
      if n=0 then zero () else succ (n-1))".

After I understand those things, I hope that I can create, myself, the extractions that I may ever need.

Answer 1

You can just import ExtrHaskellZInteger (documentation).