git.iko.soy/Idris-dev
on master help sign in
Make `div` and `mod` functions partial.
465cc1cAndrew Cann
libs/base/Data/Bits.idr+3
compare with master
unifiedsplit
@@ -4,11 +4,13 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
7+partial
7divCeil : Nat -> Nat -> Nat
8divCeil : Nat -> Nat -> Nat
8divCeil x y = case x `mod` y of
9divCeil x y = case x `mod` y of
9 Z => x `div` y
10 Z => x `div` y
10 S _ => S (x `div` y)
11 S _ => S (x `div` y)
11
12
13+%assert_total
12nextPow2 : Nat -> Nat
14nextPow2 : Nat -> Nat
13nextPow2 Z = Z
15nextPow2 Z = Z
14nextPow2 x = if x == (2 `power` l2x)
16nextPow2 x = if x == (2 `power` l2x)
@@ -17,6 +19,7 @@ nextPow2 x = if x == (2 `power` l2x)
17 where
19 where
18 l2x = log2 x
20 l2x = log2 x
19
21
22+%assert_total
20nextBytes : Nat -> Nat
23nextBytes : Nat -> Nat
21nextBytes bits = (nextPow2 (bits `divCeil` 8))
24nextBytes bits = (nextPow2 (bits `divCeil` 8))
22
25
libs/contrib/Data/Hash.idr+7−3
@@ -40,10 +40,14 @@ private
40mod64 : Integer -> Bits64
40mod64 : Integer -> Bits64
41mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
41mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
42
42
43+%assert_total
44+saltedHash64Bits64 : Bits64 -> Bits64 -> Bits64
45+saltedHash64Bits64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
46+ salt
47+ [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto
48+
43instance Hashable Bits64 where
49instance Hashable Bits64 where
44− saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
50+ saltedHash64 = saltedHash64Bits64
45− salt
46− [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto
47
51
48instance Hashable Integer where
52instance Hashable Integer where
49 saltedHash64 i = saltedHash64 (mod64 i)
53 saltedHash64 i = saltedHash64 (mod64 i)
libs/prelude/Prelude.idr+2−3
@@ -335,8 +335,7 @@ total natEnumFromThen : Nat -> Nat -> Stream Nat
335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
336total natEnumFromTo : Nat -> Nat -> List Nat
336total natEnumFromTo : Nat -> Nat -> List Nat
337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
338−total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
338+partial natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
339−natEnumFromThenTo _ Z _ = []
340natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
339natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
341
340
342class Enum a where
341class Enum a where
@@ -351,7 +350,7 @@ class Enum a where
351 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
350 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
352 total enumFromTo : a -> a -> List a
351 total enumFromTo : a -> a -> List a
353 enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
352 enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
354− total enumFromThenTo : a -> a -> a -> List a
353+ partial enumFromThenTo : a -> a -> a -> List a
355 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
354 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
356
355
357instance Enum Nat where
356instance Enum Nat where
libs/prelude/Prelude/Classes.idr+24−12
@@ -315,10 +315,12 @@ class Integral a where
315
315
316-- ---------------------------------------------------------------- [ Integers ]
316-- ---------------------------------------------------------------- [ Integers ]
317divBigInt : Integer -> Integer -> Integer
317divBigInt : Integer -> Integer -> Integer
318+divBigInt x y = case y == 0 of
318−divBigInt = prim__sdivBigInt
319+ False => prim__sdivBigInt x y
319
320
320modBigInt : Integer -> Integer -> Integer
321modBigInt : Integer -> Integer -> Integer
322+modBigInt x y = case y == 0 of
321−modBigInt = prim__sremBigInt
323+ False => prim__sremBigInt x y
322
324
323instance Integral Integer where
325instance Integral Integer where
324 div = divBigInt
326 div = divBigInt
@@ -327,10 +329,12 @@ instance Integral Integer where
327-- --------------------------------------------------------------------- [ Int ]
329-- --------------------------------------------------------------------- [ Int ]
328
330
329divInt : Int -> Int -> Int
331divInt : Int -> Int -> Int
332+divInt x y = case y == 0 of
330−divInt = prim__sdivInt
333+ False => prim__sdivInt x y
331
334
332modInt : Int -> Int -> Int
335modInt : Int -> Int -> Int
336+modInt x y = case y == 0 of
333−modInt = prim__sremInt
337+ False => prim__sremInt x y
334
338
335instance Integral Int where
339instance Integral Int where
336 div = divInt
340 div = divInt
@@ -338,10 +342,12 @@ instance Integral Int where
338
342
339-- ------------------------------------------------------------------- [ Bits8 ]
343-- ------------------------------------------------------------------- [ Bits8 ]
340divB8 : Bits8 -> Bits8 -> Bits8
344divB8 : Bits8 -> Bits8 -> Bits8
345+divB8 x y = case y == 0 of
341−divB8 = prim__sdivB8
346+ False => prim__sdivB8 x y
342
347
343modB8 : Bits8 -> Bits8 -> Bits8
348modB8 : Bits8 -> Bits8 -> Bits8
349+modB8 x y = case y == 0 of
344−modB8 = prim__sremB8
350+ False => prim__sremB8 x y
345
351
346instance Integral Bits8 where
352instance Integral Bits8 where
347 div = divB8
353 div = divB8
@@ -349,10 +355,12 @@ instance Integral Bits8 where
349
355
350-- ------------------------------------------------------------------ [ Bits16 ]
356-- ------------------------------------------------------------------ [ Bits16 ]
351divB16 : Bits16 -> Bits16 -> Bits16
357divB16 : Bits16 -> Bits16 -> Bits16
358+divB16 x y = case y == 0 of
352−divB16 = prim__sdivB16
359+ False => prim__sdivB16 x y
353
360
354modB16 : Bits16 -> Bits16 -> Bits16
361modB16 : Bits16 -> Bits16 -> Bits16
362+modB16 x y = case y == 0 of
355−modB16 = prim__sremB16
363+ False => prim__sremB16 x y
356
364
357instance Integral Bits16 where
365instance Integral Bits16 where
358 div = divB16
366 div = divB16
@@ -360,10 +368,12 @@ instance Integral Bits16 where
360
368
361-- ------------------------------------------------------------------ [ Bits32 ]
369-- ------------------------------------------------------------------ [ Bits32 ]
362divB32 : Bits32 -> Bits32 -> Bits32
370divB32 : Bits32 -> Bits32 -> Bits32
371+divB32 x y = case y == 0 of
363−divB32 = prim__sdivB32
372+ False => prim__sdivB32 x y
364
373
365modB32 : Bits32 -> Bits32 -> Bits32
374modB32 : Bits32 -> Bits32 -> Bits32
375+modB32 x y = case y == 0 of
366−modB32 = prim__sremB32
376+ False => prim__sremB32 x y
367
377
368instance Integral Bits32 where
378instance Integral Bits32 where
369 div = divB32
379 div = divB32
@@ -371,10 +381,12 @@ instance Integral Bits32 where
371
381
372-- ------------------------------------------------------------------ [ Bits64 ]
382-- ------------------------------------------------------------------ [ Bits64 ]
373divB64 : Bits64 -> Bits64 -> Bits64
383divB64 : Bits64 -> Bits64 -> Bits64
384+divB64 x y = case y == 0 of
374−divB64 = prim__sdivB64
385+ False => prim__sdivB64 x y
375
386
376modB64 : Bits64 -> Bits64 -> Bits64
387modB64 : Bits64 -> Bits64 -> Bits64
388+modB64 x y = case y == 0 of
377−modB64 = prim__sremB64
389+ False => prim__sremB64 x y
378
390
379instance Integral Bits64 where
391instance Integral Bits64 where
380 div = divB64
392 div = divB64
libs/prelude/Prelude/Nat.idr+6−11
@@ -274,9 +274,8 @@ fact (S n) = (S n) * fact n
274-- Division and modulus
274-- Division and modulus
275--------------------------------------------------------------------------------
275--------------------------------------------------------------------------------
276
276
277−total
277+partial
278modNat : Nat -> Nat -> Nat
278modNat : Nat -> Nat -> Nat
279−modNat left Z = left
280modNat left (S right) = mod' left left right
279modNat left (S right) = mod' left left right
281 where
280 where
282 total mod' : Nat -> Nat -> Nat -> Nat
281 total mod' : Nat -> Nat -> Nat -> Nat
@@ -287,9 +286,8 @@ modNat left (S right) = mod' left left right
287 else
286 else
288 mod' left (centre - (S right)) right
287 mod' left (centre - (S right)) right
289
288
290−total
289+partial
291divNat : Nat -> Nat -> Nat
290divNat : Nat -> Nat -> Nat
292−divNat left Z = S left -- div by zero
293divNat left (S right) = div' left left right
291divNat left (S right) = div' left left right
294 where
292 where
295 total div' : Nat -> Nat -> Nat -> Nat
293 total div' : Nat -> Nat -> Nat -> Nat
@@ -304,19 +302,21 @@ instance Integral Nat where
304 div = divNat
302 div = divNat
305 mod = modNat
303 mod = modNat
306
304
305+partial
307log2 : Nat -> Nat
306log2 : Nat -> Nat
308−log2 Z = Z
309log2 (S Z) = Z
307log2 (S Z) = Z
310log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
308log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
311
309
312--------------------------------------------------------------------------------
310--------------------------------------------------------------------------------
313-- GCD and LCM
311-- GCD and LCM
314--------------------------------------------------------------------------------
312--------------------------------------------------------------------------------
313+partial
315gcd : Nat -> Nat -> Nat
314gcd : Nat -> Nat -> Nat
316gcd a Z = a
315gcd a Z = a
317gcd a b = assert_total (gcd b (a `modNat` b))
316gcd a b = assert_total (gcd b (a `modNat` b))
318
317
318+partial
319−total lcm : Nat -> Nat -> Nat
319+lcm : Nat -> Nat -> Nat
320lcm _ Z = Z
320lcm _ Z = Z
321lcm Z _ = Z
321lcm Z _ = Z
322lcm x y = divNat (x * y) (gcd x y)
322lcm x y = divNat (x * y) (gcd x y)
@@ -710,11 +710,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
710sucMinR Z = Refl
710sucMinR Z = Refl
711sucMinR (S l) = cong (sucMinR l)
711sucMinR (S l) = cong (sucMinR l)
712
712
713−-- div and mod
714−total modZeroZero : (n : Nat) -> mod 0 n = Z
715−modZeroZero Z = Refl
716−modZeroZero (S n) = Refl
717−
718--------------------------------------------------------------------------------
713--------------------------------------------------------------------------------
719-- Proofs
714-- Proofs
720--------------------------------------------------------------------------------
715--------------------------------------------------------------------------------