feat: add Sym.getMaxFVar?

This PR adds the function `getMaxFVar?` for implementing `SymM` primitives.

src/Lean/Meta/Sym.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.SymM
 public import Lean.Meta.Sym.Main
 public import Lean.Meta.Sym.Util
+public import Lean.Meta.Sym.MaxFVar
 
 /-!
 # Symbolic simulation support.

src/Lean/Meta/Sym/Main.lean

@@ -13,7 +13,7 @@ namespace Lean.Meta.Sym
 open Grind (Params)
 
 def SymM.run (x : SymM α) (params : Params) : MetaM α := do
-  x.run' {} |>.run params
+  x params |>.run' {} |>.run params
 
 def SymM.run' (x : SymM α) (config : Grind.Config := {}) : MetaM α := do
   let params ← Grind.mkDefaultParams config

src/Lean/Meta/Sym/MaxFVar.lean

@@ -0,0 +1,51 @@
+/-
+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
+public section
+namespace Lean.Meta.Sym
+
+private def max (fvarId1? : Option FVarId) (fvarId2? : Option FVarId) : MetaM (Option FVarId) := do
+  let some fvarId1 := fvarId1? | return fvarId2?
+  let some fvarId2 := fvarId2? | return fvarId1?
+  if fvarId1 == fvarId2 then return fvarId1?
+  let localDecl1 ← fvarId1.getDecl
+  let localDecl2 ← fvarId2.getDecl
+  if localDecl1.index > localDecl2.index then
+    return fvarId1?
+  else
+    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?
+  else
+    let fvarId? ← k
+    modify fun s => { s with maxFVar := s.maxFVar.insert { expr := e } fvarId? }
+    return fvarId?
+
+/--
+Returns the maximal free variable occurring in `e`.
+This function assumes the current local context contains all free variables used in `e`.
+-/
+def getMaxFVar? (e : Expr) : SymM (Option FVarId) := do
+  match e with
+  | .fvar fvarId => return some fvarId
+  | .const .. | .bvar .. | .sort .. | .lit .. => return none
+  | .app f a => check e do max (← getMaxFVar? f) (← getMaxFVar? a)
+  | .proj _ _ s => check e do getMaxFVar? s
+  | .lam _ d b _ | .forallE _ d b _ => check e do max (← getMaxFVar? d) (← getMaxFVar? b)
+  | .letE _ t v b _ => check e do max (← max (← getMaxFVar? t) (← getMaxFVar? v)) (← getMaxFVar? b)
+  | .mdata _ e => check e do getMaxFVar? e
+  | .mvar mvarId => check e do
+    let mvarDecl ← mvarId.getDecl
+    let lctx := mvarDecl.lctx
+    if lctx.decls.isEmpty then return none
+    let some last := lctx.lastDecl | unreachable! -- SymM local contexts do not have holes
+    return some last.fvarId
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/SymM.lean

@@ -6,12 +6,14 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Main
+public section
 namespace Lean.Meta.Sym
 export Grind (ExprPtr Goal)
 
 structure State where
-  maxFVar : PHashMap ExprPtr Expr := {}
+  maxFVar : PHashMap ExprPtr (Option FVarId) := {}
 
-public abbrev SymM := StateRefT State Grind.GrindM
+abbrev SymM := ReaderT Grind.Params StateRefT State Grind.GrindM
 
 end Lean.Meta.Sym

tests/lean/run/getMaxFVar.lean

@@ -0,0 +1,34 @@
+import Lean.Meta.Sym
+import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+open Lean Meta Grind Sym
+
+def checkMaxFVar (e : Expr) (x : Expr) : SymM Unit := do
+  let some fvarId ← getMaxFVar? e | unreachable!
+  assert! x.fvarId! == fvarId
+
+def test1 : MetaM Unit := do
+  let nat := mkConst ``Nat
+  withLocalDeclD `x nat fun x => do
+  let m₁ ← mkFreshExprMVar nat
+  withLocalDeclD `y nat fun y => do
+  let m₂ ← mkFreshExprMVar nat
+  withLocalDeclD `z nat fun z => do
+  SymM.run' do
+  let x ← shareCommon x
+  let y ← shareCommon y
+  let z ← shareCommon z
+  let m₁ ← shareCommon m₁
+  let m₂ ← shareCommon m₂
+  let f ← mkConstS `f
+  let e₁ ← mkAppS f x
+  checkMaxFVar e₁ x
+  let e₂ ← mkAppS e₁ m₁
+  checkMaxFVar e₂ x
+  let e₂ ← mkAppS e₁ m₂
+  checkMaxFVar e₂ y
+  let e₃ ← mkAppS e₂ (← mkProjS ``Prod 0 (← mkAppS f z))
+  checkMaxFVar e₃ z
+  let e₄ ← mkAppS f (← shareCommon (mkNatLit 3))
+  assert! (← getMaxFVar? e₄).isNone
+
+#eval test1