From c46ef56ac7dd7cce87f4cbe054b3042d6d802d49 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Jul 2022 13:10:04 -0700
Subject: [PATCH] perf: avoid blowup at `deriving Repr`

The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.

Closes #1365
---
 src/Init/Data/Repr.lean  | 45 +++++++++++++++++++++++++---------------
 tests/lean/run/1365.lean | 28 +++++++++++++++++++++++++
 2 files changed, 56 insertions(+), 17 deletions(-)
 create mode 100644 tests/lean/run/1365.lean

diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 8e10b7499c..334a92074c 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -64,15 +64,19 @@ instance [Repr α] : Repr (ULift.{v} α) where
 instance : Repr Unit where
   reprPrec _ _ := "()"
 
+protected def Option.repr [Repr α] : Option α → Nat → Format
+  | none,    _   => "none"
+  | some a, prec => Repr.addAppParen ("some " ++ reprArg a) prec
+
 instance [Repr α] : Repr (Option α) where
-  reprPrec
-    | none,    _   => "none"
-    | some a, prec => Repr.addAppParen ("some " ++ reprArg a) prec
+  reprPrec := Option.repr
+
+protected def Sum.repr [Repr α] [Repr β] : Sum α β → Nat → Format
+  | Sum.inl a, prec => Repr.addAppParen ("Sum.inl " ++ reprArg a) prec
+  | Sum.inr b, prec => Repr.addAppParen ("Sum.inr " ++ reprArg b) prec
 
 instance [Repr α] [Repr β] : Repr (Sum α β) where
-  reprPrec
-    | Sum.inl a, prec => Repr.addAppParen ("Sum.inl " ++ reprArg a) prec
-    | Sum.inr b, prec => Repr.addAppParen ("Sum.inr " ++ reprArg b) prec
+  reprPrec := Sum.repr
 
 class ReprTuple (α : Type u) where
   reprTuple : α → List Format → List Format
@@ -85,8 +89,11 @@ instance [Repr α] : ReprTuple α where
 instance [Repr α] [ReprTuple β] : ReprTuple (α × β) where
   reprTuple | (a, b), xs => reprTuple b (repr a :: xs)
 
+protected def Prod.repr [Repr α] [ReprTuple β] : α × β → Nat → Format
+  | (a, b), _ => Format.bracket "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")"
+
 instance [Repr α] [ReprTuple β] : Repr (α × β) where
-  reprPrec | (a, b), _ => Format.bracket "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")"
+  reprPrec := Prod.repr
 
 instance {β : α → Type v} [Repr α] [(x : α) → Repr (β x)] : Repr (Sigma β) where
   reprPrec | ⟨a, b⟩, _ => Format.bracket "⟨" (repr a ++ ", " ++ repr b) "⟩"
@@ -227,19 +234,23 @@ instance : Repr UInt64 where
 instance : Repr USize where
   reprPrec n _ := repr n.toNat
 
+protected def List.repr [Repr α] (a : List α) (n : Nat) : Format :=
+  let _ : ToFormat α := ⟨repr⟩
+  match a, n with
+  | [], _ => "[]"
+  | as, _ => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"
+
 instance [Repr α] : Repr (List α) where
-  reprPrec a n :=
-    let _ : ToFormat α := ⟨repr⟩
-    match a, n with
-    | [], _ => "[]"
-    | as, _ => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"
+  reprPrec := List.repr
+
+protected def List.repr' [Repr α] [ReprAtom α] (a : List α) (n : Nat) : Format :=
+  let _ : ToFormat α := ⟨repr⟩
+  match a, n with
+  | [], _ => "[]"
+  | as, _ => Format.bracketFill "[" (Format.joinSep as ("," ++ Format.line)) "]"
 
 instance [Repr α] [ReprAtom α] : Repr (List α) where
-  reprPrec a n :=
-    let _ : ToFormat α := ⟨repr⟩
-    match a, n with
-    | [], _ => "[]"
-    | as, _ => Format.bracketFill "[" (Format.joinSep as ("," ++ Format.line)) "]"
+  reprPrec := List.repr'
 
 instance : ReprAtom Bool   := ⟨⟩
 instance : ReprAtom Nat    := ⟨⟩
diff --git a/tests/lean/run/1365.lean b/tests/lean/run/1365.lean
new file mode 100644
index 0000000000..525606fd06
--- /dev/null
+++ b/tests/lean/run/1365.lean
@@ -0,0 +1,28 @@
+structure Foo where
+  a : Option Bool
+  b : Option Bool
+  c : Option Bool
+  d : Option Bool
+  e : Option Bool
+  f : Option Bool
+  g : Option Bool
+  h : Option Bool
+  i : Option Bool
+  j : Option Bool
+  k : Option Bool
+  l : Option Bool
+  m : Option Bool
+  n : Option Bool
+  o : Option Bool
+  p : Option Bool
+  q : Option Bool
+  r : Option Bool
+  s : Option Bool
+  t : Option Bool
+  u : Option Bool
+  v : Option Bool
+  w : Option Bool
+  x : Option Bool
+  y : Option Bool
+  z : Option Bool
+deriving Repr