From 5089872d20c9e3089676c9267a6394e99cca5121 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sat, 23 May 2015 12:22:48 -0700 Subject: 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 --- plugins/extraction/ExtrHaskellNatNum.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 plugins/extraction/ExtrHaskellNatNum.v (limited to 'plugins/extraction/ExtrHaskellNatNum.v') diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v new file mode 100644 index 000000000..979a1cdc4 --- /dev/null +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -0,0 +1,27 @@ +(** + * Efficient (but uncertified) extraction of usual [nat] functions + * into equivalent versions in Haskell's Prelude that are defined + * for any [Num] typeclass instances. Useful in combination with + * [Extract Inductive nat] that maps [nat] onto a Haskell type that + * implements [Num]. + *) + +Require Import Arith. +Require Import EqNat. + +Extract Inlined Constant Nat.add => "(Prelude.+)". +Extract Inlined Constant Nat.mul => "(Prelude.*)". +Extract Inlined Constant Nat.div => "Prelude.div". +Extract Inlined Constant Nat.max => "Prelude.max". +Extract Inlined Constant Nat.min => "Prelude.min". +Extract Inlined Constant Init.Nat.add => "(Prelude.+)". +Extract Inlined Constant Init.Nat.mul => "(Prelude.*)". +Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)". +Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)". +Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)". +Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)". +Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)". +Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)". + +Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))". +Extract Constant minus => "(\n m -> Prelude.max 0 (n Prelude.- m))". -- cgit v1.2.3