on master help sign in
since BitsN is unsigned through the definition, unsigned operations like prim__udivB8 and
7186adezjhmale
CHANGELOG.md+1
@@ -26,6 +26,7 @@
26* The File Effect has been updated to take into account changes in
26* The File Effect has been updated to take into account changes in
27 `Prelude.File` and to provide a 'better' API.
27 `Prelude.File` and to provide a 'better' API.
28* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.
28* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.
29+* `divBN` and `modBN` now can only be used for unsigned numbers.
29
30
30## Tool updates
31## Tool updates
31
32
libs/prelude/Prelude/Interfaces.idr+8−8
@@ -354,11 +354,11 @@ Integral Int where
354-- ------------------------------------------------------------------- [ Bits8 ]
354-- ------------------------------------------------------------------- [ Bits8 ]
355divB8 : Bits8 -> Bits8 -> Bits8
355divB8 : Bits8 -> Bits8 -> Bits8
356divB8 x y = case y == 0 of
356divB8 x y = case y == 0 of
357− False => prim__sdivB8 x y
357+ False => prim__udivB8 x y
358
358
359modB8 : Bits8 -> Bits8 -> Bits8
359modB8 : Bits8 -> Bits8 -> Bits8
360modB8 x y = case y == 0 of
360modB8 x y = case y == 0 of
361− False => prim__sremB8 x y
361+ False => prim__uremB8 x y
362
362
363Integral Bits8 where
363Integral Bits8 where
364 div = divB8
364 div = divB8
@@ -367,11 +367,11 @@ Integral Bits8 where
367-- ------------------------------------------------------------------ [ Bits16 ]
367-- ------------------------------------------------------------------ [ Bits16 ]
368divB16 : Bits16 -> Bits16 -> Bits16
368divB16 : Bits16 -> Bits16 -> Bits16
369divB16 x y = case y == 0 of
369divB16 x y = case y == 0 of
370− False => prim__sdivB16 x y
370+ False => prim__udivB16 x y
371
371
372modB16 : Bits16 -> Bits16 -> Bits16
372modB16 : Bits16 -> Bits16 -> Bits16
373modB16 x y = case y == 0 of
373modB16 x y = case y == 0 of
374− False => prim__sremB16 x y
374+ False => prim__uremB16 x y
375
375
376Integral Bits16 where
376Integral Bits16 where
377 div = divB16
377 div = divB16
@@ -380,11 +380,11 @@ Integral Bits16 where
380-- ------------------------------------------------------------------ [ Bits32 ]
380-- ------------------------------------------------------------------ [ Bits32 ]
381divB32 : Bits32 -> Bits32 -> Bits32
381divB32 : Bits32 -> Bits32 -> Bits32
382divB32 x y = case y == 0 of
382divB32 x y = case y == 0 of
383− False => prim__sdivB32 x y
383+ False => prim__udivB32 x y
384
384
385modB32 : Bits32 -> Bits32 -> Bits32
385modB32 : Bits32 -> Bits32 -> Bits32
386modB32 x y = case y == 0 of
386modB32 x y = case y == 0 of
387− False => prim__sremB32 x y
387+ False => prim__uremB32 x y
388
388
389Integral Bits32 where
389Integral Bits32 where
390 div = divB32
390 div = divB32
@@ -393,11 +393,11 @@ Integral Bits32 where
393-- ------------------------------------------------------------------ [ Bits64 ]
393-- ------------------------------------------------------------------ [ Bits64 ]
394divB64 : Bits64 -> Bits64 -> Bits64
394divB64 : Bits64 -> Bits64 -> Bits64
395divB64 x y = case y == 0 of
395divB64 x y = case y == 0 of
396− False => prim__sdivB64 x y
396+ False => prim__udivB64 x y
397
397
398modB64 : Bits64 -> Bits64 -> Bits64
398modB64 : Bits64 -> Bits64 -> Bits64
399modB64 x y = case y == 0 of
399modB64 x y = case y == 0 of
400− False => prim__sremB64 x y
400+ False => prim__uremB64 x y
401
401
402Integral Bits64 where
402Integral Bits64 where
403 div = divB64
403 div = divB64
test/basic011/basic011.idr+4
@@ -13,4 +13,8 @@ main = do printLn $ hash (the Bits8 3)
13 printLn $ hash (the Bits64 3)
13 printLn $ hash (the Bits64 3)
14 printLn $ hash (the Int 3)
14 printLn $ hash (the Int 3)
15 printLn $ hash (the Integer 3)
15 printLn $ hash (the Integer 3)
16+ printLn $ divB8 10 255
17+ printLn $ divB16 10 65535
18+ printLn $ divB32 10 4294967295
19+ printLn $ divB64 10 18446744073709551615
16
20
test/basic011/expected+4
@@ -8,3 +8,7 @@ AD85270E93646134
86EA049D797FA18D6
86EA049D797FA18D6
96EA049D797FA18D6
96EA049D797FA18D6
106EA049D797FA18D6
106EA049D797FA18D6
11+00
12+0000
13+00000000
14+0000000000000000