From c7fd3cb7945bcd385ace06f583d1b57681c8716d Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Thu, 16 Jul 2015 18:24:19 -0400 Subject: Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v The previous extraction of [Nat.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Nat.modulo], with the same check for modulo-by-zero. --- plugins/extraction/ExtrHaskellNatNum.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 979a1cdc41..81d76a5ffa 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -11,7 +11,6 @@ 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.+)". @@ -23,5 +22,8 @@ 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))". +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 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)". -- cgit v1.2.3 From 5c060d56a9d94d74cdeca6f6b424306218e81562 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Thu, 16 Jul 2015 18:31:00 -0400 Subject: Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v The previous extraction of [Z.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Z.modulo], with the same check for modulo-by-zero. --- plugins/extraction/ExtrHaskellZNum.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v index 3f645db9b1..cbbfda75e5 100644 --- a/plugins/extraction/ExtrHaskellZNum.v +++ b/plugins/extraction/ExtrHaskellZNum.v @@ -12,8 +12,10 @@ Require Import EqNat. Extract Inlined Constant Z.add => "(Prelude.+)". Extract Inlined Constant Z.sub => "(Prelude.-)". Extract Inlined Constant Z.mul => "(Prelude.*)". -Extract Inlined Constant Z.div => "Prelude.div". Extract Inlined Constant Z.max => "Prelude.max". Extract Inlined Constant Z.min => "Prelude.min". Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)". Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)". + +Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". +Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". -- cgit v1.2.3 From b5c646a37ac0375f9fbb2427549c925ee3f127ad Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 Sep 2015 19:37:22 +0200 Subject: Improve directives for Haskell extraction of nat. --- plugins/extraction/ExtrHaskellNatNum.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'plugins') diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 81d76a5ffa..244eb85fc2 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -15,6 +15,8 @@ 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.<=)". @@ -24,6 +26,10 @@ 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