perf: derive Repr, BEq and Hashable once per mutual block

src/Lean/Elab/Deriving/BEq.lean

@@ -206,8 +206,8 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-def mkBEqInstanceCmds (ctx : Context) (declName : Name) : TermElabM (Array Syntax) := do
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName])
+def mkBEqInstanceCmds (ctx : Context) (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
 
@@ -222,22 +222,27 @@ def mkBEqEnumCmd (ctx : Context) (name : Name): TermElabM (Array Syntax) := do
 
 open Command
 
-def mkBEqInstance (declName : Name) : CommandElabM Unit := do
-  withoutExposeFromCtors declName do
+/-- Derives `BEq` for `declNames`, which must belong to the same mutual block. -/
+def mkBEqInstance (declNames : Array Name) : CommandElabM Unit := do
+  let declName := declNames[0]!
+  withoutExposeFromCtorsAll declNames do
     let ctx ← liftTermElabM <| mkContext ``BEq "beq" declName
     let cmds ← liftTermElabM <|
       if (← isEnumType declName) then
         mkBEqEnumCmd ctx declName
       else
-        mkBEqInstanceCmds ctx declName
+        mkBEqInstanceCmds ctx declNames
+    -- `mkInstName` picks names still free, so compute them before adding the instances.
+    let instNames ← liftTermElabM <| declNames.mapM (mkInstName ``BEq)
     cmds.forM elabCommand
     unless ctx.usePartial do
-      elabCommand (← `(attribute [method_specs] $(mkIdent ctx.instName):ident))
+      for instName in instNames do
+        elabCommand (← `(attribute [method_specs] $(mkIdent instName):ident))
 
 def mkBEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then
-    for declName in declNames do
-      mkBEqInstance declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      mkBEqInstance block
     return true
   else
     return false

src/Lean/Elab/Deriving/Hashable.lean

@@ -80,18 +80,19 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual $auxDefs:command* end)
 
-private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext ``Hashable "hash" declName
-  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName])
+/-- Builds one aux-function block for the mutual block of `declNames` and an instance for each. -/
+private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext ``Hashable "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
   withoutExporting do  -- This deriving handler handles visibility of generated decls syntactically
   if (← declNames.allM isInductive)  then
-    for declName in declNames do
-      withoutExposeFromCtors declName do
-        let cmds ← liftTermElabM <| mkHashableInstanceCmds declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      withoutExposeFromCtorsAll block do
+        let cmds ← liftTermElabM <| mkHashableInstanceCmds block
         cmds.forM elabCommand
     return true
   else

src/Lean/Elab/Deriving/Repr.lean

@@ -112,19 +112,20 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext ``Repr "repr" declName
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName])
+/-- Builds one aux-function block for the mutual block of `declNames` and an instance for each. -/
+private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext ``Repr "repr" declNames[0]!
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames)
   trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds
 
 open Command
 
 def mkReprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then
-    for declName in declNames do
-      withoutExposeFromCtors declName do
-        let cmds ← liftTermElabM <| mkReprInstanceCmd declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      withoutExposeFromCtorsAll block do
+        let cmds ← liftTermElabM <| mkReprInstanceCmds block
         cmds.forM elabCommand
     return true
   else

src/Lean/Elab/Deriving/Util.lean

@@ -83,7 +83,15 @@ def withoutExposeFromCtors (typeName : Name) (cont : CommandElabM α) : CommandE
         attrs := sc.attrs.filter (!· matches `(Parser.Term.attrInstance| expose)) }) cont
   else cont
 
+/-- Runs `cont` under `withoutExposeFromCtors` for each of `typeNames`. -/
+def withoutExposeFromCtorsAll (typeNames : Array Name) (cont : CommandElabM α) : CommandElabM α :=
+  typeNames.foldr withoutExposeFromCtors cont
+
 structure Context where
+  /--
+  The instance name for the type passed to `mkContext`, which also prefixes `auxFunNames`.
+  `mkInstanceCmds` names each instance after its own type instead.
+  -/
   instName    : Name
   typeInfos   : Array InductiveVal
   auxFunNames : Array Name
@@ -158,10 +166,24 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let mut val      := mkIdent auxFunName
       if useAnonCtor then
         val ← `(⟨$val⟩)
-      let instCmd ← `(instance $(mkIdent ctx.instName):ident $binders:implicitBinder* : $type := $val)
+      let instName     ← mkInstName className indVal.name
+      let instCmd ← `(instance $(mkIdent instName):ident $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
 
+/-- Groups inductive type names by mutual block, keeping the given order. -/
+def groupByMutualBlock (declNames : Array Name) : CoreM (Array (Array Name)) := do
+  let mut blocks : Array (Array Name) := #[]
+  let mut idxOfBlock : NameMap Nat := {}
+  for declName in declNames do
+    let head := (← getConstInfoInduct declName).all.head!
+    if let some i := idxOfBlock.find? head then
+      blocks := blocks.modify i (·.push declName)
+    else
+      idxOfBlock := idxOfBlock.insert head blocks.size
+      blocks := blocks.push #[declName]
+  return blocks
+
 def mkDiscr (varName : Name) : TermElabM (TSyntax ``Parser.Term.matchDiscr) :=
  `(Parser.Term.matchDiscr| $(mkIdent varName):term)
 

tests/elab/derivingBEqMutualOnce.lean

@@ -0,0 +1,81 @@
+/-!
+`deriving BEq` on a mutual block generates one block of auxiliary functions for the whole block
+instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.beq]
+    [mutual
+       set_option match.ignoreUnusedAlts✝ true
+       partial def instBEqA.beq_1 (x✝ : @A✝) (x✝¹ : @A✝) : Bool✝ :=
+         let localinst✝ : BEq✝ (@A✝) := ⟨instBEqA.beq_1⟩;
+         let localinst✝¹ : BEq✝ (@B✝) := ⟨instBEqA.beq_2⟩;
+         match x✝, x✝¹ with
+         | @A.a a✝, @A.a b✝ => a✝ == b✝
+         | @A.leaf, @A.leaf => true✝
+         | _, _ => false✝
+       partial def instBEqA.beq_2 (x✝² : @B✝) (x✝³ : @B✝) : Bool✝ :=
+         let localinst✝² : BEq✝ (@A✝) := ⟨instBEqA.beq_1⟩;
+         let localinst✝³ : BEq✝ (@B✝) := ⟨instBEqA.beq_2⟩;
+         match x✝², x✝³ with
+         | @B.b a✝¹, @B.b b✝¹ => a✝¹ == b✝¹
+         | @B.leaf, @B.leaf => true✝
+         | _, _ => false✝
+     end,
+     instance instBEqA : BEq✝ (@A✝) :=
+       ⟨instBEqA.beq_1⟩,
+     instance instBEqB : BEq✝ (@B✝) :=
+       ⟨instBEqA.beq_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.beq true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving BEq
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving BEq
+end
+
+#guard A.a (.b .leaf) == A.a (.b .leaf)
+#guard A.a (.b .leaf) != A.a .leaf
+#guard B.b (.a .leaf) == B.b (.a .leaf)
+#guard B.b (.a .leaf) != B.leaf
+
+example : BEq A := instBEqA
+example : BEq B := instBEqB
+
+/-! Types from different mutual blocks, and an enum, in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+inductive F where
+  | x | y
+
+deriving instance BEq for C, E, F, D
+
+#guard C.c (.d .leaf) == C.c (.d .leaf)
+#guard C.c (.d .leaf) != C.leaf
+#guard D.d (.c .leaf) == D.d (.c .leaf)
+#guard E.e 3 == E.e 3
+#guard E.e 3 != E.e 4
+#guard F.x == F.x
+#guard F.x != F.y
+
+example : BEq C := instBEqC
+example : BEq D := instBEqD
+example : BEq E := instBEqE
+example : BEq F := instBEqF

tests/elab/derivingHashableMutualOnce.lean

@@ -0,0 +1,69 @@
+/-!
+`deriving Hashable` on a mutual block generates one block of auxiliary functions for the whole
+block instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.hashable]
+    [mutual
+       partial def instHashableA.hash_1 (x✝ : @A✝) : UInt64✝ :=
+         let localinst✝ : Hashable✝ (@A✝) := ⟨instHashableA.hash_1⟩;
+         let localinst✝¹ : Hashable✝ (@B✝) := ⟨instHashableA.hash_2⟩;
+         match x✝ with
+         | @A.a a✝ => mixHash✝ 0 (instHashableA.hash_2 a✝)
+         | @A.leaf => 1
+       partial def instHashableA.hash_2 (x✝¹ : @B✝) : UInt64✝ :=
+         let localinst✝² : Hashable✝ (@A✝) := ⟨instHashableA.hash_1⟩;
+         let localinst✝³ : Hashable✝ (@B✝) := ⟨instHashableA.hash_2⟩;
+         match x✝¹ with
+         | @B.b a✝¹ => mixHash✝ 0 (instHashableA.hash_1 a✝¹)
+         | @B.leaf => 1
+     end,
+     instance instHashableA : Hashable✝ (@A✝) :=
+       ⟨instHashableA.hash_1⟩,
+     instance instHashableB : Hashable✝ (@B✝) :=
+       ⟨instHashableA.hash_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.hashable true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving Hashable
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving Hashable
+end
+
+#guard hash (A.a (.b .leaf)) == hash (A.a (.b .leaf))
+#guard hash (A.a (.b .leaf)) != hash (A.a .leaf)
+#guard hash (B.b (.a .leaf)) != hash B.leaf
+
+example : Hashable A := instHashableA
+example : Hashable B := instHashableB
+
+/-! Types from different mutual blocks in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+deriving instance Hashable for C, E, D
+
+#guard hash (C.c (.d .leaf)) == hash (C.c (.d .leaf))
+#guard hash (D.d (.c .leaf)) != hash D.leaf
+#guard hash (E.e 3) != hash (E.e 4)
+
+example : Hashable C := instHashableC
+example : Hashable D := instHashableD
+example : Hashable E := instHashableE

tests/elab/derivingReprMutualOnce.lean

@@ -0,0 +1,90 @@
+/-!
+`deriving Repr` on a mutual block generates one block of auxiliary functions for the whole block
+instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.repr]
+    [mutual
+       @[no_expose✝]
+       partial def instReprA.repr_1 (x✝ : @A✝) (prec✝ : Nat✝) : Format✝ :=
+         let localinst✝ : Repr✝ (@A✝) := ⟨instReprA.repr_1⟩;
+         let localinst✝¹ : Repr✝ (@B✝) := ⟨instReprA.repr_2⟩;
+         match x✝ with
+         | @A.a a✝ =>
+           Repr.addAppParen✝
+             (Format.group✝
+               (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "A.a" ++ Format.line✝ ++ reprArg✝ a✝)))
+             prec✝
+         | @A.leaf =>
+           Repr.addAppParen✝ (Format.group✝ (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "A.leaf")))
+             prec✝
+       @[no_expose✝]
+       partial def instReprA.repr_2 (x✝¹ : @B✝) (prec✝ : Nat✝) : Format✝ :=
+         let localinst✝² : Repr✝ (@A✝) := ⟨instReprA.repr_1⟩;
+         let localinst✝³ : Repr✝ (@B✝) := ⟨instReprA.repr_2⟩;
+         match x✝¹ with
+         | @B.b a✝¹ =>
+           Repr.addAppParen✝
+             (Format.group✝
+               (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "B.b" ++ Format.line✝ ++ reprArg✝ a✝¹)))
+             prec✝
+         | @B.leaf =>
+           Repr.addAppParen✝ (Format.group✝ (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "B.leaf")))
+             prec✝
+     end,
+     instance instReprA : Repr✝ (@A✝) :=
+       ⟨instReprA.repr_1⟩,
+     instance instReprB : Repr✝ (@B✝) :=
+       ⟨instReprA.repr_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.repr true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving Repr
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving Repr
+end
+
+/-- info: A.a (B.b (A.leaf)) -/
+#guard_msgs in #eval A.a (.b .leaf)
+
+/-- info: B.b (A.a (B.leaf)) -/
+#guard_msgs in #eval B.b (.a .leaf)
+
+example : Repr A := instReprA
+example : Repr B := instReprB
+
+/-! Types from different mutual blocks in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+deriving instance Repr for C, E, D
+
+/-- info: C.c (D.d (C.leaf)) -/
+#guard_msgs in #eval C.c (.d .leaf)
+
+/-- info: D.d (C.c (D.leaf)) -/
+#guard_msgs in #eval D.d (.c .leaf)
+
+/-- info: E.e 3 -/
+#guard_msgs in #eval E.e 3
+
+example : Repr C := instReprC
+example : Repr D := instReprD
+example : Repr E := instReprE