
   0 | module Core.Hash
   1 | 
   2 | import Core.Case.CaseTree
   3 | import Core.CompileExpr
   4 | import Core.TT
   5 | 
   6 | import Data.List1
   7 | import Libraries.Data.String.Iterator
   8 | import Data.Vect
   9 | 
  10 | %default covering
  11 | 
  12 | -- This is so that we can store a hash of the interface in ttc files, to avoid
  13 | -- the need for reloading modules when no interfaces have changed in imports.
  14 | -- As you can probably tell, I know almost nothing about writing good hash
  15 | -- functions, so better implementations will be very welcome...
  16 | 
  17 | public export
  18 | interface Hashable a where
  19 |   hash : a -> Int
  20 |   hashWithSalt : Int -> a -> Int
  21 | 
  22 |   hash = hashWithSalt 5381
  23 |   hashWithSalt h i = h * 33 + hash i
  24 | 
  25 | export infixl 5 `hashWithSalt`
  26 | 
  27 | export
  28 | Hashable Int where
  29 |   hash = id
  30 | 
  31 | export
  32 | Hashable Int8 where
  33 |   hash = cast
  34 | 
  35 | export
  36 | Hashable Int16 where
  37 |   hash = cast
  38 | 
  39 | export
  40 | Hashable Int32 where
  41 |   hash = cast
  42 | 
  43 | export
  44 | Hashable Int64 where
  45 |   hash = cast
  46 | 
  47 | export
  48 | Hashable Bits8 where
  49 |   hash = cast
  50 | 
  51 | export
  52 | Hashable Bits16 where
  53 |   hash = cast
  54 | 
  55 | export
  56 | Hashable Bits32 where
  57 |   hash = cast
  58 | 
  59 | export
  60 | Hashable Bits64 where
  61 |   hash = cast
  62 | 
  63 | export
  64 | Hashable Integer where
  65 |   hash = fromInteger
  66 | 
  67 | export
  68 | Hashable Nat where
  69 |   hash = cast
  70 | 
  71 | export
  72 | Hashable Char where
  73 |   hash = cast
  74 | 
  75 | export
  76 | Hashable a => Hashable (Vect n a) where
  77 |   hashWithSalt h [] = abs h
  78 |   hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
  79 | 
  80 | export
  81 | Hashable a => Hashable (List a) where
  82 |   hashWithSalt h [] = abs h
  83 |   hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
  84 | 
  85 | export
  86 | Hashable a => Hashable (SnocList a) where
  87 |   hashWithSalt h [<] = abs h
  88 |   hashWithSalt h (xs :< x) = hashWithSalt (h * 33 + hash x) xs
  89 | 
  90 | export
  91 | Hashable a => Hashable (List1 a) where
  92 |   hashWithSalt h xxs = hashWithSalt (h * 33 + hash (head xxs)) (tail xxs)
  93 | 
  94 | export
  95 | Hashable a => Hashable (Maybe a) where
  96 |   hashWithSalt h Nothing = abs h
  97 |   hashWithSalt h (Just x) = hashWithSalt h x
  98 | 
  99 | export
 100 | Hashable a => Hashable b => Hashable (a, b) where
 101 |   hashWithSalt h (x, y) = h `hashWithSalt` x `hashWithSalt` y
 102 | 
 103 | export
 104 | Hashable String where
 105 |   hashWithSalt h = String.Iterator.foldl hashWithSalt h
 106 | 
 107 | export
 108 | Hashable Double where
 109 |   hash = hash . show
 110 | 
 111 | export
 112 | Hashable Namespace where
 113 |   hashWithSalt h ns = hashWithSalt h (unsafeUnfoldNamespace ns)
 114 | 
 115 | export
 116 | Hashable Name where
 117 |   hashWithSalt h (MN s _) = hashWithSalt h s
 118 |   hashWithSalt h (DN _ n) = hashWithSalt h n
 119 |   hashWithSalt h (NS ns n) = hashWithSalt (hashWithSalt h ns) n
 120 |   hashWithSalt h (Resolved i) = hashWithSalt h i
 121 |   hashWithSalt h n = hashWithSalt h (show n)
 122 | 
 123 | export
 124 | Hashable RigCount where
 125 |   hashWithSalt h = elimSemi
 126 |                      (hashWithSalt h 0)
 127 |                      (hashWithSalt h 1)
 128 |                      (const $ hashWithSalt h 2)
 129 | 
 130 | export
 131 | Hashable t => Hashable (PiInfo t) where
 132 |   hashWithSalt h Implicit = hashWithSalt h 0
 133 |   hashWithSalt h Explicit = hashWithSalt h 1
 134 |   hashWithSalt h AutoImplicit = hashWithSalt h 2
 135 |   hashWithSalt h (DefImplicit t) = h `hashWithSalt` 3 `hashWithSalt` t
 136 | 
 137 | export
 138 | Hashable ty => Hashable (Binder ty) where
 139 |   hashWithSalt h (Lam _ c p ty)
 140 |       = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
 141 |   hashWithSalt h (Let _ c val ty)
 142 |       = h `hashWithSalt` 1 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
 143 |   hashWithSalt h (Pi _ c p ty)
 144 |       = h `hashWithSalt` 2 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
 145 |   hashWithSalt h (PVar _ c p ty)
 146 |       = h `hashWithSalt` 3 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
 147 |   hashWithSalt h (PLet _ c val ty)
 148 |       = h `hashWithSalt` 4 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
 149 |   hashWithSalt h (PVTy _ c ty)
 150 |       = h `hashWithSalt` 5 `hashWithSalt` c `hashWithSalt` ty
 151 | 
 152 | Hashable (Var vars) where
 153 |   hashWithSalt h (MkVar {varIdx = i} _) = hashWithSalt h i
 154 | 
 155 | mutual
 156 |   export
 157 |   Hashable (Term vars) where
 158 |     hashWithSalt h (Local fc x idx y)
 159 |         = h `hashWithSalt` 0 `hashWithSalt` idx
 160 |     hashWithSalt h (Ref fc x name)
 161 |         = h `hashWithSalt` 1 `hashWithSalt` name
 162 |     hashWithSalt h (Meta fc x y xs)
 163 |         = h `hashWithSalt` 2 `hashWithSalt` y `hashWithSalt` xs
 164 |     hashWithSalt h (Bind fc x b scope)
 165 |         = h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope
 166 |     hashWithSalt h (App fc fn arg)
 167 |         = h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg
 168 |     hashWithSalt h (As fc _ nm pat)
 169 |         = h `hashWithSalt` 5 `hashWithSalt` nm `hashWithSalt` pat
 170 |     hashWithSalt h (TDelayed fc x y)
 171 |         = h `hashWithSalt` 6 `hashWithSalt` y
 172 |     hashWithSalt h (TDelay fc x t y)
 173 |         = h `hashWithSalt` 7 `hashWithSalt` t `hashWithSalt` y
 174 |     hashWithSalt h (TForce fc r x)
 175 |         = h `hashWithSalt` 8 `hashWithSalt` x
 176 |     hashWithSalt h (PrimVal fc c)
 177 |         = h `hashWithSalt` 9 `hashWithSalt` (show c)
 178 |     hashWithSalt h (Erased fc _)
 179 |         = hashWithSalt h 10
 180 |     hashWithSalt h (TType fc u)
 181 |         = hashWithSalt h 11 `hashWithSalt` u
 182 | 
 183 |   export
 184 |   Hashable Pat where
 185 |     hashWithSalt h (PAs fc nm pat)
 186 |         = h `hashWithSalt` 0 `hashWithSalt` nm `hashWithSalt` pat
 187 |     hashWithSalt h (PCon fc x tag arity xs)
 188 |         = h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs
 189 |     hashWithSalt h (PTyCon fc x arity xs)
 190 |         = h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` xs
 191 |     hashWithSalt h (PConst fc c)
 192 |         = h `hashWithSalt` 3 `hashWithSalt` (show c)
 193 |     hashWithSalt h (PArrow fc x s t)
 194 |         = h `hashWithSalt` 4 `hashWithSalt` s `hashWithSalt` t
 195 |     hashWithSalt h (PDelay fc r t p)
 196 |         = h `hashWithSalt` 5 `hashWithSalt` t `hashWithSalt` p
 197 |     hashWithSalt h (PLoc fc x)
 198 |         = h `hashWithSalt` 6 `hashWithSalt` x
 199 |     hashWithSalt h (PUnmatchable fc x)
 200 |         = h `hashWithSalt` 7 `hashWithSalt` x
 201 | 
 202 |   export
 203 |   Hashable (CaseTree vars) where
 204 |     hashWithSalt h (Case idx x scTy xs)
 205 |         = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
 206 |     hashWithSalt h (STerm _ x)
 207 |         = h `hashWithSalt` 1 `hashWithSalt` x
 208 |     hashWithSalt h (Unmatched msg)
 209 |         = h `hashWithSalt` 2
 210 |     hashWithSalt h Impossible
 211 |         = h `hashWithSalt` 3
 212 | 
 213 |   export
 214 |   Hashable (CaseAlt vars) where
 215 |     hashWithSalt h (ConCase x tag args y)
 216 |         = h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args
 217 |             `hashWithSalt` y
 218 |     hashWithSalt h (DelayCase t x y)
 219 |         = h `hashWithSalt` 2 `hashWithSalt` (show t)
 220 |             `hashWithSalt` (show x) `hashWithSalt` y
 221 |     hashWithSalt h (ConstCase x y)
 222 |         = h `hashWithSalt` 3 `hashWithSalt` (show x) `hashWithSalt` y
 223 |     hashWithSalt h (DefaultCase x)
 224 |         = h `hashWithSalt` 4 `hashWithSalt` x
 225 | 
 226 | export
 227 | Hashable CFType where
 228 |   hashWithSalt h = \case
 229 |     CFUnit =>
 230 |       h `hashWithSalt` 0
 231 |     CFInt =>
 232 |       h `hashWithSalt` 1
 233 |     CFUnsigned8 =>
 234 |       h `hashWithSalt` 2
 235 |     CFUnsigned16 =>
 236 |       h `hashWithSalt` 3
 237 |     CFUnsigned32 =>
 238 |       h `hashWithSalt` 4
 239 |     CFUnsigned64 =>
 240 |       h `hashWithSalt` 5
 241 |     CFString =>
 242 |       h `hashWithSalt` 6
 243 |     CFDouble =>
 244 |       h `hashWithSalt` 7
 245 |     CFChar =>
 246 |       h `hashWithSalt` 8
 247 |     CFPtr =>
 248 |       h `hashWithSalt` 9
 249 |     CFGCPtr =>
 250 |       h `hashWithSalt` 10
 251 |     CFBuffer =>
 252 |       h `hashWithSalt` 11
 253 |     CFWorld =>
 254 |       h `hashWithSalt` 12
 255 |     CFFun a b =>
 256 |       h `hashWithSalt` 13 `hashWithSalt` a `hashWithSalt` b
 257 |     CFIORes a =>
 258 |       h `hashWithSalt` 14 `hashWithSalt` a
 259 |     CFStruct n fs =>
 260 |       h `hashWithSalt` 15 `hashWithSalt` n `hashWithSalt` fs
 261 |     CFUser n xs =>
 262 |       h `hashWithSalt` 16 `hashWithSalt` n `hashWithSalt` xs
 263 |     CFInt8 =>
 264 |       h `hashWithSalt` 17
 265 |     CFInt16 =>
 266 |       h `hashWithSalt` 18
 267 |     CFInt32 =>
 268 |       h `hashWithSalt` 19
 269 |     CFInt64 =>
 270 |       h `hashWithSalt` 20
 271 |     CFForeignObj =>
 272 |       h `hashWithSalt` 21
 273 |     CFInteger =>
 274 |       h `hashWithSalt` 22
 275 | 
 276 | export
 277 | Hashable PrimType where
 278 |   hashWithSalt h = \case
 279 |     IntType     => h `hashWithSalt` 1
 280 |     Int8Type    => h `hashWithSalt` 2
 281 |     Int16Type   => h `hashWithSalt` 3
 282 |     Int32Type   => h `hashWithSalt` 4
 283 |     Int64Type   => h `hashWithSalt` 5
 284 |     IntegerType => h `hashWithSalt` 6
 285 |     Bits8Type   => h `hashWithSalt` 7
 286 |     Bits16Type  => h `hashWithSalt` 8
 287 |     Bits32Type  => h `hashWithSalt` 9
 288 |     Bits64Type  => h `hashWithSalt` 10
 289 |     StringType  => h `hashWithSalt` 11
 290 |     CharType    => h `hashWithSalt` 12
 291 |     DoubleType  => h `hashWithSalt` 13
 292 |     WorldType   => h `hashWithSalt` 14
 293 | 
 294 | export
 295 | Hashable Constant where
 296 |   hashWithSalt h = \case
 297 |     I i   => h `hashWithSalt` 0  `hashWithSalt` i
 298 |     I8 x  => h `hashWithSalt` 1  `hashWithSalt` x
 299 |     I16 x => h `hashWithSalt` 2  `hashWithSalt` x
 300 |     I32 x => h `hashWithSalt` 3  `hashWithSalt` x
 301 |     I64 x => h `hashWithSalt` 4  `hashWithSalt` x
 302 |     BI x  => h `hashWithSalt` 5  `hashWithSalt` x
 303 |     B8 x  => h `hashWithSalt` 6  `hashWithSalt` x
 304 |     B16 x => h `hashWithSalt` 7  `hashWithSalt` x
 305 |     B32 x => h `hashWithSalt` 8  `hashWithSalt` x
 306 |     B64 x => h `hashWithSalt` 9  `hashWithSalt` x
 307 |     Str x => h `hashWithSalt` 10 `hashWithSalt` x
 308 |     Ch x  => h `hashWithSalt` 11 `hashWithSalt` x
 309 |     Db x  => h `hashWithSalt` 12 `hashWithSalt` x
 310 |     PrT x => h `hashWithSalt` 13 `hashWithSalt` x
 311 | 
 312 |     WorldVal => h `hashWithSalt` 14
 313 | 
 314 | export
 315 | Hashable LazyReason where
 316 |   hashWithSalt h = \case
 317 |     LInf => h `hashWithSalt` 0
 318 |     LLazy => h `hashWithSalt` 1
 319 |     LUnknown => h `hashWithSalt` 2
 320 | 
 321 | export
 322 | Hashable (PrimFn arity) where
 323 |   hashWithSalt h = \case
 324 |     Add ty =>
 325 |       h `hashWithSalt` 0 `hashWithSalt` ty
 326 |     Sub ty =>
 327 |       h `hashWithSalt` 1 `hashWithSalt` ty
 328 |     Mul ty =>
 329 |       h `hashWithSalt` 2 `hashWithSalt` ty
 330 |     Div ty =>
 331 |       h `hashWithSalt` 3 `hashWithSalt` ty
 332 |     Mod ty =>
 333 |       h `hashWithSalt` 4 `hashWithSalt` ty
 334 |     Neg ty =>
 335 |       h `hashWithSalt` 5 `hashWithSalt` ty
 336 |     ShiftL ty =>
 337 |       h `hashWithSalt` 6 `hashWithSalt` ty
 338 |     ShiftR ty =>
 339 |       h `hashWithSalt` 7 `hashWithSalt` ty
 340 | 
 341 |     BAnd ty =>
 342 |       h `hashWithSalt` 8 `hashWithSalt` ty
 343 |     BOr ty =>
 344 |       h `hashWithSalt` 9 `hashWithSalt` ty
 345 |     BXOr ty =>
 346 |       h `hashWithSalt` 10 `hashWithSalt` ty
 347 | 
 348 |     LT ty =>
 349 |       h `hashWithSalt` 11 `hashWithSalt` ty
 350 |     LTE ty =>
 351 |       h `hashWithSalt` 12 `hashWithSalt` ty
 352 |     EQ ty =>
 353 |       h `hashWithSalt` 13 `hashWithSalt` ty
 354 |     GTE ty =>
 355 |       h `hashWithSalt` 14 `hashWithSalt` ty
 356 |     GT ty =>
 357 |       h `hashWithSalt` 15 `hashWithSalt` ty
 358 | 
 359 |     StrLength =>
 360 |       h `hashWithSalt` 16
 361 |     StrHead =>
 362 |       h `hashWithSalt` 17
 363 |     StrTail =>
 364 |       h `hashWithSalt` 18
 365 |     StrIndex =>
 366 |       h `hashWithSalt` 19
 367 |     StrCons =>
 368 |       h `hashWithSalt` 20
 369 |     StrAppend =>
 370 |       h `hashWithSalt` 21
 371 |     StrReverse =>
 372 |       h `hashWithSalt` 22
 373 |     StrSubstr =>
 374 |       h `hashWithSalt` 23
 375 | 
 376 |     DoubleExp =>
 377 |       h `hashWithSalt` 24
 378 |     DoubleLog =>
 379 |       h `hashWithSalt` 25
 380 |     DoubleSin =>
 381 |       h `hashWithSalt` 26
 382 |     DoubleCos =>
 383 |       h `hashWithSalt` 27
 384 |     DoubleTan =>
 385 |       h `hashWithSalt` 28
 386 |     DoubleASin =>
 387 |       h `hashWithSalt` 29
 388 |     DoubleACos =>
 389 |       h `hashWithSalt` 30
 390 |     DoubleATan =>
 391 |       h `hashWithSalt` 31
 392 |     DoubleSqrt =>
 393 |       h `hashWithSalt` 32
 394 |     DoubleFloor =>
 395 |       h `hashWithSalt` 33
 396 |     DoubleCeiling =>
 397 |       h `hashWithSalt` 34
 398 | 
 399 |     Cast f t =>
 400 |       h `hashWithSalt` 35 `hashWithSalt` f `hashWithSalt` t
 401 |     BelieveMe =>
 402 |       h `hashWithSalt` 36
 403 |     Crash =>
 404 |       h `hashWithSalt` 37
 405 | 
 406 |     DoublePow =>
 407 |       h `hashWithSalt` 38
 408 | 
 409 | export
 410 | Hashable ConInfo where
 411 |   hashWithSalt h = \case
 412 |     DATACON => h `hashWithSalt` 0
 413 |     TYCON => h `hashWithSalt` 1
 414 |     NIL => h `hashWithSalt` 2
 415 |     CONS => h `hashWithSalt` 3
 416 |     ENUM n => h `hashWithSalt` 4 `hashWithSalt` n
 417 |     NOTHING => h `hashWithSalt` 5
 418 |     JUST => h `hashWithSalt` 6
 419 |     RECORD => h `hashWithSalt` 7
 420 |     ZERO => h `hashWithSalt` 8
 421 |     SUCC => h `hashWithSalt` 9
 422 |     UNIT => h `hashWithSalt` 10
 423 | 
 424 | mutual
 425 |   export
 426 |   Hashable NamedCExp where
 427 |     hashWithSalt h = \case
 428 |       NmLocal fc n =>
 429 |         h `hashWithSalt` 0 `hashWithSalt` n
 430 |       NmRef fc n =>
 431 |         h `hashWithSalt` 1 `hashWithSalt` n
 432 |       NmLam fc x rhs =>
 433 |         h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` rhs
 434 |       NmLet fc x val rhs =>
 435 |         h `hashWithSalt` 3 `hashWithSalt` x `hashWithSalt` val `hashWithSalt` rhs
 436 |       NmApp fc f xs =>
 437 |         h `hashWithSalt` 4 `hashWithSalt` f `hashWithSalt` xs
 438 |       NmCon fc cn ci t args =>
 439 |         h `hashWithSalt` 5 `hashWithSalt` cn `hashWithSalt` ci `hashWithSalt` t `hashWithSalt` args
 440 |       NmOp fc fn args =>
 441 |         h `hashWithSalt` 6 `hashWithSalt` fn `hashWithSalt` args
 442 |       NmExtPrim fc p args =>
 443 |         h `hashWithSalt` 7 `hashWithSalt` p `hashWithSalt` args
 444 |       NmForce fc r x =>
 445 |         h `hashWithSalt` 8 `hashWithSalt` r `hashWithSalt` x
 446 |       NmDelay fc r x =>
 447 |         h `hashWithSalt` 9 `hashWithSalt` r `hashWithSalt` x
 448 |       NmConCase fc sc alts df =>
 449 |         h `hashWithSalt` 10 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
 450 |       NmConstCase fc sc alts df =>
 451 |         h `hashWithSalt` 11 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
 452 |       NmPrimVal fc c =>
 453 |         h `hashWithSalt` 12 `hashWithSalt` c
 454 |       NmErased fc =>
 455 |         h `hashWithSalt` 13
 456 |       NmCrash fc msg =>
 457 |         h `hashWithSalt` 14 `hashWithSalt` msg
 458 | 
 459 |   export
 460 |   Hashable NamedConAlt where
 461 |     hashWithSalt h (MkNConAlt n ci tag args rhs) =
 462 |       h `hashWithSalt` n `hashWithSalt` ci `hashWithSalt` tag `hashWithSalt` args `hashWithSalt` rhs
 463 | 
 464 |   export
 465 |   Hashable NamedConstAlt where
 466 |     hashWithSalt h (MkNConstAlt c rhs) =
 467 |       h `hashWithSalt` c `hashWithSalt` rhs
 468 | 
 469 | export
 470 | Hashable NamedDef where
 471 |   hashWithSalt h = \case
 472 |     MkNmFun args ce =>
 473 |       h `hashWithSalt` 0 `hashWithSalt` args `hashWithSalt` ce
 474 |     MkNmCon tag arity nt =>
 475 |       h `hashWithSalt` 1 `hashWithSalt` tag `hashWithSalt` arity `hashWithSalt` nt
 476 |     MkNmForeign ccs fargs cft =>
 477 |       h `hashWithSalt` 2 `hashWithSalt` ccs `hashWithSalt` fargs `hashWithSalt` cft
 478 |     MkNmError e =>
 479 |       h `hashWithSalt` 3 `hashWithSalt` e
 480 |