git.iko.soy/Idris-dev
on master help sign in
Make `div` and `mod` behave consistently

These functions now satisfy the following equality for all builtin integral types: ``` (div a b) * b + (mod a b) = a ``` Fixes #3592, #3740

commitbe90757a9295351473207e453ef41714210aeae8 authorAlex Queiroz <asandroq@gmail.com> dateFri 20 Oct 2017, 01:07 (9 years ago) parent9400779
6 files changed+185−10
compare with master
unifiedsplit
rts/idris_gmp.c+1−1 src/Idris/Primitives.hs+8−8 test/TestData.hs+2−1 test/basic024/expected+76 test/basic024/input+93 test/basic024/run+5
rts/idris_gmp.c+1−1
@@ -195,7 +195,7 @@ VAL bigMod(VM* vm, VAL x, VAL y) {
195195 VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
196196 idris_doneAlloc();
197197 bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
198− mpz_mod(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
198+ mpz_tdiv_r(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
199199 SETTY(cl, CT_BIGINT);
200200 cl -> info.ptr = (void*)bigint;
201201 return cl;
src/Idris/Primitives.hs+8−8
@@ -205,7 +205,7 @@ intArith ity =
205205 [ iBinOp ity "add" (bitBin ity (+)) (LPlus . ATInt) total
206206 , iBinOp ity "sub" (bitBin ity (-)) (LMinus . ATInt) total
207207 , iBinOp ity "mul" (bitBin ity (*)) (LTimes . ATInt) total
208− , iBinOp ity "udiv" (bitBin ity div) LUDiv partial
208+ , iBinOp ity "udiv" (bitBin ity quot) LUDiv partial
209209 , iBinOp ity "sdiv" (bsdiv ity) (LSDiv . ATInt) partial
210210 , iBinOp ity "urem" (bitBin ity rem) LURem partial
211211 , iBinOp ity "srem" (bsrem ity) (LSRem . ATInt) partial
@@ -285,17 +285,17 @@ bsrem ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `rem` (ord y))
285285bsrem _ _ = Nothing
286286
287287bsdiv :: IntTy -> [Const] -> Maybe Const
288−bsdiv ITBig [BI x, BI y] = Just . BI $ x `div` y
288+bsdiv ITBig [BI x, BI y] = Just . BI $ x `quot` y
289289bsdiv (ITFixed IT8) [B8 x, B8 y]
290− = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
290+ = Just $ B8 (fromIntegral (fromIntegral x `quot` fromIntegral y :: Int8))
291291bsdiv (ITFixed IT16) [B16 x, B16 y]
292− = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
292+ = Just $ B16 (fromIntegral (fromIntegral x `quot` fromIntegral y :: Int16))
293293bsdiv (ITFixed IT32) [B32 x, B32 y]
294− = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
294+ = Just $ B32 (fromIntegral (fromIntegral x `quot` fromIntegral y :: Int32))
295295bsdiv (ITFixed IT64) [B64 x, B64 y]
296− = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
297−bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
298−bsdiv ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `div` (ord y))
296+ = Just $ B64 (fromIntegral (fromIntegral x `quot` fromIntegral y :: Int64))
297+bsdiv ITNative [I x, I y] = Just $ I (x `quot` y)
298+bsdiv ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `quot` (ord y))
299299bsdiv _ _ = Nothing
300300
301301bashr :: IntTy -> [Const] -> Maybe Const
test/TestData.hs+2−1
@@ -74,7 +74,8 @@ testFamiliesData = [
7474 ( 20, ANY ),
7575 ( 21, C_CG ),
7676 ( 22, NODE_CG ),
77− ( 23, ANY )]),
77+ ( 23, ANY ),
78+ ( 24, ANY )]),
7879 ("bignum", "Bignum",
7980 [ ( 1, ANY ),
8081 ( 2, ANY )]),
test/basic024/expectednew file+76
@@ -0,0 +1,76 @@
1+2 : Integer
2+2 : Int
3+2 : Bits8
4+2 : Bits16
5+2 : Bits32
6+2 : Bits64
7+2 : Nat
8+1 : Integer
9+1 : Int
10+1 : Bits8
11+1 : Bits16
12+1 : Bits32
13+1 : Bits64
14+1 : Nat
15+0 : Integer
16+0 : Int
17+0 : Bits8
18+0 : Bits16
19+0 : Bits32
20+0 : Bits64
21+0 : Nat
22+3 : Integer
23+3 : Int
24+3 : Bits8
25+3 : Bits16
26+3 : Bits32
27+3 : Bits64
28+3 : Nat
29+-2 : Integer
30+-2 : Int
31+-1 : Integer
32+-1 : Int
33+0 : Integer
34+0 : Int
35+-3 : Integer
36+-3 : Int
37+-11861903511836511836 : Integer
38+-25643355395 : Integer
39+2
40+2
41+02
42+0002
43+00000002
44+0000000000000002
45+2
46+1
47+1
48+01
49+0001
50+00000001
51+0000000000000001
52+1
53+0
54+0
55+00
56+0000
57+00000000
58+0000000000000000
59+0
60+3
61+3
62+03
63+0003
64+00000003
65+0000000000000003
66+3
67+-2
68+-2
69+-1
70+-1
71+0
72+0
73+-3
74+-3
75+-11861903511836511836
76+-25643355395
test/basic024/inputnew file+93
@@ -0,0 +1,93 @@
1+:x div (the Integer 5) 2
2+:x div (the Int 5) 2
3+:x div (the Bits8 5) 2
4+:x div (the Bits16 5) 2
5+:x div (the Bits32 5) 2
6+:x div (the Bits64 5) 2
7+:x div (the Nat 5) 2
8+
9+:x mod (the Integer 5) 2
10+:x mod (the Int 5) 2
11+:x mod (the Bits8 5) 2
12+:x mod (the Bits16 5) 2
13+:x mod (the Bits32 5) 2
14+:x mod (the Bits64 5) 2
15+:x mod (the Nat 5) 2
16+
17+:x div (the Integer 3) 5
18+:x div (the Int 3) 5
19+:x div (the Bits8 3) 5
20+:x div (the Bits16 3) 5
21+:x div (the Bits32 3) 5
22+:x div (the Bits64 3) 5
23+:x div (the Nat 3) 5
24+
25+:x mod (the Integer 3) 5
26+:x mod (the Int 3) 5
27+:x mod (the Bits8 3) 5
28+:x mod (the Bits16 3) 5
29+:x mod (the Bits32 3) 5
30+:x mod (the Bits64 3) 5
31+:x mod (the Nat 3) 5
32+
33+:x div (the Integer (-5)) 2
34+:x div (the Int (-5)) 2
35+
36+:x mod (the Integer (-5)) 2
37+:x mod (the Int (-5)) 2
38+
39+:x div (the Integer (-3)) 5
40+:x div (the Int (-3)) 5
41+
42+:x mod (the Integer (-3)) 5
43+:x mod (the Int (-3)) 5
44+
45+:x div (-432642342742368327462378462387) 36473264372
46+:x mod (-432642342742368327462378462387) 36473264372
47+
48+:exec div (the Integer 5) 2
49+:exec div (the Int 5) 2
50+:exec div (the Bits8 5) 2
51+:exec div (the Bits16 5) 2
52+:exec div (the Bits32 5) 2
53+:exec div (the Bits64 5) 2
54+:exec div (the Nat 5) 2
55+
56+:exec mod (the Integer 5) 2
57+:exec mod (the Int 5) 2
58+:exec mod (the Bits8 5) 2
59+:exec mod (the Bits16 5) 2
60+:exec mod (the Bits32 5) 2
61+:exec mod (the Bits64 5) 2
62+:exec mod (the Nat 5) 2
63+
64+:exec div (the Integer 3) 5
65+:exec div (the Int 3) 5
66+:exec div (the Bits8 3) 5
67+:exec div (the Bits16 3) 5
68+:exec div (the Bits32 3) 5
69+:exec div (the Bits64 3) 5
70+:exec div (the Nat 3) 5
71+
72+:exec mod (the Integer 3) 5
73+:exec mod (the Int 3) 5
74+:exec mod (the Bits8 3) 5
75+:exec mod (the Bits16 3) 5
76+:exec mod (the Bits32 3) 5
77+:exec mod (the Bits64 3) 5
78+:exec mod (the Nat 3) 5
79+
80+:exec div (the Integer (-5)) 2
81+:exec div (the Int (-5)) 2
82+
83+:exec mod (the Integer (-5)) 2
84+:exec mod (the Int (-5)) 2
85+
86+:exec div (the Integer (-3)) 5
87+:exec div (the Int (-3)) 5
88+
89+:exec mod (the Integer (-3)) 5
90+:exec mod (the Int (-3)) 5
91+
92+:exec div (-432642342742368327462378462387) 36473264372
93+:exec mod (-432642342742368327462378462387) 36473264372
test/basic024/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+
3+${IDRIS:-idris} $@ --quiet --port none < input
4+
5+rm -f *.ibc