git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into fix-div-and-mod
b85425eAlex Queiroz
idris.cabal+1−1
compare with master
unifiedsplit
@@ -314,7 +314,7 @@ Library
314
314
315 if os(windows)
315 if os(windows)
316 build-depends: mintty >= 0.1 && < 0.2
316 build-depends: mintty >= 0.1 && < 0.2
317− , Win32 < 2.4
317+ , Win32 < 2.7
318 else
318 else
319 build-depends: unix < 2.8
319 build-depends: unix < 2.8
320 if flag(FFI)
320 if flag(FFI)
libs/base/Data/Primitives/Views.idr+19−15
@@ -12,9 +12,9 @@ namespace Integer
12 DivByZero : Divides x 0
12 DivByZero : Divides x 0
13 DivBy : (prf : rem >= 0 && rem < d = True) ->
13 DivBy : (prf : rem >= 0 && rem < d = True) ->
14 Divides ((d * div) + rem) d
14 Divides ((d * div) + rem) d
15−
15+
16 ||| Covering function for the `Divides` view
16 ||| Covering function for the `Divides` view
17− export
17+ public export
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
19 divides val 0 = DivByZero
19 divides val 0 = DivByZero
20 divides val d
20 divides val d
@@ -22,21 +22,23 @@ namespace Integer
22 let dividend = if d < 0 then -(val `div` abs d)
22 let dividend = if d < 0 then -(val `div` abs d)
23 else val `div` d
23 else val `div` d
24 remainder = abs (val - dividend * d) in
24 remainder = abs (val - dividend * d) in
25− believe_me (DivBy {d} {div = dividend} {rem = remainder}
25+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
26− (believe_me (Refl {x = True})))
26+ (really_believe_me (Refl {x = True})))
27
27
28 ||| View for recursion over Integers
28 ||| View for recursion over Integers
29+ public export
29 data IntegerRec : Integer -> Type where
30 data IntegerRec : Integer -> Type where
30 IntegerZ : IntegerRec 0
31 IntegerZ : IntegerRec 0
31 IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
32 IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
32 IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
33 IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
33−
34+
34 ||| Covering function for `IntegerRec`
35 ||| Covering function for `IntegerRec`
36+ public export
35 integerRec : (x : Integer) -> IntegerRec x
37 integerRec : (x : Integer) -> IntegerRec x
36 integerRec 0 = IntegerZ
38 integerRec 0 = IntegerZ
37 integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
39 integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
38− else believe_me (IntegerPred {n=-x}
40+ else really_believe_me (IntegerPred {n=-x}
39− (assert_total (believe_me (integerRec (x + 1)))))
41+ (assert_total (really_believe_me (integerRec (x + 1)))))
40
42
41namespace Int
43namespace Int
42 ||| View for expressing a number as a multiplication + a remainder
44 ||| View for expressing a number as a multiplication + a remainder
@@ -45,13 +47,13 @@ namespace Int
45 DivByZero : Int.Divides x 0
47 DivByZero : Int.Divides x 0
46 DivBy : (prf : rem >= 0 && rem < d = True) ->
48 DivBy : (prf : rem >= 0 && rem < d = True) ->
47 Int.Divides ((d * div) + rem) d
49 Int.Divides ((d * div) + rem) d
48−
50+
49 -- I have assumed, but not actually verified, that this will still
51 -- I have assumed, but not actually verified, that this will still
50 -- give a right result (i.e. still adding up) when the Ints overflow.
52 -- give a right result (i.e. still adding up) when the Ints overflow.
51 -- TODO: Someone please check this and fix if necessary...
53 -- TODO: Someone please check this and fix if necessary...
52
54
53 ||| Covering function for the `Divides` view
55 ||| Covering function for the `Divides` view
54− export
56+ public export
55 divides : (val : Int) -> (d : Int) -> Divides val d
57 divides : (val : Int) -> (d : Int) -> Divides val d
56 divides val 0 = DivByZero
58 divides val 0 = DivByZero
57 divides val d
59 divides val d
@@ -59,19 +61,21 @@ namespace Int
59 let dividend = if d < 0 then -(val `div` abs d)
61 let dividend = if d < 0 then -(val `div` abs d)
60 else val `div` d
62 else val `div` d
61 remainder = abs (val - dividend * d) in
63 remainder = abs (val - dividend * d) in
62− believe_me (DivBy {d} {div = dividend} {rem = remainder}
64+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
63− (believe_me (Refl {x = True})))
65+ (really_believe_me (Refl {x = True})))
64
66
65 ||| View for recursion over Ints
67 ||| View for recursion over Ints
68+ public export
66 data IntRec : Int -> Type where
69 data IntRec : Int -> Type where
67 IntZ : IntRec 0
70 IntZ : IntRec 0
68 IntSucc : IntRec (n - 1) -> IntRec n
71 IntSucc : IntRec (n - 1) -> IntRec n
69 IntPred : IntRec ((-n) + 1) -> IntRec (-n)
72 IntPred : IntRec ((-n) + 1) -> IntRec (-n)
70−
73+
71 ||| Covering function for `IntRec`
74 ||| Covering function for `IntRec`
75+ public export
72 intRec : (x : Int) -> IntRec x
76 intRec : (x : Int) -> IntRec x
73 intRec 0 = IntZ
77 intRec 0 = IntZ
74 intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
78 intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
75− else believe_me (IntPred {n=-x}
79+ else really_believe_me (IntPred {n=-x}
76− (assert_total (believe_me (intRec (x + 1)))))
80+ (assert_total (really_believe_me (intRec (x + 1)))))
77−
81+
src/IRTS/CodegenC.hs+1−1
@@ -179,7 +179,7 @@ bcc i (ASSIGNCONST l c)
179 = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
179 = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
180 where
180 where
181 mkConst (I i) = "MKINT(" ++ show i ++ ")"
181 mkConst (I i) = "MKINT(" ++ show i ++ ")"
182− mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
182+ mkConst (BI i) | i > ((-2)^30) && i < (2^30) = "MKINT(" ++ show i ++ ")"
183 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"
183 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"
184 mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"
184 mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"
185 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
185 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
test/bignum002/bignum002.idr+1
@@ -3,3 +3,4 @@ module Main
3main : IO ()
3main : IO ()
4main = do
4main = do
5 putStrLn $ show $ divNat 1809022195644390369852458 91238741987
5 putStrLn $ show $ divNat 1809022195644390369852458 91238741987
6+ putStrLn $ show $ div (-432642342742368327462378462387) 36473264372
test/bignum002/expected+1
@@ -1 +1,2 @@
119827346982734
119827346982734
2+-11861903511836511836