on master help sign in
Make Data.Hash total
commite76e6d455d3448d18fc453529c12cf15f503a4dc authorSebastian de Bellefon <arnaudpourseb@gmail.com> dateSat 4 Oct 2014, 16:13 (12 years ago) parent8695823
1 file changed+6−3
libs/base/Data/Hash.idr+6−3
libs/base/Data/Hash.idr+6−3
@@ -1,7 +1,7 @@
11module Data.Hash
22
33%access public
4−%default partial
4+%default total
55
66||| A type that can be hashed
77class Hashable a where
@@ -23,6 +23,11 @@ byte n w = prim__lshrB64 (prim__andB64 mask w) offset
2323 where offset = 8*n
2424 mask = prim__shlB64 0xff (the Bits64 offset)
2525
26+||| Modulo of an integer, downsized to a Bits64
27+private
28+mod64 : Integer -> Bits64
29+mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
30+
2631instance Hashable Bits64 where
2732 saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
2833 salt
@@ -30,8 +35,6 @@ instance Hashable Bits64 where
3035
3136instance Hashable Integer where
3237 saltedHash64 i = saltedHash64 (mod64 i)
33− where mod64 : Integer -> Bits64
34− mod64 i = fromInteger (abs i `mod` 0xffffffffffffffff)
3538
3639instance Hashable () where
3740 saltedHash64 _ salt = salt