Extraction to Haskell Int type

Using Coq
1

Hello,

I am trying to extract my project into Haskell. I have a type that handles memory addresses which I want to extract to Haskell Int (instead of Integer).
Which standard library numeric type should I use for this?

1 Like
2

It seems to me that you are looking for the Extract Constant command
https://coq.inria.fr/refman/addendum/extraction.html

Here you can find a more detailed explanation of how to properly extract your programs
https://softwarefoundations.cis.upenn.edu/vfa-current/Extract.html

3

Use the following (add more as necessary)

Require Import Extraction.
Extraction Language Haskell.

Extract Inductive list => "[]" [ "[]" "(:)" ].
Extract Inductive prod => "(,)"  [ "(,)" ].
Extract Inductive sum => "Prelude.Either"  [ "Prelude.Left" "Prelude.Right" ].
Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ] "(\fO fS n -> if n Prelude.== 0 then fO () else fS (Prelude.pred n))".

Extract Constant plus => "(Prelude.+)".
Extract Constant andb => "(Prelude.&&)".
Extract Constant fst => "Prelude.fst".
Extract Constant snd => "Prelude.snd".