diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-06 13:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-06 13:23:28 +0200 |
| commit | d8b245d688ff64d17acd9e7591daf6d63b4e54f7 (patch) | |
| tree | 0e202d1f39e97844d94a873b30e4fb14fb481f84 /plugins | |
| parent | c53f2f75375dfffd2f258c76f5b722d37ab0daf9 (diff) | |
| parent | 5080991902a05ee720ab1d6fa1c9d592d3ffd36c (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrHaskellNatNum.v | 14 | ||||
| -rw-r--r-- | plugins/extraction/ExtrHaskellZNum.v | 4 |
2 files changed, 14 insertions, 4 deletions
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 979a1cdc4..244eb85fc 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -11,11 +11,12 @@ 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 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.<=)". @@ -23,5 +24,12 @@ 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 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 diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v index 3f645db9b..cbbfda75e 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)". |