diff options
| author | Nickolai Zeldovich | 2015-07-16 18:31:00 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2015-09-03 18:11:32 +0200 |
| commit | 5c060d56a9d94d74cdeca6f6b424306218e81562 (patch) | |
| tree | 0fefa957d9eee140b55299bfa3d8d4505c230b9c /plugins | |
| parent | c7fd3cb7945bcd385ace06f583d1b57681c8716d (diff) | |
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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrHaskellZNum.v | 4 |
1 files changed, 3 insertions, 1 deletions
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)". |