diff --git a/tests/bench/simp_subexpr.lean b/tests/bench/simp_subexpr.lean new file mode 100644 index 0000000000..5d8a179179 --- /dev/null +++ b/tests/bench/simp_subexpr.lean @@ -0,0 +1,41 @@ +/-! +A micro-benchmark based on `simp_bubblesort`, designed specifically to use the subexpression +cache for rewriting in `simp`. +-/ + +inductive V where | a | b +open V + +axiom L : Type +axiom N : Type +axiom z : N +axiom s : N → N +axiom nil : L +axiom f : V → L → L +axiom iter : N → (L → L) → (L → L) +axiom combine : L → L → L + +axiom swap : f b (f a xs) = f a (f b xs) +axiom iter_zero : iter z g x = g x +axiom iter_succ : iter (s i) g x = iter i g (iter i g x) + +noncomputable def steps : N := s (s (s (s (s (s (s z)))))) + +set_option maxRecDepth 100000 +set_option profiler true + +syntax "tree(" num "," term "," term ")" : term + +macro_rules + | `(tree($n, $l, $r)) => + match n.getNat with + | 0 => `(combine $l $r) + | n + 1 => `(combine tree($(Lean.quote n), $l, $r) tree($(Lean.quote n), $r, $l)) + + +-- If run with -memoize or caching fails otherwise this regresses to timeout + +theorem normalized: + tree(0, (iter steps (f a) (iter steps (f b) nil)), (iter steps (f b) (iter steps (f a) nil))) = + tree(0, (iter steps (f b) (iter steps (f a) nil)), (iter steps (f a) (iter steps (f b) nil))) := +by simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 42396a3adb..599be10fd8 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -413,6 +413,12 @@ run_config: <<: *time cmd: lean simp_local.lean +- attributes: + description: simp_subexpr + tags: [fast, suite] + run_config: + <<: *time + cmd: lean simp_subexpr.lean - attributes: description: nat_repr tags: [fast, suite]