test: add instantiateMVars tests and benchmark for delayed assignments (#12808)
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>
This commit is contained in:
Joachim Breitner
GitHub
parent
a165292462
commit
ee293de982
5 changed files with 446 additions and 0 deletions
86
tests/elab/instantiateMVarsCrossScope.lean
Normal file
86
tests/elab/instantiateMVarsCrossScope.lean
Normal file
|
|
@ -0,0 +1,86 @@
|
|||
import Lean
|
||||
|
||||
open Lean Meta
|
||||
|
||||
/-!
|
||||
Test: cross-scope sharing in `instantiateMVars` with nested delayed mvars.
|
||||
|
||||
A shared expression `succ_x := Nat.succ x_fvar` is visited at scope 1
|
||||
(as d2's argument, before scope 2 is pushed) and then at scope 2
|
||||
(inside d2's pending value). Since the result only depends on scope 1,
|
||||
which hasn't changed, both visits should produce the same object.
|
||||
|
||||
?root := fun (a : Nat) => ?d1 a
|
||||
?d1 delayed [x] := ?body
|
||||
?body := ?d2 succ_x ← succ_x visited at scope 1 as d2's arg
|
||||
?d2 delayed [z] := ?inner
|
||||
?inner := Prod.mk z succ_x ← z = R1, succ_x visited at scope 2
|
||||
|
||||
The ordering guarantee comes from the delayed mvar resolution control
|
||||
flow: arguments are visited before pushing the new scope, the pending
|
||||
value is visited after. This does not depend on the order in which
|
||||
application arguments are traversed.
|
||||
|
||||
Expected result: fun (a : Nat) => (Nat.succ a, Nat.succ a)
|
||||
|
||||
Both `Nat.succ a` subexpressions in the result should be the same
|
||||
object (ptrEq), since the shared input `succ_x` produces the same
|
||||
result at both scope levels.
|
||||
-/
|
||||
|
||||
private def mkCrossScopeTest : MetaM Expr := do
|
||||
let nat := mkConst ``Nat
|
||||
withLocalDeclD `x nat fun x_fvar =>
|
||||
withLocalDeclD `z nat fun z_fvar => do
|
||||
let succ_x := mkApp (mkConst ``Nat.succ) x_fvar
|
||||
|
||||
-- ?inner := Prod.mk z succ_x
|
||||
let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat
|
||||
let inner ← mkFreshExprMVar pairTy
|
||||
inner.mvarId!.assign
|
||||
(mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat z_fvar succ_x)
|
||||
|
||||
-- ?d2 delayed [z] := ?inner, takes one Nat arg
|
||||
let d2_ty ← mkArrow nat pairTy
|
||||
let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d2.mvarId! #[z_fvar] inner.mvarId!
|
||||
|
||||
-- ?body := ?d2 succ_x
|
||||
let body ← mkFreshExprMVar pairTy
|
||||
body.mvarId!.assign (mkApp d2 succ_x)
|
||||
|
||||
-- ?d1 delayed [x] := ?body
|
||||
let d1_ty ← mkArrow nat pairTy
|
||||
let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId!
|
||||
|
||||
-- ?root := fun (a : Nat) => ?d1 a
|
||||
let rootTy ← mkArrow nat pairTy
|
||||
let root ← mkFreshExprMVar rootTy
|
||||
root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0)))
|
||||
return root
|
||||
|
||||
-- Expected: fun (a : Nat) => (Nat.succ a, Nat.succ a)
|
||||
private def mkExpected : Expr :=
|
||||
let nat := mkConst ``Nat
|
||||
let succ_a := mkApp (mkConst ``Nat.succ) (.bvar 0)
|
||||
let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_a succ_a
|
||||
Lean.mkLambda `a .default nat body
|
||||
|
||||
-- Extract the two components from the result
|
||||
-- Result shape: fun (a : Nat) => @Prod.mk Nat Nat fst snd
|
||||
private def extractComponents (e : Expr) : Expr × Expr :=
|
||||
let body := e.bindingBody!
|
||||
let snd := body.appArg!
|
||||
let fst := body.appFn!.appArg!
|
||||
(fst, snd)
|
||||
|
||||
run_meta do
|
||||
let root ← mkCrossScopeTest
|
||||
let expected := mkExpected
|
||||
let result ← instantiateMVars root
|
||||
unless result == expected do
|
||||
throwError "cross-scope: wrong result, got {result}"
|
||||
let (fst, snd) := extractComponents result
|
||||
unless unsafe ptrEq fst snd do
|
||||
throwError "cross-scope: fst and snd are not shared (not ptrEq)"
|
||||
152
tests/elab/instantiateMVarsShadow.lean
Normal file
152
tests/elab/instantiateMVarsShadow.lean
Normal file
|
|
@ -0,0 +1,152 @@
|
|||
import Lean
|
||||
|
||||
open Lean Meta
|
||||
|
||||
/-!
|
||||
Test: fvar shadowing in nested delayed mvars.
|
||||
|
||||
Two delayed mvars bind the same fvar `x_fvar` to different values.
|
||||
A shared subexpression `succ_x := Nat.succ x_fvar` appears in both scopes.
|
||||
|
||||
?root := fun (a : Nat) => ?d1 a
|
||||
?d1 delayed [x_fvar] := ?body
|
||||
?body := Prod.mk succ_x (?d2 succ_x) ← succ_x is shared
|
||||
?d2 delayed [x_fvar] := ?inner
|
||||
?inner := succ_x ← same shared object
|
||||
|
||||
Expected result:
|
||||
fun (a : Nat) => (Nat.succ a, Nat.succ (Nat.succ a))
|
||||
|
||||
When resolving ?d1 with arg `a`:
|
||||
- succ_x with x_fvar → a gives Nat.succ a (first component)
|
||||
- ?d2 gets arg (Nat.succ a), so x_fvar → Nat.succ a
|
||||
succ_x with x_fvar → Nat.succ a gives Nat.succ (Nat.succ a) (second component)
|
||||
|
||||
A buggy cache could return the cached scope-1 result (Nat.succ a) for the scope-2
|
||||
visit, producing (Nat.succ a, Nat.succ a) instead.
|
||||
-/
|
||||
|
||||
private def mkShadowTest : MetaM Expr := do
|
||||
let nat := mkConst ``Nat
|
||||
withLocalDeclD `x nat fun x_fvar => do
|
||||
-- shared object referencing x_fvar
|
||||
let succ_x := mkApp (mkConst ``Nat.succ) x_fvar
|
||||
|
||||
-- ?inner := succ_x
|
||||
let inner ← mkFreshExprMVar nat
|
||||
inner.mvarId!.assign succ_x
|
||||
|
||||
-- ?d2 delayed [x_fvar] := ?inner
|
||||
let d2_ty ← mkArrow nat nat
|
||||
let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d2.mvarId! #[x_fvar] inner.mvarId!
|
||||
|
||||
-- ?body := ⟨succ_x, ?d2 succ_x⟩
|
||||
let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat
|
||||
let body ← mkFreshExprMVar pairTy
|
||||
body.mvarId!.assign
|
||||
(mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat
|
||||
succ_x (mkApp d2 succ_x))
|
||||
|
||||
-- ?d1 delayed [x_fvar] := ?body
|
||||
let d1_ty ← mkArrow nat pairTy
|
||||
let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId!
|
||||
|
||||
-- ?root := fun (a : Nat) => ?d1 a
|
||||
let rootTy ← mkArrow nat pairTy
|
||||
let root ← mkFreshExprMVar rootTy
|
||||
root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0)))
|
||||
return root
|
||||
|
||||
-- Expected: fun (a : Nat) => (Nat.succ a, Nat.succ (Nat.succ a))
|
||||
private def mkExpected : Expr :=
|
||||
let nat := mkConst ``Nat
|
||||
let succ := mkConst ``Nat.succ
|
||||
-- #0 refers to the lambda-bound `a`
|
||||
let succ_a := mkApp succ (.bvar 0)
|
||||
let succ_succ_a := mkApp succ succ_a
|
||||
let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_a succ_succ_a
|
||||
Lean.mkLambda `a .default nat body
|
||||
|
||||
run_meta do
|
||||
let root ← mkShadowTest
|
||||
let result ← instantiateMVars root
|
||||
let expected := mkExpected
|
||||
unless result == expected do
|
||||
throwError "shadow: expected\n {expected}\ngot\n {result}"
|
||||
|
||||
/-!
|
||||
Test: an fvar first seen unsubstituted, then substituted at a higher scope.
|
||||
|
||||
A shared subexpression `succ_y := Nat.succ y_fvar` is used both:
|
||||
- directly in the body of d1 (where y is NOT bound), and
|
||||
- inside d2's pending value (where y IS bound).
|
||||
|
||||
?root := fun (a : Nat) => ?d1 a
|
||||
?d1 delayed [x] := ?body
|
||||
?body := Prod.mk succ_y (?d2 succ_y) ← succ_y shared
|
||||
?d2 delayed [y] := ?inner ← y is NOW bound
|
||||
?inner := succ_y ← same shared object
|
||||
|
||||
Expected result:
|
||||
fun (a : Nat) => (Nat.succ y_fvar, Nat.succ (Nat.succ y_fvar))
|
||||
|
||||
At scope 1 (d1), x → a. Visit body:
|
||||
- succ_y: y is NOT in fvar_subst. Result is succ_y unchanged.
|
||||
- ?d2 succ_y: arg succ_y visited → succ_y. Then d2 at scope 2 with y → succ_y.
|
||||
- Visit ?inner = succ_y. y IS in fvar_subst → Nat.succ succ_y = Nat.succ (Nat.succ y_fvar).
|
||||
|
||||
A buggy cache would return the scope-1 result (succ_y unchanged) at scope 2,
|
||||
producing (Nat.succ y_fvar, Nat.succ y_fvar) instead.
|
||||
-/
|
||||
|
||||
private def mkLateBindTest : MetaM (Expr × Expr) := do
|
||||
let nat := mkConst ``Nat
|
||||
withLocalDeclD `x nat fun x_fvar =>
|
||||
withLocalDeclD `y nat fun y_fvar => do
|
||||
-- shared object referencing y_fvar (NOT x_fvar)
|
||||
let succ_y := mkApp (mkConst ``Nat.succ) y_fvar
|
||||
|
||||
-- ?inner := succ_y
|
||||
let inner ← mkFreshExprMVar nat
|
||||
inner.mvarId!.assign succ_y
|
||||
|
||||
-- ?d2 delayed [y_fvar] := ?inner
|
||||
let d2_ty ← mkArrow nat nat
|
||||
let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d2.mvarId! #[y_fvar] inner.mvarId!
|
||||
|
||||
-- ?body := ⟨succ_y, ?d2 succ_y⟩
|
||||
let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat
|
||||
let body ← mkFreshExprMVar pairTy
|
||||
body.mvarId!.assign
|
||||
(mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat
|
||||
succ_y (mkApp d2 succ_y))
|
||||
|
||||
-- ?d1 delayed [x_fvar] := ?body
|
||||
let d1_ty ← mkArrow nat pairTy
|
||||
let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque)
|
||||
assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId!
|
||||
|
||||
-- ?root := fun (a : Nat) => ?d1 a
|
||||
let rootTy ← mkArrow nat pairTy
|
||||
let root ← mkFreshExprMVar rootTy
|
||||
root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0)))
|
||||
return (root, y_fvar)
|
||||
|
||||
-- Expected: fun (a : Nat) => (Nat.succ y_fvar, Nat.succ (Nat.succ y_fvar))
|
||||
private def mkExpectedLateBind (y_fvar : Expr) : Expr :=
|
||||
let nat := mkConst ``Nat
|
||||
let succ := mkConst ``Nat.succ
|
||||
let succ_y := mkApp succ y_fvar
|
||||
let succ_succ_y := mkApp succ succ_y
|
||||
let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_y succ_succ_y
|
||||
Lean.mkLambda `a .default nat body
|
||||
|
||||
run_meta do
|
||||
let (root, y_fvar) ← mkLateBindTest
|
||||
let result ← instantiateMVars root
|
||||
let expected := mkExpectedLateBind y_fvar
|
||||
unless result == expected do
|
||||
throwError "late-bind: expected\n {expected}\ngot\n {result}"
|
||||
101
tests/elab/instantiateMVarsSharing.lean
Normal file
101
tests/elab/instantiateMVarsSharing.lean
Normal file
|
|
@ -0,0 +1,101 @@
|
|||
import Lean
|
||||
|
||||
open Lean Meta
|
||||
|
||||
/-!
|
||||
Test for sharing in `instantiateMVars` with delayed mvar assignments.
|
||||
|
||||
We construct the metavariable assignment graph for the goal
|
||||
`∀ s, (s = s → (s = s) ∧ (s = s)) ∧ (s = s)`:
|
||||
|
||||
?root := fun (s : Nat) => ?rootAux #0
|
||||
?rootAux delayed [s_fvar] := ?body
|
||||
?body := @And.intro leftTy rightTy ?left right
|
||||
?left := fun (h : eq_ss) => ?leftAux #0
|
||||
?leftAux delayed [h_fvar] := ?inner
|
||||
?inner := @And.intro eq_ss eq_ss h_fvar h_fvar
|
||||
|
||||
where
|
||||
|
||||
eq_ss := @Eq Nat s_fvar s_fvar ← single shared object
|
||||
andTy := And eq_ss eq_ss ← contains eq_ss
|
||||
leftTy := eq_ss → andTy ← forallE body contains eq_ss
|
||||
rightTy := eq_ss
|
||||
right := @Eq.refl Nat s_fvar
|
||||
|
||||
After instantiation, the shared `eq_ss` input should produce shared results
|
||||
at each binding depth:
|
||||
- At depth 1: `@Eq Nat #0 #0` (used as rightTy, leftTy.domain, left.domain)
|
||||
- At depth 2: `@Eq Nat #1 #1` (used as And args in leftTy body and And.intro
|
||||
type args in inner body)
|
||||
-/
|
||||
|
||||
private def mkTestRoot : MetaM Expr := do
|
||||
let nat := mkConst ``Nat
|
||||
withLocalDeclD `s nat fun s_fvar => do
|
||||
let eq_ss ← mkEq s_fvar s_fvar -- shared object
|
||||
|
||||
let andTy := mkApp2 (mkConst ``And) eq_ss eq_ss -- (s=s) ∧ (s=s)
|
||||
let leftTy ← mkArrow eq_ss andTy -- s=s → (s=s) ∧ (s=s)
|
||||
let rightTy := eq_ss -- s=s
|
||||
let bodyTy := mkApp2 (mkConst ``And) leftTy rightTy
|
||||
|
||||
let body ← mkFreshExprMVar bodyTy
|
||||
let left ← mkFreshExprMVar leftTy
|
||||
|
||||
withLocalDeclD `h eq_ss fun h_fvar => do
|
||||
-- ?inner : (s=s) ∧ (s=s), proved by And.intro eq_ss eq_ss h h
|
||||
let inner ← mkFreshExprMVar andTy
|
||||
let leftDecl ← left.mvarId!.getDecl
|
||||
let leftAux ← mkFreshExprMVarAt leftDecl.lctx leftDecl.localInstances
|
||||
leftDecl.type .syntheticOpaque
|
||||
assignDelayedMVar leftAux.mvarId! #[h_fvar] inner.mvarId!
|
||||
left.mvarId!.assign (Lean.mkLambda `h .default eq_ss (mkApp leftAux (.bvar 0)))
|
||||
inner.mvarId!.assign (mkApp4 (mkConst ``And.intro) eq_ss eq_ss h_fvar h_fvar)
|
||||
|
||||
let right := mkApp2 (mkConst ``Eq.refl [1]) nat s_fvar
|
||||
body.mvarId!.assign (mkApp4 (mkConst ``And.intro) leftTy rightTy left right)
|
||||
|
||||
let rootTy ← mkForallFVars #[s_fvar] bodyTy
|
||||
let root ← mkFreshExprMVar rootTy
|
||||
let rootDecl ← root.mvarId!.getDecl
|
||||
let rootAux ← mkFreshExprMVarAt rootDecl.lctx rootDecl.localInstances
|
||||
rootDecl.type .syntheticOpaque
|
||||
assignDelayedMVar rootAux.mvarId! #[s_fvar] body.mvarId!
|
||||
root.mvarId!.assign (Lean.mkLambda `s .default nat (mkApp rootAux (.bvar 0)))
|
||||
return root
|
||||
|
||||
-- Instantiate and verify sharing
|
||||
run_meta do
|
||||
let root ← mkTestRoot
|
||||
let result ← instantiateMVars root
|
||||
|
||||
-- Result: fun (s : Nat) => @And.intro leftTy rightTy left right
|
||||
let outerBody := result.bindingBody!
|
||||
let rightTy := outerBody.appFn!.appFn!.appArg!
|
||||
let leftTy := outerBody.appFn!.appFn!.appFn!.appArg!
|
||||
let left := outerBody.appFn!.appArg!
|
||||
|
||||
-- At depth 1: rightTy, leftTy.domain, and left.domain are all
|
||||
-- instantiations of the shared `eq_ss` at the same depth → ptrEq.
|
||||
unless unsafe ptrEq rightTy leftTy.bindingDomain! do
|
||||
throwError "sharing: rightTy and leftTy.domain are not ptrEq"
|
||||
unless unsafe ptrEq rightTy left.bindingDomain! do
|
||||
throwError "sharing: rightTy and left.domain are not ptrEq"
|
||||
|
||||
-- At depth 2: the two eq_ss args inside `And` in leftTy's body → ptrEq.
|
||||
let andInLeftTyBody := leftTy.bindingBody!
|
||||
unless unsafe ptrEq andInLeftTyBody.appFn!.appArg! andInLeftTyBody.appArg! do
|
||||
throwError "sharing: And args in leftTy body are not ptrEq"
|
||||
|
||||
-- At depth 2: the two type args inside `And.intro` in the inner body → ptrEq.
|
||||
let innerBody := left.bindingBody!
|
||||
let innerTyArg1 := innerBody.appFn!.appFn!.appFn!.appArg!
|
||||
let innerTyArg2 := innerBody.appFn!.appFn!.appArg!
|
||||
unless unsafe ptrEq innerTyArg1 innerTyArg2 do
|
||||
throwError "sharing: And.intro type args in inner body are not ptrEq"
|
||||
|
||||
-- Cross-expression: depth-2 eq_ss from leftTy body and inner body should
|
||||
-- be the same object (same shared input at the same binding depth).
|
||||
unless unsafe ptrEq andInLeftTyBody.appArg! innerTyArg1 do
|
||||
throwError "sharing: eq_ss at depth 2 not shared across leftTy and inner"
|
||||
55
tests/elab_bench/delayed_assign.lean
Normal file
55
tests/elab_bench/delayed_assign.lean
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
import Lean
|
||||
|
||||
/-!
|
||||
This benchmark exercises `instantiateMVars` on a large metavariable
|
||||
assignment graph with many nested delayed assignments.
|
||||
|
||||
We construct a goal of the form
|
||||
`∀ x₁ … xₙ, ((0 ≤ x₁) ∧ … ∧ True) ∧ … ∧ ((0 ≤ xₙ) ∧ … ∧ True)`
|
||||
as a single mvar, solve it (creating O(n²) delayed mvars), and then
|
||||
call `instantiateMVars` to fully resolve the result.
|
||||
-/
|
||||
|
||||
set_option maxHeartbeats 40000000
|
||||
|
||||
open Lean Meta
|
||||
|
||||
def mkLE (i : Nat) : Expr :=
|
||||
mkNatLE (mkNatLit 0) (mkBVar i)
|
||||
|
||||
partial def solve (mvarId : MVarId) : MetaM Unit := do
|
||||
let type ← instantiateMVars (← mvarId.getType)
|
||||
if type.isForall then
|
||||
let (_, mvarId) ← mvarId.intro1
|
||||
solve mvarId
|
||||
else if type.isAppOf ``And then
|
||||
let [mvarId₁, mvarId₂] ← mvarId.applyConst ``And.intro | failure
|
||||
solve mvarId₁
|
||||
solve mvarId₂
|
||||
else if type.isAppOf ``LE.le then
|
||||
let [] ← mvarId.applyConst ``Nat.zero_le | failure
|
||||
else
|
||||
let [] ← mvarId.applyConst ``True.intro | failure
|
||||
|
||||
def mkBench (n : Nat) : MetaM MVarId := do
|
||||
let type := mkType n
|
||||
return (← mkFreshExprSyntheticOpaqueMVar type).mvarId!
|
||||
where
|
||||
mkResultType (i : Nat) : Expr :=
|
||||
match i with
|
||||
| 0 => mkConst ``True
|
||||
| i+1 => mkAnd (mkLE i) (mkResultType i)
|
||||
|
||||
mkType (i : Nat) : Expr :=
|
||||
match i with
|
||||
| 0 => mkResultType n
|
||||
| i+1 => .forallE `x Nat.mkType (mkAnd (mkType i) (mkLE (n - i - 1))) .default
|
||||
|
||||
-- n=200 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 200 else 50
|
||||
let mvarId ← mkBench n
|
||||
solve mvarId
|
||||
discard <| instantiateMVars (mkMVar mvarId)
|
||||
52
tests/elab_bench/delayed_sharing.lean
Normal file
52
tests/elab_bench/delayed_sharing.lean
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
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
|
||||
Loading…
Add table
Reference in a new issue