From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- plugins/extraction/ExtrHaskellNatNum.v | 35 ++++++++++++++++++++++++++++++++++ 1 file changed, 35 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 00000000..244eb85f --- /dev/null +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -0,0 +1,35 @@ +(** + * 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.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 Init.Nat.max => "Prelude.max". +Extract Inlined Constant Init.Nat.min => "Prelude.min". +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 Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". +Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". +Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". +Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". + +Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". +Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". +Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". +Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". \ No newline at end of file -- cgit v1.2.3