Add hashable deriving.

src/Init/Data/Hashable.lean

@@ -39,3 +39,11 @@ instance : Hashable UInt64 where
 
 instance : Hashable USize where
   hash n := n
+
+instance : Hashable Int where
+  hash 
+    | Int.ofNat n => USize.ofNat (2 * n)
+    | Int.negSucc n => USize.ofNat (2 * n + 1)
+
+instance (P : Prop) : Hashable P where
+  hash := Function.const P 0

src/Init/Prelude.lean

@@ -1562,7 +1562,7 @@ instance nonBacktrackable : Backtrackable PUnit σ where
 
 end EStateM
 
-class Hashable (α : Type u) where
+class Hashable (α : Sort u) where
   hash : α → USize
 
 export Hashable (hash)

src/Lean/Elab/Deriving.lean

@@ -11,3 +11,4 @@ import Lean.Elab.Deriving.DecEq
 import Lean.Elab.Deriving.Repr
 import Lean.Elab.Deriving.FromToJson
 import Lean.Elab.Deriving.SizeOf
+import Lean.Elab.Deriving.Hashable

src/Lean/Elab/Deriving/Hashable.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dany Fabian
+-/
+import Lean.Meta.Inductive
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Util
+
+namespace Lean.Elab.Deriving.Hashable
+open Command
+open Lean.Parser.Term
+open Meta
+
+def mkHashableHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
+  mkHeader ctx `Hashable 1 indVal
+
+def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFuncIdx : Nat) : TermElabM Syntax := do
+  let discrs ← mkDiscrs header indVal
+  let alts ← mkAlts
+  `(match $[$discrs],* with $alts:matchAlt*)
+where
+
+  mkAlts : TermElabM (Array Syntax) := do
+    let mut alts := #[]
+    let mut ctorIdx := 0
+    let allIndVals := indVal.all.toArray
+    for ctorName in indVal.ctors do
+      let ctorInfo ← getConstInfoCtor ctorName
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
+        let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+        let mut patterns := #[]
+        -- add `_` pattern for indices
+        for i in [:indVal.numIndices] do
+          patterns := patterns.push (← `(_))
+        let mut ctorArgs := #[]
+        let mut rhs ← `($(quote ctorIdx))
+        -- add `_` for inductive parameters, they are inaccessible
+        for i in [:indVal.numParams] do
+          ctorArgs := ctorArgs.push (← `(_))
+        for i in [:ctorInfo.numFields] do
+          let x := xs[indVal.numParams + i]
+          let xTy ← inferType x
+          let typeName := xTy.getAppFn.constName!
+          let a := mkIdent (← mkFreshUserName `a)
+          ctorArgs := ctorArgs.push a
+          match allIndVals.findIdx? (· == typeName) with
+          | some x => rhs ← `(mixHash $rhs ($(mkIdent ctx.auxFunNames[x]) $a:ident))
+          | none => rhs ← `(mixHash $rhs (hash $a:ident))
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
+        `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
+      alts := alts.push alt
+      ctorIdx := ctorIdx + 1
+    return alts
+
+def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
+  let auxFunName ← ctx.auxFunNames[i]
+  let indVal     ← ctx.typeInfos[i]
+  let header     ← mkHashableHeader ctx indVal
+  let body       ← mkMatch ctx header indVal i
+  let binders    := header.binders
+  if ctx.usePartial then
+    -- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
+    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term) 
+  else
+    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term) 
+
+def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
+  let mut auxDefs := #[]
+  for i in [:ctx.typeInfos.size] do
+    auxDefs := auxDefs.push (← mkAuxFunction ctx i)
+  `(mutual $auxDefs:command* end)
+
+private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "hash" declNames[0]
+  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable declNames)
+  trace[Elab.Deriving.hashable] "\n{cmds}"
+  return cmds
+
+def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
+  if (← declNames.allM isInductive) && declNames.size > 0 then
+    let cmds ← liftTermElabM none <| mkHashableInstanceCmds declNames
+    cmds.forM elabCommand
+    return true
+  else
+    return false
+
+builtin_initialize
+  registerBuiltinDerivingHandler ``Hashable mkHashableHandler
+  registerTraceClass `Elab.Deriving.hashable

tests/playground/hashable.lean

@@ -0,0 +1,83 @@
+set_option trace.Elab.Deriving.hashable true
+
+inductive SimpleInd
+| A
+| B
+deriving Hashable
+
+theorem «inductive fields have different base hashes» : ∀ x, hash x = 
+match x with
+| SimpleInd.A => 0
+| SimpleInd.B => 1 := λ x => rfl
+mutual 
+inductive Foo : Type → Type
+| A : Int → (3 = 3) → String → Foo Int
+| B : Bar → Foo String 
+deriving Hashable
+inductive Bar
+| C
+| D : Foo String → Bar 
+deriving Hashable
+end
+
+#eval hash (Foo.A 3 rfl "bla")
+#eval hash (Foo.B $ Bar.D $ Foo.B Bar.C)
+
+inductive ManyConstructors | A | B | C | D | E | F | G | H | I | J | K | L 
+| M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
+deriving Hashable
+
+theorem «Each constructor is hashed as a different number to make mixing better» : ∀ x, hash x = 
+match x with 
+| ManyConstructors.A => 0
+| ManyConstructors.B => 1
+| ManyConstructors.C => 2
+| ManyConstructors.D => 3
+| ManyConstructors.E => 4
+| ManyConstructors.F => 5
+| ManyConstructors.G => 6
+| ManyConstructors.H => 7
+| ManyConstructors.I => 8
+| ManyConstructors.J => 9
+| ManyConstructors.K => 10
+| ManyConstructors.L => 11
+| ManyConstructors.M => 12
+| ManyConstructors.N => 13
+| ManyConstructors.O => 14
+| ManyConstructors.P => 15
+| ManyConstructors.Q => 16
+| ManyConstructors.R => 17
+| ManyConstructors.S => 18
+| ManyConstructors.T => 19
+| ManyConstructors.U => 20
+| ManyConstructors.V => 21
+| ManyConstructors.W => 22
+| ManyConstructors.X => 23
+| ManyConstructors.Y => 24
+| ManyConstructors.Z => 25 := λ x => rfl
+
+structure Person := 
+  FirstName : String
+  LastName : String
+  Age : Nat
+deriving Hashable
+
+structure Company :=
+  Name : String
+  CEO : Person
+  NumberOfEmployees : Nat
+deriving Hashable
+
+-- structures hash just fine 
+#eval hash { 
+  Name := "Microsoft" 
+  CEO := { FirstName := "Satya", LastName := "Nadella", Age := 53 } 
+  NumberOfEmployees := 165000 : Company }
+-- 10875484723257753924
+
+-- syntax(name := tst) "tst" : command
+-- @[commandElab «tst»] def elab_tst : CommandElab := fun stx => do
+--   let declNames := #[`Foo, `Bar]
+--   let declNames := #[`Foo]
+--   discard $ mkHashableHandler declNames
+--   pure ()