mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
ee293de982
This PR adds tests and a benchmark exercising `instantiateMVars` on metavariable assignment graphs with nested delayed assignments, in preparation for optimizing the delayed mvar resolution path. - `tests/elab/instantiateMVarsShadow.lean`: Two test cases for correctness when the same fvar is bound to different values at different scope levels (fvar shadowing and late-bind patterns). A buggy cache could return a stale result from one scope level in another. - `tests/elab/instantiateMVarsSharing.lean`: Verifies correct resolution and object sharing on a graph with nested delayed mvars producing `∀ s, (s = s → (s = s) ∧ (s = s)) ∧ (s = s)`. - `tests/elab_bench/delayed_assign.lean`: Constructs an O(n²) delayed mvar graph (n=700) and measures `instantiateMVars` resolution time, calibrated to ~1s total elaboration. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
53 lines
1.7 KiB
Lean4
53 lines
1.7 KiB
Lean4
import Lean
|
|
|
|
/-!
|
|
This benchmark exercises `instantiateMVars` sharing on an exponential DAG
|
|
of delayed metavariable assignments.
|
|
|
|
We build a chain of n delayed mvars:
|
|
?d₀ delayed [x] := x
|
|
?dᵢ delayed [x] := Nat.add (?dᵢ₋₁ x) (?dᵢ₋₁ x)
|
|
?root := fun (a : Nat) => ?dₙ a
|
|
|
|
Without sharing, instantiating ?root would produce 2ⁿ leaf nodes.
|
|
With sharing, it produces O(n) unique subexpressions.
|
|
-/
|
|
|
|
set_option maxHeartbeats 40000000
|
|
|
|
open Lean Meta
|
|
|
|
def mkSharingBench (n : Nat) : MetaM Expr := do
|
|
let nat := mkConst ``Nat
|
|
withLocalDeclD `x nat fun x_fvar => do
|
|
-- d₀ delayed [x] := x
|
|
let d₀Inner ← mkFreshExprMVar nat
|
|
d₀Inner.mvarId!.assign x_fvar
|
|
let d₀Ty ← mkArrow nat nat
|
|
let d₀ ← mkFreshExprMVar d₀Ty (kind := .syntheticOpaque)
|
|
assignDelayedMVar d₀.mvarId! #[x_fvar] d₀Inner.mvarId!
|
|
|
|
let mut prev := d₀
|
|
for _ in [:n] do
|
|
let app := mkApp prev x_fvar -- shared subexpression
|
|
let inner ← mkFreshExprMVar nat
|
|
inner.mvarId!.assign (mkApp2 (mkConst ``Nat.add) app app)
|
|
let dTy ← mkArrow nat nat
|
|
let d ← mkFreshExprMVar dTy (kind := .syntheticOpaque)
|
|
assignDelayedMVar d.mvarId! #[x_fvar] inner.mvarId!
|
|
prev := d
|
|
|
|
-- root := fun a => dₙ a
|
|
let rootTy ← mkArrow nat nat
|
|
let root ← mkFreshExprMVar rootTy
|
|
root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp prev (.bvar 0)))
|
|
return root
|
|
|
|
-- n=19 is calibrated to take roughly 1s total elaboration time.
|
|
-- Use a small n unless TEST_BENCH=1, so that the test suite runs quickly.
|
|
run_meta do
|
|
let bench := (← IO.getEnv "TEST_BENCH") == some "1"
|
|
let n := if bench then 19 else 10
|
|
let root ← mkSharingBench n
|
|
discard <| instantiateMVars root
|