From 0362acd5575854b43451b9669eb3c6037b123139 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 2 Oct 2023 10:32:50 +0200
Subject: [PATCH] perf: do not inhibit caching of default-level `match`
 reduction

---
 src/Lean/Meta/WHNF.lean                  | 11 ++++---
 tests/bench/reduceMatch.lean             | 40 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 ++++
 3 files changed, 53 insertions(+), 4 deletions(-)
 create mode 100644 tests/bench/reduceMatch.lean

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index d4cfa085d938..aa45bb1b0862 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -419,10 +419,13 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
      For example, `simp [Int.div]` will not unfold the application `Int.div 2 1` occuring in the target.
 
      TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
-  let mut transparency ← getTransparency
-  if transparency == TransparencyMode.reducible then
-    transparency := TransparencyMode.instances
-  withTransparency transparency <| withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+  if (← getTransparency) matches .instances | .reducible then
+    -- Also unfold some default-reducible constants; see `canUnfoldAtMatcher`
+    withTransparency .instances <| withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+      whnf e
+  else
+    -- Do NOT use `canUnfoldAtMatcher` here as it does not affect all/default reducibility and inhibits caching (#2564).
+    -- In the future, we want to work on better reduction strategies that do not require caching.
     whnf e
 
 def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
diff --git a/tests/bench/reduceMatch.lean b/tests/bench/reduceMatch.lean
new file mode 100644
index 000000000000..8fc0af9ee6d8
--- /dev/null
+++ b/tests/bench/reduceMatch.lean
@@ -0,0 +1,40 @@
+import Lean
+
+/-!
+  #2564. `match` reduction currently has some special cases.
+  When combined with nonlinear functions like `List.insert` below,
+  it is crucial to preserve sharing during reduction. -/
+
+section decidability_instances
+
+variable {α : Type} {p : α → Prop} [DecidablePred p]
+
+instance decidableBex : ∀ (l : List α), Decidable (∃ x, x ∈ l → p x)
+  | []    => isFalse sorry
+  | x::xs =>
+    match ‹DecidablePred p› x with
+    | isTrue h₁ => isTrue sorry
+    | isFalse h₁ => match decidableBex xs with
+      | isTrue h₂  => isTrue sorry
+      | isFalse h₂ => isFalse sorry
+
+instance decidableBall (l : List α) : Decidable (∀ x, x ∈ l → p x) :=
+  match (inferInstance : Decidable <| ∃ x, x ∈ l → ¬ p x) with
+  | isFalse h => isTrue $ fun x hx => match ‹DecidablePred p› x with
+    | isTrue h' => h'
+    | isFalse h' => False.elim $ h sorry
+  | isTrue h => isFalse sorry
+
+end decidability_instances
+
+@[inline] protected def List.insert {α : Type} [DecidableEq α] (a : α) (l : List α) : List α :=
+  if a ∈ l then l else a :: l
+
+def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0, 1, 1]) <|
+  List.insert ([1, 0, 0, 1]) <| List.insert ([1, 1, 1, 0]) <| List.insert ([1, 0, 0, 0]) <|
+  List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] []
+
+#eval show Lean.Elab.Command.CommandElabM _ from
+  for _ in [0:10] do
+    Lean.Elab.Command.elabCommand (←
+      `(example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by decide))
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index e70cbdab41ba..6cc0d1783d0f 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -282,6 +282,12 @@
     cmd: ./rbmap_library.lean.out 2000000
   build_config:
     cmd: ./compile.sh rbmap_library.lean
+- attributes:
+    description: reduceMatch
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean reduceMatch.lean
 - attributes:
     description: unionfind
     tags: [fast, suite]