From 8ef742647e6996011ba2f34de7459ce86fc54cf9 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 16 Nov 2025 12:20:31 +0100
Subject: [PATCH] test: benchmark for large partial match (#11199)

Creates an inductive data type with 100 constructors, and a function
that does
matches on half of its constructors, with a catch-all for the other
half, and generates the splitter.

Related to #11183.
---
 tests/bench/big_match_partial.lean       | 66 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 +++
 2 files changed, 72 insertions(+)
 create mode 100644 tests/bench/big_match_partial.lean

diff --git a/tests/bench/big_match_partial.lean b/tests/bench/big_match_partial.lean
new file mode 100644
index 0000000000..b4d04b5b17
--- /dev/null
+++ b/tests/bench/big_match_partial.lean
@@ -0,0 +1,66 @@
+import Lean
+
+/-!
+Creates an inductive data type with n constructors, and a function that does
+matches on half of its constructors, with a catch-all for the other hal.
+-/
+
+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/2] do
+      let con1 := mkQualCtor cIdx1
+      let case ← `(matchAltExpr| | .$con1:ident n =>n)
+      cases := cases.push case
+    cases := cases.push (← `(matchAltExpr| | _ => 0))
+    let fdecl ←
+        `(def $f:ident (x : $t:ident Nat) : Nat :=
+            match x with
+            $cases:matchAlt*
+        )
+    let stx ← `(
+      $idecl:command
+      $fdecl:command
+      )
+    -- logInfo stx
+    elabCommand stx
+  | _ =>
+    throwIllFormedSyntax
+
+#test_gen T f 100
+
+#time example := f.match_1.splitter
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 31c473af20..c080e1ab9c 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -441,6 +441,12 @@
   run_config:
     <<: *time
     cmd: lean big_match.lean
+- attributes:
+    description: big_match_partial
+    tags: [other]
+  run_config:
+    <<: *time
+    cmd: lean big_match_partial.lean
 - attributes:
     description: big_beq
     tags: [other]