
  0 | module Derive.Hashable
  1 | 
  2 | import public Data.Hashable
  3 | import Language.Mk
  4 | import Language.Reflection.Util
  5 | 
  6 | %default total
  7 | 
  8 | %language ElabReflection
  9 | 
 10 | %macro %inline
 11 | MkName : (t : ty) -> Elab Name
 12 | MkName = getMk
 13 | 
 14 | export
 15 | HashableVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 16 | HashableVis vis nms p = do
 17 |   let fun := funName p "hashWithSalt"
 18 |   let impl := implName p "Hashable"
 19 |   Right
 20 |     [ TL (hwsClaim fun p) (hwsDef fun p.info)
 21 |     , TL (hashableImplClaim impl p) (hashableImplDef fun impl)
 22 |     ]
 23 |   where
 24 |     hwsClaim : Name -> ParamTypeInfo -> Decl
 25 |     hwsClaim fun p =
 26 |       simpleClaim vis fun $
 27 |         piAll `(Bits64 -> ~(p.applied) -> Bits64) $ allImplicits p "Hashable"
 28 |     
 29 |     hwsDef : Name -> TypeInfo -> Decl
 30 |     hwsDef fun ti =
 31 |       def fun $ map clause $ [0 .. length ti.cons] `zip` ti.cons where
 32 | 
 33 |         clause : (Nat, Con _ _) -> Clause
 34 |         clause (idx, con) = accumArgs unerased (\x => `(~(var fun) salt ~x)) rhs arg con where
 35 | 
 36 |           arg : BoundArg 1 Unerased -> TTImp
 37 |           -- arg (BA a [x] _) = if unAppAny a.type == var ti.name then `(flip ~(var fun) ~(var x)) else `(flip hashWithSalt ~(var x))
 38 |           arg (BA a [x] _) = var x
 39 | 
 40 |           rhs : SnocList TTImp -> TTImp
 41 |           rhs = foldl (\l, r => `(assert_total $ hashWithSalt ~l ~r)) `(hashWithSalt salt ~(primVal $ BI $ cast idx))
 42 |     
 43 |     hashableImplClaim : Name -> ParamTypeInfo -> Decl
 44 |     hashableImplClaim impl p = implClaimVis vis impl $ implType "Hashable" p
 45 | 
 46 |     hashableImplDef : (fun, impl : Name) -> Decl 
 47 |     hashableImplDef fun impl = 
 48 |       def impl $ pure $ patClause (var impl) (`(~(var $ MkName Hashable) ~(var fun) (~(var fun) defaultSalt)))
 49 | 
 50 | 
 51 | 
 52 | export %inline
 53 | Hashable : List Name -> ParamTypeInfo -> Res (List TopLevel)
 54 | Hashable = HashableVis Public
 55 | 
 56 | -- %runElab derive "Namespace" [Hashable]