From b60556af4ef59890fe709d3cd3f7d807afc417f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Dec 2025 09:07:56 -0800 Subject: [PATCH] chore: `Sym` cleanup (#11833) This PR fixes a few typos, adds missing docstrings, and adds a (simple) missing optimization. --- src/Lean/Meta/Sym/InstantiateS.lean | 7 ++++++- src/Lean/Meta/Sym/Intro.lean | 2 +- src/Lean/Meta/Sym/LooseBVarsS.lean | 6 +++--- src/Lean/Meta/Sym/MaxFVar.lean | 14 +++++++++----- src/Lean/Meta/Sym/Pattern.lean | 3 +-- src/Lean/Meta/Sym/SymM.lean | 18 ++++++++++++++++++ 6 files changed, 38 insertions(+), 12 deletions(-) diff --git a/src/Lean/Meta/Sym/InstantiateS.lean b/src/Lean/Meta/Sym/InstantiateS.lean index 37377fbd8d..c208380a67 100644 --- a/src/Lean/Meta/Sym/InstantiateS.lean +++ b/src/Lean/Meta/Sym/InstantiateS.lean @@ -79,6 +79,7 @@ def instantiateRangeS' (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) : else return none +/-- Internal variant of `instantiateS` that runs in `AlphaShareBuilderM`. -/ def instantiateS' (e : Expr) (subst : Array Expr) : AlphaShareBuilderM Expr := instantiateRangeS' e 0 subst.size subst @@ -101,7 +102,8 @@ where loop revArgs start (← mkAppS b revArgs[i]!) i /-- -Similar to `betaRev`, but ensures maximally shared terms. +Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms. +`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`. -/ partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr := if revArgs.size == 0 then @@ -121,12 +123,15 @@ partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr mkAppRevRangeS (← instantiateRangeS' e n sz revArgs) 0 n revArgs go f 0 +/-- Monad for `instantiateRevBetaS'` with caching keyed by `(expression pointer, binder offset)`. -/ abbrev M := StateT (Std.HashMap (ExprPtr × Nat) Expr) AlphaShareBuilderM +/-- Caches the result `r` for `key` and returns `r`. -/ def save (key : ExprPtr × Nat) (r : Expr) : M Expr := do modify fun cache => cache.insert key r return r +/-- Internal variant of `instantiateRevBetaS` that runs in `AlphaShareBuilderM`. -/ partial def instantiateRevBetaS' (e : Expr) (subst : Array Expr) : AlphaShareBuilderM Expr := do if subst.isEmpty || !e.hasLooseBVars then return e visit e 0 |>.run' {} diff --git a/src/Lean/Meta/Sym/Intro.lean b/src/Lean/Meta/Sym/Intro.lean index 4716bf2f7e..add0e9c87b 100644 --- a/src/Lean/Meta/Sym/Intro.lean +++ b/src/Lean/Meta/Sym/Intro.lean @@ -120,7 +120,7 @@ Throws an error if the target type does not have a leading binder. public def intro (goal : Goal) (name : Name) : SymM (FVarId × Goal) := do let (fvarIds, goal') ← introCore goal 1 #[name] if h : 0 < fvarIds.size then - return (fvarIds[0], goal) + return (fvarIds[0], goal') else throwError "`intro` failed, binder expected" diff --git a/src/Lean/Meta/Sym/LooseBVarsS.lean b/src/Lean/Meta/Sym/LooseBVarsS.lean index 5406f00d7f..791d34daa9 100644 --- a/src/Lean/Meta/Sym/LooseBVarsS.lean +++ b/src/Lean/Meta/Sym/LooseBVarsS.lean @@ -9,7 +9,7 @@ public import Lean.Meta.Sym.SymM public import Lean.Meta.Sym.ReplaceS public section namespace Lean.Meta.Sym - +open Grind /-- Lowers the loose bound variables `>= s` in `e` by `d`. That is, a loose bound variable `bvar i` with `i >= s` is mapped to `bvar (i-d)`. @@ -24,7 +24,7 @@ def lowerLooseBVarsS' (e : Expr) (s d : Nat) : AlphaShareBuilderM Expr := do else match e with | .bvar idx => if idx >= s₁ then - return some (← Grind.mkBVarS (idx - d)) + return some (← mkBVarS (idx - d)) else return none | _ => return none @@ -45,7 +45,7 @@ def liftLooseBVarsS' (e : Expr) (s d : Nat) : AlphaShareBuilderM Expr := do else match e with | .bvar idx => if idx >= s₁ then - return some (← Grind.mkBVarS (idx + d)) + return some (← mkBVarS (idx + d)) else return none | _ => return none diff --git a/src/Lean/Meta/Sym/MaxFVar.lean b/src/Lean/Meta/Sym/MaxFVar.lean index e029dc55fd..930cbe4a42 100644 --- a/src/Lean/Meta/Sym/MaxFVar.lean +++ b/src/Lean/Meta/Sym/MaxFVar.lean @@ -21,12 +21,16 @@ private def max (fvarId1? : Option FVarId) (fvarId2? : Option FVarId) : MetaM (O return fvarId2? private abbrev check (e : Expr) (k : SymM (Option FVarId)) : SymM (Option FVarId) := do - if let some fvarId? := (← get).maxFVar.find? { expr := e } then - return fvarId? + if e.hasFVar || e.hasMVar then + if let some fvarId? := (← get).maxFVar.find? { expr := e } then + return fvarId? + else + let fvarId? ← k + modify fun s => { s with maxFVar := s.maxFVar.insert { expr := e } fvarId? } + return fvarId? else - let fvarId? ← k - modify fun s => { s with maxFVar := s.maxFVar.insert { expr := e } fvarId? } - return fvarId? + -- `e` does not contain free variables or metavariables, then `maxFVar[e]` is definitely `none`. + return none /-- Returns the maximal free variable occurring in `e`. diff --git a/src/Lean/Meta/Sym/Pattern.lean b/src/Lean/Meta/Sym/Pattern.lean index 0bf7983b62..86e8bb0e9d 100644 --- a/src/Lean/Meta/Sym/Pattern.lean +++ b/src/Lean/Meta/Sym/Pattern.lean @@ -421,7 +421,7 @@ in `t`. We use this function when `t` is a metavariable, and we are trying to as -/ def mayAssign (t s : Expr) : SymM Bool := do let some sMaxFVarId ← getMaxFVar? s - | return true -- `s` does not contain metavariables + | return true -- `s` does not contain free variables let some tMaxFVarId ← getMaxFVar? t | return false let sMaxFVarDecl ← sMaxFVarId.getDecl @@ -495,7 +495,6 @@ def isDefEqAppWithInfo (t : Expr) (s : Expr) (i : Nat) (info : ProofInstInfo) : if (← tryAssignUnassigned a₁ a₂) then return true else - -- isDefEqI a₁ a₂ else if argInfo.isProof then discard <| tryAssignUnassigned a₁ a₂ diff --git a/src/Lean/Meta/Sym/SymM.lean b/src/Lean/Meta/Sym/SymM.lean index 70516b5149..048d189d3f 100644 --- a/src/Lean/Meta/Sym/SymM.lean +++ b/src/Lean/Meta/Sym/SymM.lean @@ -36,6 +36,24 @@ public structure ProofInstInfo where deriving Inhabited structure State where + /-- + Maps expressions to their maximal free variable (by declaration index). + + - `maxFVar[e] = some fvarId` means `fvarId` is the free variable with the largest declaration + index occurring in `e`. + - `maxFVar[e] = none` means `e` contains no free variables (but may contain metavariables). + + Recall that if `e` contains a metavariable `?m`, then we assume `e` may contain any free variable + in the local context associated with `?m`. + + This mapping enables O(1) local context compatibility checks during metavariable assignment. + Instead of traversing local contexts with `isSubPrefixOf`, we check if the maximal free variable + in the assigned value is in scope of the metavariable's local context. + + **Note**: We considered using a mapping `PHashMap ExprPtr FVarId`. However, there is a corner + case that is not supported by this representation. `e` contains a metavariable (with an empty local context), + and no free variables. + -/ maxFVar : PHashMap ExprPtr (Option FVarId) := {} proofInstInfo : PHashMap Name (Option ProofInstInfo) := {}