From d179d6c8d792e7aaad30be8a64a29822d3de9e53 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 23 Feb 2024 16:38:46 -0800
Subject: [PATCH] perf: bitvector literals in match patterns (#3485)

---
 src/Lean/Meta/WHNF.lean              |  1 +
 tests/lean/run/bv_math_lit_perf.lean | 22 ++++++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 tests/lean/run/bv_math_lit_perf.lean

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a8704f54ba..80fa7bdfd3 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -450,6 +450,7 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
        || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
        || info.name == ``String.decEq || info.name == ``List.hasDecEq
        || info.name == ``Fin.ofNat
+       || info.name == ``Fin.ofNat' -- It is used to define `BitVec` literals
        || info.name == ``UInt8.ofNat  || info.name == ``UInt8.decEq
        || info.name == ``UInt16.ofNat || info.name == ``UInt16.decEq
        || info.name == ``UInt32.ofNat || info.name == ``UInt32.decEq
diff --git a/tests/lean/run/bv_math_lit_perf.lean b/tests/lean/run/bv_math_lit_perf.lean
new file mode 100644
index 0000000000..308d5e226c
--- /dev/null
+++ b/tests/lean/run/bv_math_lit_perf.lean
@@ -0,0 +1,22 @@
+open BitVec
+
+def f (x : BitVec 32) : Nat :=
+  match x with
+  | 10#32  => 0
+  | 100#32 => 2
+  | 200#32 => 3
+  | 300#32 => 4
+  | 400#32 => 5
+  | 500#32 => 6
+  | 600#32 => 7
+  | 700#32 => 8
+  | 800#32 => 9
+  | 900#32 => 10
+  | 910#32 => 11
+  | 920#32 => 12
+  | _      => 1000
+
+set_option maxHeartbeats 500
+example : f 500#32 = x := by
+  simp [f]
+  sorry