0 | module Data.Hashable
  1 |
  2 | import Data.Vect
  3 |
  4 | ||| A default salt used in the implementation of 'hash'.
  5 | export
  6 | defaultSalt : Bits64
  7 | defaultSalt = 14695981039346656037
  8 |
  9 | export infixl 10 `hashWithSalt`
 10 | export infixl 10 `hash`
 11 |
 12 | ||| Interface for type that can be hashed.
 13 | ||| Minimal implementation: 'hashWithSalt'
 14 | public export
 15 | interface Hashable a where
 16 |     ||| Hash a value with the given salt
 17 |     total
 18 |     hashWithSalt : Bits64 -> a -> Bits64
 19 |     ||| Hash a value with the default salt
 20 |     total
 21 |     hash : a -> Bits64
 22 |     hash = hashWithSalt defaultSalt
 23 |
 24 | ||| Combine 2 hashes.
 25 | export
 26 | combine : Bits64 -> Bits64 -> Bits64
 27 | combine h1 h2 = (h1 * 16777619) `prim__xor_Bits64` h2
 28 |
 29 | ||| Default implementation of 'hashWithSalt' for types which are smaller than Bits64 (eg Bits32, Int).
 30 | export
 31 | defaultHashWithSalt : (a -> Bits64) -> Bits64 -> a -> Bits64
 32 | defaultHashWithSalt hash salt x = salt `combine` hash x
 33 |
 34 | export
 35 | Hashable Bits8 where
 36 |     hash = cast
 37 |     hashWithSalt = defaultHashWithSalt hash
 38 |
 39 | export
 40 | Hashable Bits16 where
 41 |     hash = cast
 42 |     hashWithSalt = defaultHashWithSalt hash
 43 |
 44 | export
 45 | Hashable Bits32 where
 46 |     hash = cast
 47 |     hashWithSalt = defaultHashWithSalt hash
 48 |
 49 | export
 50 | Hashable Bits64 where
 51 |     hash = id
 52 |     hashWithSalt = defaultHashWithSalt hash
 53 |
 54 | export
 55 | Hashable Int where
 56 |     hash = cast
 57 |     hashWithSalt = defaultHashWithSalt hash
 58 |
 59 | export
 60 | Hashable Int8 where
 61 |     hash = cast
 62 |     hashWithSalt = defaultHashWithSalt hash
 63 |
 64 | export
 65 | Hashable Int16 where
 66 |     hash = cast
 67 |     hashWithSalt = defaultHashWithSalt hash
 68 |
 69 | export
 70 | Hashable Int32 where
 71 |     hash = cast
 72 |     hashWithSalt = defaultHashWithSalt hash
 73 |
 74 | export
 75 | Hashable Int64 where
 76 |     hash = cast
 77 |     hashWithSalt = defaultHashWithSalt hash
 78 |
 79 | export
 80 | Hashable Char where
 81 |     hash = cast . ord
 82 |     hashWithSalt = defaultHashWithSalt hash
 83 |
 84 | export
 85 | Hashable Integer where
 86 |     hashWithSalt salt x = hashPositive (makeSalt salt x) (abs x)
 87 |       where
 88 |         makeSalt : Bits64 -> Integer -> Bits64
 89 |         makeSalt x y = if y >= 0
 90 |             then x
 91 |             else negate x
 92 |
 93 |         bits64Max : Integer
 94 |         bits64Max = 1 `prim__shl_Integer` 64 - 1
 95 |
 96 |         hashPositive : Bits64 -> Integer -> Bits64
 97 |         hashPositive salt x = if x > bits64Max
 98 |             then hashPositive
 99 |                 (hashWithSalt salt
100 |                     (cast {to=Bits64} (x `prim__and_Integer` bits64Max)))
101 |                 (assert_smaller x $ x `prim__shr_Integer` 64)
102 |             else hashWithSalt salt (cast {to=Bits64} x)
103 |
104 | export
105 | Hashable Nat where
106 |     hash x = hash (cast {to=Integer} x)
107 |     hashWithSalt salt x = hashWithSalt salt (cast {to=Integer} x)
108 |
109 | export
110 | Hashable String where
111 |     hashWithSalt salt str = finalise (foldl step (salt, 0) $ unpack str)
112 |       where
113 |         step : (Bits64, Bits64) -> Char -> (Bits64, Bits64)
114 |         step (s, l) x = (hashWithSalt s x, l + 1)
115 |         finalise : (Bits64, Bits64) -> Bits64
116 |         finalise (s, l) = hashWithSalt s l
117 |
118 | export
119 | Hashable Bool where
120 |     hash False = 0
121 |     hash True = 1
122 |     
123 |     hashWithSalt = defaultHashWithSalt hash
124 |
125 | export
126 | (Hashable a, Hashable b) => Hashable (a, b) where
127 |     hashWithSalt salt (a, b) = salt `hashWithSalt` a `hashWithSalt` b
128 |
129 | export
130 | Hashable a => Hashable (Maybe a) where
131 |     hashWithSalt salt Nothing = hashWithSalt salt 0
132 |     hashWithSalt salt (Just x) = hashWithSalt salt 1 `hashWithSalt` x
133 |
134 | export
135 | Hashable a => Hashable (List a) where
136 |     hashWithSalt salt [] = hashWithSalt salt 0
137 |     hashWithSalt salt (x :: xs) =
138 |         salt
139 |             `hashWithSalt` 1
140 |             `hashWithSalt` x
141 |             `hashWithSalt` xs
142 |
143 | export
144 | Hashable a => Hashable (SnocList a) where
145 |     hashWithSalt salt [<] = hashWithSalt salt 0
146 |     hashWithSalt salt (sx :< x) =
147 |         salt
148 |             `hashWithSalt` 1
149 |             `hashWithSalt` x
150 |             `hashWithSalt` sx
151 |
152 | export
153 | Hashable a => Hashable (Vect len a) where
154 |     hashWithSalt salt [] = hashWithSalt salt 0
155 |     hashWithSalt salt (x :: xs) =
156 |         salt
157 |             `hashWithSalt` 1
158 |             `hashWithSalt` x
159 |             `hashWithSalt` xs
160 |
161 |