mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
2e06fb5008
This PR replaces the default `instantiateMVars` implementation with a two-pass variant that fuses fvar substitution into the traversal, avoiding separate `replace_fvars` calls for delayed-assigned MVars and preserving sharing. The old single-pass implementation is removed entirely. The previous implementation had quadratic complexity when instantiating expressions with long chains of nested delayed-assigned MVars. Such chains arise naturally from repeated `intro`/`apply` tactic sequences, where each step creates a new delayed assignment wrapping the previous one. The new two-pass approach resolves the entire chain in a single traversal with a fused fvar substitution, reducing this to linear complexity. ### Terminology (used in this PR and in the source) * **Direct MVar**: an MVar that is not delayed-assigned. * **Pending MVar**: the direct MVar stored in a `DelayedMetavarAssignment`. * **Assigned MVar**: a direct MVar with an assignment, or a delayed-assigned MVar with an assigned pending MVar. * **MVar DAG**: the directed acyclic graph of MVars reachable from the expression. * **Resolvable MVar**: an MVar where all MVars reachable from it (including itself) are assigned. * **Updateable MVar**: an assigned direct MVar, or a delayed-assigned MVar that is resolvable but not reachable from any other resolvable delayed-assigned MVar. In the MVar DAG, the updateable delayed-assigned MVars form a cut (the **updateable-MVar cut**) with only assigned MVars behind it and no resolvable delayed-assigned MVars before it. ### Two-pass architecture **Pass 1** (`instantiate_direct_fn`): Traverses all MVars and expressions reachable from the initial expression and instantiates all updateable direct MVars (updating their assignment with the result), instantiates all level MVars, and determines if there are any updateable delayed-assigned MVars. **Pass 2** (`instantiate_delayed_fn`): Only run if pass 1 found updateable delayed-assigned MVars. Has an **outer** and an **inner** mode, depending on whether it has crossed the updateable-MVar cut. In outer mode (empty fvar substitution), all MVars are either unassigned direct MVars (left alone), non-updateable delayed-assigned MVars (pending MVar traversed in outer mode and updated with the result), or updateable delayed-assigned MVars. When a delayed-assigned MVar is encountered, its MVar DAG is explored (via `is_resolvable_pending`) to determine if it is resolvable (and thus updateable). Results are cached across invocations. If it is updateable, the substitution is initialized from its arguments and traversal continues with the value of its pending MVar in inner mode. In inner mode (non-empty substitution), all encountered delayed-assigned MVars are, by construction, resolvable but not updateable. The substitution is carried along and extended as we cross such MVars. Pending MVars of these delayed-assigned MVars are NOT updated with the result (as the result is valid only for this substitution, not in general). Applying the substitution in one go, rather than instantiating each delayed-assigned MVar on its own from inside out, avoids the quadratic overhead of that approach when there are long chains of delayed-assigned MVars. **Write-back behavior**: Pass 2 writes back the normalized pending MVar values of delayed-assigned MVars above the updateable-MVar cut (the non-resolvable ones whose children may have been resolved). This is exactly the right set: these MVars are visited in outer mode, so their normalized values are suitable for storing in the mctx. MVars below the cut are visited in inner mode, so their intermediate values cannot be written back. ### Pass 2 scope-tracked caching A `scope_cache` data structure ensures that sharing is preserved even across different delayed-assigned MVars (and hence with different substitutions), when possible. Each `visit_delayed` call pushes a new scope with fresh fvar bindings. The cache correctly handles cross-scope reuse, fvar shadowing, and late-binding via generation counters and scope-level tracking. The `scope_cache` has been formally verified: `tests/elab/scopeCacheProofs.lean` contains a complete Lean proof that the lazy generation-based implementation refines the eager specification, covering all operations (push, pop, lookup, insert) including the rewind lazy cleanup with scope re-entry and degradation. The key correctness invariant is inter-entry gen list consistency (GensConsistent), which, unlike per-entry alignment with `currentGens`, survives pop+push cycles. ### Behavioral differences from original `instantiateMVars` The implementation matches the original single-pass `instantiateMVars` behavior with one cosmetic difference: the new implementation substitutes fvars inline during traversal rather than constructing intermediate beta-redexes, producing more beta-reduced terms in some edge cases. This changes the pretty-printed output for two elab tests (`1179b`, `depElim1`) but all terms remain definitionally equal. ### Tests Correctness and performance tests for the new implementation were added in #12808. ### Files - `src/library/instantiate_mvars.cpp` — C++ implementation of both passes (replaces `src/kernel/instantiate_mvars.cpp`) - `src/library/scope_cache.h` — scope-aware cache data structure - `src/Lean/MetavarContext.lean` — exported accessors for `DelayedMetavarAssignment` fields - `tests/elab/scopeCacheProofs.lean` — formal verification of `scope_cache` correctness - `tests/elab/1179b.lean.out.expected`, `tests/elab/depElim1.lean.out.expected` — updated expected output Co-authored-by: Claude <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
15 lines
854 B
Plaintext
15 lines
854 B
Plaintext
def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
|
|
(motive : Foo l₂ → Sort u_1) →
|
|
(t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive s₁.cons) → ((x : Foo l₂) → motive x) → motive t₂ :=
|
|
fun {l₂} motive t₂ h_1 h_2 =>
|
|
Foo.bar._sparseCasesOn_1 (motive := fun a x => l₂ = a → t₂ ≍ x → motive t₂) t₂
|
|
(fun {l} t h =>
|
|
Eq.ndrec (motive := fun {l} => (t : Foo l) → t₂ ≍ t.cons → motive t₂) (fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h
|
|
t)
|
|
(fun h h_3 =>
|
|
Eq.ndrec (motive := fun a => (t₂_1 : Foo a) → Nat.hasNotBit 2 t₂_1.ctorIdx → t₂ ≍ t₂_1 → motive t₂)
|
|
(fun t₂_1 h h_4 =>
|
|
Eq.ndrec (motive := fun t₂_2 => Nat.hasNotBit 2 t₂_2.ctorIdx → motive t₂) (fun h => h_2 t₂) (eq_of_heq h_4) h)
|
|
h_3 t₂ h)
|
|
(Eq.refl l₂) (HEq.refl t₂)
|