on master help sign in
Make Data.Hash total
e76e6d4Sebastian de Bellefon
libs/base/Data/Hash.idr+6−3
@@ -1,7 +1,7 @@
1module Data.Hash
1module Data.Hash
2
2
3%access public
3%access public
4−%default partial
4+%default total
5
5
6||| A type that can be hashed
6||| A type that can be hashed
7class Hashable a where
7class Hashable a where
@@ -23,6 +23,11 @@ byte n w = prim__lshrB64 (prim__andB64 mask w) offset
23 where offset = 8*n
23 where offset = 8*n
24 mask = prim__shlB64 0xff (the Bits64 offset)
24 mask = prim__shlB64 0xff (the Bits64 offset)
25
25
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+
26instance Hashable Bits64 where
31instance Hashable Bits64 where
27 saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
32 saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
28 salt
33 salt
@@ -30,8 +35,6 @@ instance Hashable Bits64 where
30
35
31instance Hashable Integer where
36instance Hashable Integer where
32 saltedHash64 i = saltedHash64 (mod64 i)
37 saltedHash64 i = saltedHash64 (mod64 i)
33− where mod64 : Integer -> Bits64
34− mod64 i = fromInteger (abs i `mod` 0xffffffffffffffff)
35
38
36instance Hashable () where
39instance Hashable () where
37 saltedHash64 _ salt = salt
40 saltedHash64 _ salt = salt