perf: scale Expr.replace cache with input size

[Kha]

When the cache is much bigger than the traversed term, we're spending most of the time with allocating and deallocating it. This change speeds up mathlib4 cumulative CPU time by ~20% and TC inference time by ~32%. In particular, instantiateLevelParams falls in one arbitrarily selected test case (Mathlib.Algebra.Order.Ring.Defs) from 12.7% cumulative time share to 3.4%.

Other approaches are conceivable such as doing no caching at all below a certain term depth, but this one does not introduce any new magic numbers and the potential for further savings in this part is unclear.

[Kha]

!bench

[Kha]

In particular, this should mostly obsolete the need for #2028

[leanprover-bot]

Here are the benchmark results for commit 86132a2.
There were significant changes against commit 96aa021:

  Benchmark                  Metric                  Change
  =====================================================================
+ stdlib                     attribute application    -4.7%   (-29.4 σ)
+ stdlib                     instructions            -15.0% (-4757.7 σ)
+ stdlib                     tactic execution        -18.5%  (-332.0 σ)
+ stdlib                     task-clock               -6.9%  (-166.0 σ)
+ stdlib                     type checking            -1.5%   (-31.4 σ)
+ stdlib                     wall-clock               -6.9%  (-135.7 σ)
+ tests/bench/ interpreted   instructions             -3.1% (-7895.6 σ)
+ workspaceSymbols           task-clock               -3.4%   (-10.7 σ)
+ workspaceSymbols           wall-clock               -3.4%   (-10.7 σ)