From 417031fc173c8d292ac9e9d210a39217de909334 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 1 Aug 2025 17:25:07 +0200
Subject: [PATCH] chore: large match statement benchmark (#9665)

This PR adds a benchmark with a large, two-level, not-overlapping match
statement, including the splitter generation.
---
 tests/bench/big_match.lean               | 67 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 +++
 2 files changed, 73 insertions(+)
 create mode 100644 tests/bench/big_match.lean

diff --git a/tests/bench/big_match.lean b/tests/bench/big_match.lean
new file mode 100644
index 0000000000..df7ebc2ced
--- /dev/null
+++ b/tests/bench/big_match.lean
@@ -0,0 +1,67 @@
+import Lean
+
+/-!
+Creates an inductive data type with n constructors, and a function that does
+a n-times-n nested non-overlapping match on it.
+-/
+
+set_option Elab.async false
+
+open Lean Elab
+open Elab.Command (CommandElab CommandElabM elabCommand)
+open Parser.Command
+open Parser.Term
+
+-- Create a name.
+def strName (s : String) : Name := Name.anonymous |>.str s
+
+def mkBaseCtorStr (idx : Nat) : String := s!"base{idx}"
+def mkBaseCtorIdent (idx : Nat) : Ident :=
+  mkIdent <| strName <| mkBaseCtorStr idx
+def mkQualCtor (idx : Nat) : Ident :=
+  mkIdent <| Name.anonymous |>.str (mkBaseCtorStr idx)
+
+/--
+`#test_gen name dt ccnt icnt` creates
+`dt` mutually inductive types where each type has `ccnt` nullary constructors
+and `icnt` unary recursive constructors
+-/
+syntax (name := testGen) (docComment)? "#test_gen" ident ident num : command -- declare the syntax
+
+@[command_elab testGen]
+def testGenImpl: CommandElab := fun stx => do
+  match stx with
+  | `(#test_gen $t $f $con_count) =>
+    let con_count := con_count.getNat
+    let cons ← Array.ofFnM (n := con_count) fun cIdx =>
+      let con := mkBaseCtorIdent cIdx
+      `(ctor| | $con:ident : α → $t:ident α )
+    let idecl ←
+      -- Create constant case definitions
+      `(inductive $t:ident α where
+        $cons:ctor*
+      )
+    let mut cases : TSyntaxArray `Lean.Parser.Term.matchAlt := #[]
+    for cIdx1 in [:con_count] do
+      let con1 := mkQualCtor cIdx1
+      for cIdx2 in [:con_count] do
+        let con2 := mkQualCtor cIdx2
+        let case ← `(matchAltExpr| | .$con1:ident (.$con2:ident n) =>n)
+        cases := cases.push case
+    let fdecl ←
+        `(def $f:ident (x : $t:ident ($t:ident Nat)) : Nat :=
+            match x with
+            $cases:matchAlt*
+        )
+    let stx ← `(
+      $idecl:command
+      $fdecl:command
+      )
+    -- logInfo stx
+    elabCommand stx
+  | _ =>
+    throwIllFormedSyntax
+
+#test_gen T f 12
+
+#time example := f.match_1.splitter
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 62f882459a..180ffc370f 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -433,6 +433,12 @@
   run_config:
     <<: *time
     cmd: lean mut_rec_wf.lean
+- attributes:
+    description: big_match
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean big_match.lean
 - attributes:
     description: nat_repr
     tags: [fast, suite]