From 1e99ff1dba98d9dc99fd9db65d08428862b7f14b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Dec 2025 15:12:21 -0800 Subject: [PATCH] feat: optimized `abstractFVars` and `abstractFVarsRange` (#11820) This PR adds optimized `abstractFVars` and `abstractFVarsRange` for converting free variables to de Bruijn indices during pattern matching/unification. **Optimizations:** - Metavariables are skipped (their contexts must not include abstracted fvars) - Subterms whose `maxFVar` is below the minimal abstracted fvar are skipped via early cutoff - Results are maximally shared via `AlphaShareBuilderM` These optimizations are sound for Miller pattern matching where metavariables are created before entering binders. --- src/Lean/Meta/Sym.lean | 1 + src/Lean/Meta/Sym/AbstractS.lean | 87 +++++++++++++++++++++++++++++ tests/lean/run/sym_instantiate.lean | 32 ++++++++++- 3 files changed, 118 insertions(+), 2 deletions(-) create mode 100644 src/Lean/Meta/Sym/AbstractS.lean diff --git a/src/Lean/Meta/Sym.lean b/src/Lean/Meta/Sym.lean index 83b815fe3d..11709a3012 100644 --- a/src/Lean/Meta/Sym.lean +++ b/src/Lean/Meta/Sym.lean @@ -16,6 +16,7 @@ public import Lean.Meta.Sym.IsClass public import Lean.Meta.Sym.Intro public import Lean.Meta.Sym.InstantiateMVarsS public import Lean.Meta.Sym.ProofInstInfo +public import Lean.Meta.Sym.AbstractS public import Lean.Meta.Sym.Pattern /-! diff --git a/src/Lean/Meta/Sym/AbstractS.lean b/src/Lean/Meta/Sym/AbstractS.lean new file mode 100644 index 0000000000..4833574ffa --- /dev/null +++ b/src/Lean/Meta/Sym/AbstractS.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Lean.Meta.Sym.SymM +import Lean.Meta.Sym.ReplaceS +namespace Lean.Meta.Sym +open Grind + +/-- +Helper function for implementing `abstractFVars` (and possible variants in the future). +-/ +@[inline] def abstractFVarsCore (e : Expr) (lctx : LocalContext) + (maxFVar : PHashMap ExprPtr (Option FVarId)) + (minFVarId : FVarId) (toDeBruijn? : FVarId → Option Nat) : AlphaShareBuilderM Expr := do + let minIndex := (lctx.find? minFVarId).get!.index + replaceS' e fun e offset => do + match e with + | .fvar fvarId => + if let some bidx := toDeBruijn? fvarId then + mkBVarS (offset + bidx) + else + return some e + | .lit _ | .mvar _ | .bvar _ | .const _ _ | .sort _ => + /- + Avoid `e.hasFVar` check. + **Note**: metavariables are safe to skip because we assume their local contexts never include + the free variables being abstracted (they were created before entering binders). + -/ + return some e + | _ => + -- Non-atomic expressions. + if !e.hasFVar then + -- Stop visiting: `e` does not contain free variables. + return some e + let some maxFVarId? := maxFVar.find? ⟨e⟩ + | return none -- maxFVar information is not available, keep visiting + let maxIndex := (lctx.find? maxFVarId?.get!).get!.index + if maxIndex < minIndex then + -- Stop visiting: maximal free variable in `e` is smaller than minimal free variable being abstracted. + return some e + else + -- Keep visiting + return none + +/-- +Abstracts free variables `xs[start...*]` in expression `e`, converting them to de Bruijn indices. + +Assumptions: +- The local context of the metavariables occurring in `e` do not include the free variables being + abstracted. This invariant holds when abstracting over binders during pattern matching/unification: + metavariables in the pattern were created before entering the binder, so their contexts exclude + the bound variable's corresponding fvar. + +- If `xs[start...*]` is not empty, then the minimal variable is `xs[start]`. + +- Subterms whose `maxFVar` is below `minFVarId` are skipped entirely. This function does not assume +the `maxFVar` cache contains information for every subterm in `e`. +-/ +public def abstractFVarsRange (e : Expr) (start : Nat) (xs : Array Expr) : SymM Expr := do + if !e.hasFVar then return e + if h : start < xs.size then + let toDeBruijn? (fvarId : FVarId) : Option Nat := + let rec go (bidx : Nat) (i : Nat) (h : i < xs.size) : Option Nat := + if xs[i].fvarId! == fvarId then + some bidx + else if i > start then + go (bidx + 1) (i - 1) (by omega) + else + none + go 0 (xs.size - 1) (by omega) + liftBuilderM <| abstractFVarsCore e (← getLCtx) (← get).maxFVar xs[start].fvarId! toDeBruijn? + else + return e + +/-- +Abstracts free variables `xs` in expression `e`, converting them to de Bruijn indices. + +It is an abbreviation for `abstractFVarsRange e 0 xs`. +-/ +public abbrev abstractFVars (e : Expr) (xs : Array Expr) : SymM Expr := do + abstractFVarsRange e 0 xs + +end Lean.Meta.Sym diff --git a/tests/lean/run/sym_instantiate.lean b/tests/lean/run/sym_instantiate.lean index aa2520aeee..1626ab32cd 100644 --- a/tests/lean/run/sym_instantiate.lean +++ b/tests/lean/run/sym_instantiate.lean @@ -1,5 +1,5 @@ import Lean.Meta.Sym - +set_option grind.debug true open Lean Meta Grind Sym def tst1 : SymM Unit := do @@ -21,7 +21,6 @@ def tst1 : SymM Unit := do assert! r == e.instantiate #[a, b] logInfo r - /-- info: f b a 1 --- @@ -33,3 +32,32 @@ info: fun x => f x a 1 -/ #guard_msgs in #eval SymM.run' tst1 + +def tst2 : SymM Unit := do + let f ← mkConstS `f + withLocalDeclD `w (← mkConstS ``Nat) fun w => do + let w ← shareCommon w + let e ← mkAppS (← mkAppS (← mkAppS f (← mkBVarS 0)) (← mkBVarS 1)) w + withLocalDeclD `x (← mkConstS ``Nat) fun x => do + withLocalDeclD `y (← mkConstS ``Nat) fun y => do + let x ← shareCommon x + let y ← shareCommon y + logInfo e + let r ← instantiateRevS e #[x, y] + logInfo r + assert! isSameExpr (← abstractFVars r #[x, y]) e + logInfo (← abstractFVars r #[x, y]) + logInfo (← abstractFVarsRange r 1 #[x, y]) + + +/-- +info: f #0 #1 w +--- +info: f y x w +--- +info: f #0 #1 w +--- +info: f #0 x w +-/ +#guard_msgs in +#eval SymM.run' tst2