chore: fix tests

This PR adds an incremental variant of `shareCommon` for expressions
constructed from already-shared subterms. We use this when an
expression `e` was produced by a Lean API (e.g., `inferType`,
`mkApp4`) that does not preserve maximal sharing, but the inputs to
that API were already maximally shared. Unlike `shareCommon`, this
function does not use a local `Std.HashMap ExprPtr Expr` to track
visited nodes. This is more efficient when the number of
new (unshared) nodes is small, which is the common case when wrapping
API calls that build a few constructor nodes around shared inputs.

src/Lean/Meta/Sym/InferType.lean

@@ -9,11 +9,11 @@ public import Lean.Meta.Sym.SymM
 namespace Lean.Meta.Sym
 
 /-- Returns the type of `e`. -/
-def inferType (e : Expr) : SymM Expr := do
+public def inferType (e : Expr) : SymM Expr := do
   if let some type := (← get).inferType.find? { expr := e } then
     return type
   else
-    let type ← Meta.inferType e
+    let type ← Grind.shareCommonInc (← Meta.inferType e)
     modify fun s => { s with inferType := s.inferType.insert { expr := e } type }
     return type
 

src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean

@@ -130,4 +130,56 @@ private def go (e : Expr) : M Expr := do
     let (e, { set, .. }) := go e |>.run { map := {}, set := s.set }
     (e, ⟨set⟩)
 
+private def saveInc (e : Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).set.find? { expr := e } then
+    return r.expr
+  else
+    modify fun { set := set } => { set := set.insert { expr := e } }
+    return e
+
+@[inline] private def visitInc (e : Expr) (k : AlphaShareCommonM Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).set.find? { expr := e } then
+    return r.expr
+  else
+    saveInc (← k)
+
+/--
+Incremental variant of `shareCommonAlpha` for expressions constructed from already-shared subterms.
+
+Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
+does not preserve maximal sharing, but the inputs to that API were already maximally shared.
+In this case, only the newly constructed nodes need processing—the shared subterms can be
+looked up directly in the `AlphaShareCommonM` state without building a temporary hashmap.
+
+Unlike `shareCommonAlpha`, this function does not use a local `Std.HashMap ExprPtr Expr` to
+track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
+which is the common case when wrapping API calls that build a few constructor nodes around
+shared inputs.
+
+Example:
+```
+-- `a` and `b` are already maximally shared
+let result := mkApp2 f a b  -- result is not maximally shared
+let result ← shareCommonAlphaInc result -- efficiently restore sharing
+```
+-/
+@[inline] def shareCommonAlphaInc (e : Expr) : AlphaShareCommonM Expr :=
+  go e
+where
+  go (e : Expr) : AlphaShareCommonM Expr := do
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. => saveInc e
+  | .app f a =>
+    visitInc e (return mkApp (← go f) (← go a))
+  | .letE n t v b nd =>
+    visitInc e (return mkLet n t (← go v) (← go b) nd)
+  | .forallE n d b bi =>
+    visitInc e (return mkForall n bi (← go d) (← go b))
+  | .lam n d b bi =>
+    visitInc e (return mkLambda n bi (← go d) (← go b))
+  | .mdata d b =>
+    visitInc e (return mkMData d (← go b))
+  | .proj n i b =>
+    visitInc e (return mkProj n i (← go b))
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -424,6 +424,34 @@ def shareCommon (e : Expr) : GrindM Expr := do
   modify fun s => { s with scState }
   return e
 
+/--
+Incremental variant of `shareCommon` for expressions constructed from already-shared subterms.
+
+Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
+does not preserve maximal sharing, but the inputs to that API were already maximally shared.
+
+Unlike `shareCommon`, this function does not use a local `Std.HashMap ExprPtr Expr` to
+track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
+which is the common case when wrapping API calls that build a few constructor nodes around
+shared inputs.
+
+Example:
+```
+-- `a` and `b` are already maximally shared
+let result := mkApp2 f a b  -- result is not maximally shared
+let result ← shareCommonInc result -- efficiently restore sharing
+```
+-/
+def shareCommonInc (e : Expr) : GrindM Expr := do
+  let scState ← modifyGet fun s => (s.scState, { s with scState := {} })
+  let (e, scState) := shareCommonAlphaInc e scState
+  modify fun s => { s with scState }
+  return e
+
+@[inherit_doc shareCommonInc]
+abbrev shareCommon' (e : Expr) : GrindM Expr :=
+  shareCommonInc e
+
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
   return isSameExpr e (← getTrueExpr)

tests/lean/run/sym_pattern.lean

@@ -13,9 +13,9 @@ def test1 : SymM Unit := do
   let e ← shareCommon (← getConstInfo ``ex).value!
   let some r₁ ← pEx.match? e | throwError "failed"
   logInfo <| mkAppN (mkConst ``Exists.intro r₁.us) r₁.args
-  let some r₂ ← pAnd.match? (← inferType r₁.args[3]!) | throwError "failed"
+  let some r₂ ← pAnd.match? (← Sym.inferType r₁.args[3]!) | throwError "failed"
   logInfo <| mkAppN (mkConst ``And.intro r₂.us) r₂.args
-  let some r₃ ← pEq.unify? (← inferType r₂.args[3]!) | throwError "failed"
+  let some r₃ ← pEq.unify? (← Sym.inferType r₂.args[3]!) | throwError "failed"
   logInfo <| mkAppN (mkConst ``Eq.refl r₃.us) r₃.args
 
 /--

tests/lean/run/sym_pattern_2.lean

@@ -42,8 +42,8 @@ def test₂ : SymM Unit := do
   let h := mkAppN (mkConst ``mk_forall_and r₁.us) r₁.args
   check h
   logInfo h
-  logInfo (← inferType r₁.args[3]!)
-  logInfo (← inferType r₁.args[4]!)
+  logInfo (← Sym.inferType r₁.args[3]!)
+  logInfo (← Sym.inferType r₁.args[4]!)
 
 /--
 info: ∀ (x : #4), @#3 x ∧ @#2 x