diff options
author | Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-05-23 12:22:48 -0700 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-06-22 14:15:00 +0200 |
commit | 5089872d20c9e3089676c9267a6394e99cca5121 (patch) | |
tree | 1e2df6141c807761304e25d3328c7f2ebf2ec5c8 /plugins/extraction/ExtrHaskellZInt.v | |
parent | 949d027ce8fa94b5c62f938b58c3f85d015b177b (diff) |
Add efficient extraction of [nat], [Z], and [string] to Haskell
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
Diffstat (limited to 'plugins/extraction/ExtrHaskellZInt.v')
-rw-r--r-- | plugins/extraction/ExtrHaskellZInt.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v new file mode 100644 index 000000000..66690851a --- /dev/null +++ b/plugins/extraction/ExtrHaskellZInt.v @@ -0,0 +1,24 @@ +(** Extraction of [Z] into Haskell's [Int] *) + +Require Import ZArith. +Require Import ExtrHaskellZNum. + +(** + * Disclaimer: trying to obtain efficient certified programs + * by extracting [Z] into [Int] is definitively *not* a good idea. + * See comments in [ExtrOcamlNatInt.v]. + *) + +Extract Inductive positive => "Prelude.Int" [ + "(\x -> 2 Prelude.* x Prelude.+ 1)" + "(\x -> 2 Prelude.* x)" + "1" ] + "(\fI fO fH n -> if n Prelude.== 1 then fH () else + if Prelude.odd n + then fI (n `Prelude.div` 2) + else fO (n `Prelude.div` 2))". + +Extract Inductive Z => "Prelude.Int" [ "0" "(\x -> x)" "Prelude.negate" ] + "(\fO fP fN n -> if n Prelude.== 0 then fO () else + if n Prelude.> 0 then fP n else + fN (Prelude.negate n))". |