diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-07-16 18:24:19 -0400 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 18:11:32 +0200 |
| commit | c7fd3cb7945bcd385ace06f583d1b57681c8716d (patch) | |
| tree | efac429eaa0db1782ee5d08a464e46a6a1677f35 /plugins/extraction/ExtrHaskellNatNum.v | |
| parent | b06d3badbf5a8aa95e5150c2dc0b3fd44e1269ab (diff) | |
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.
Diffstat (limited to 'plugins/extraction/ExtrHaskellNatNum.v')
| -rw-r--r-- | plugins/extraction/ExtrHaskellNatNum.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 979a1cdc4..81d76a5ff 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)". |