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.
You can just import ExtrHaskellZInteger (documentation).