git.iko.soy/Idris-dev
on master help sign in
Make `div` and `mod` functions partial.
commit465cc1c0c1de75cefd65dc4dec1d382a82e9f370 authorAndrew Cann <shum@canndrew.org> dateMon 23 Mar 2015, 17:55 (12 years ago) parentcea7870
5 files changed+42−29
compare with master
unifiedsplit
libs/base/Data/Bits.idr+3 libs/contrib/Data/Hash.idr+7−3 libs/prelude/Prelude.idr+2−3 libs/prelude/Prelude/Classes.idr+24−12 libs/prelude/Prelude/Nat.idr+6−11
libs/base/Data/Bits.idr+3
@@ -4,11 +4,13 @@ import Data.Fin
44
55%default total
66
7+partial
78divCeil : Nat -> Nat -> Nat
89divCeil x y = case x `mod` y of
910 Z => x `div` y
1011 S _ => S (x `div` y)
1112
13+%assert_total
1214nextPow2 : Nat -> Nat
1315nextPow2 Z = Z
1416nextPow2 x = if x == (2 `power` l2x)
@@ -17,6 +19,7 @@ nextPow2 x = if x == (2 `power` l2x)
1719 where
1820 l2x = log2 x
1921
22+%assert_total
2023nextBytes : Nat -> Nat
2124nextBytes bits = (nextPow2 (bits `divCeil` 8))
2225
libs/contrib/Data/Hash.idr+7−3
@@ -40,10 +40,14 @@ private
4040mod64 : Integer -> Bits64
4141mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
4242
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+
4349instance Hashable Bits64 where
44− saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
45− salt
46− [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto
50+ saltedHash64 = saltedHash64Bits64
4751
4852instance Hashable Integer where
4953 saltedHash64 i = saltedHash64 (mod64 i)
libs/prelude/Prelude.idr+2−3
@@ -335,8 +335,7 @@ total natEnumFromThen : Nat -> Nat -> Stream Nat
335335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
336336total natEnumFromTo : Nat -> Nat -> List Nat
337337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
338−total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
339−natEnumFromThenTo _ Z _ = []
338+partial natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
340339natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
341340
342341class Enum a where
@@ -351,7 +350,7 @@ class Enum a where
351350 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
352351 total enumFromTo : a -> a -> List a
353352 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
355354 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
356355
357356instance Enum Nat where
libs/prelude/Prelude/Classes.idr+24−12
@@ -315,10 +315,12 @@ class Integral a where
315315
316316-- ---------------------------------------------------------------- [ Integers ]
317317divBigInt : Integer -> Integer -> Integer
318−divBigInt = prim__sdivBigInt
318+divBigInt x y = case y == 0 of
319+ False => prim__sdivBigInt x y
319320
320321modBigInt : Integer -> Integer -> Integer
321−modBigInt = prim__sremBigInt
322+modBigInt x y = case y == 0 of
323+ False => prim__sremBigInt x y
322324
323325instance Integral Integer where
324326 div = divBigInt
@@ -327,10 +329,12 @@ instance Integral Integer where
327329-- --------------------------------------------------------------------- [ Int ]
328330
329331divInt : Int -> Int -> Int
330−divInt = prim__sdivInt
332+divInt x y = case y == 0 of
333+ False => prim__sdivInt x y
331334
332335modInt : Int -> Int -> Int
333−modInt = prim__sremInt
336+modInt x y = case y == 0 of
337+ False => prim__sremInt x y
334338
335339instance Integral Int where
336340 div = divInt
@@ -338,10 +342,12 @@ instance Integral Int where
338342
339343-- ------------------------------------------------------------------- [ Bits8 ]
340344divB8 : Bits8 -> Bits8 -> Bits8
341−divB8 = prim__sdivB8
345+divB8 x y = case y == 0 of
346+ False => prim__sdivB8 x y
342347
343348modB8 : Bits8 -> Bits8 -> Bits8
344−modB8 = prim__sremB8
349+modB8 x y = case y == 0 of
350+ False => prim__sremB8 x y
345351
346352instance Integral Bits8 where
347353 div = divB8
@@ -349,10 +355,12 @@ instance Integral Bits8 where
349355
350356-- ------------------------------------------------------------------ [ Bits16 ]
351357divB16 : Bits16 -> Bits16 -> Bits16
352−divB16 = prim__sdivB16
358+divB16 x y = case y == 0 of
359+ False => prim__sdivB16 x y
353360
354361modB16 : Bits16 -> Bits16 -> Bits16
355−modB16 = prim__sremB16
362+modB16 x y = case y == 0 of
363+ False => prim__sremB16 x y
356364
357365instance Integral Bits16 where
358366 div = divB16
@@ -360,10 +368,12 @@ instance Integral Bits16 where
360368
361369-- ------------------------------------------------------------------ [ Bits32 ]
362370divB32 : Bits32 -> Bits32 -> Bits32
363−divB32 = prim__sdivB32
371+divB32 x y = case y == 0 of
372+ False => prim__sdivB32 x y
364373
365374modB32 : Bits32 -> Bits32 -> Bits32
366−modB32 = prim__sremB32
375+modB32 x y = case y == 0 of
376+ False => prim__sremB32 x y
367377
368378instance Integral Bits32 where
369379 div = divB32
@@ -371,10 +381,12 @@ instance Integral Bits32 where
371381
372382-- ------------------------------------------------------------------ [ Bits64 ]
373383divB64 : Bits64 -> Bits64 -> Bits64
374−divB64 = prim__sdivB64
384+divB64 x y = case y == 0 of
385+ False => prim__sdivB64 x y
375386
376387modB64 : Bits64 -> Bits64 -> Bits64
377−modB64 = prim__sremB64
388+modB64 x y = case y == 0 of
389+ False => prim__sremB64 x y
378390
379391instance Integral Bits64 where
380392 div = divB64
libs/prelude/Prelude/Nat.idr+6−11
@@ -274,9 +274,8 @@ fact (S n) = (S n) * fact n
274274-- Division and modulus
275275--------------------------------------------------------------------------------
276276
277−total
277+partial
278278modNat : Nat -> Nat -> Nat
279−modNat left Z = left
280279modNat left (S right) = mod' left left right
281280 where
282281 total mod' : Nat -> Nat -> Nat -> Nat
@@ -287,9 +286,8 @@ modNat left (S right) = mod' left left right
287286 else
288287 mod' left (centre - (S right)) right
289288
290−total
289+partial
291290divNat : Nat -> Nat -> Nat
292−divNat left Z = S left -- div by zero
293291divNat left (S right) = div' left left right
294292 where
295293 total div' : Nat -> Nat -> Nat -> Nat
@@ -304,19 +302,21 @@ instance Integral Nat where
304302 div = divNat
305303 mod = modNat
306304
305+partial
307306log2 : Nat -> Nat
308−log2 Z = Z
309307log2 (S Z) = Z
310308log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
311309
312310--------------------------------------------------------------------------------
313311-- GCD and LCM
314312--------------------------------------------------------------------------------
313+partial
315314gcd : Nat -> Nat -> Nat
316315gcd a Z = a
317316gcd a b = assert_total (gcd b (a `modNat` b))
318317
319−total lcm : Nat -> Nat -> Nat
318+partial
319+lcm : Nat -> Nat -> Nat
320320lcm _ Z = Z
321321lcm Z _ = Z
322322lcm x y = divNat (x * y) (gcd x y)
@@ -710,11 +710,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
710710sucMinR Z = Refl
711711sucMinR (S l) = cong (sucMinR l)
712712
713−-- div and mod
714−total modZeroZero : (n : Nat) -> mod 0 n = Z
715−modZeroZero Z = Refl
716−modZeroZero (S n) = Refl
717−
718713--------------------------------------------------------------------------------
719714-- Proofs
720715--------------------------------------------------------------------------------