feat: add AlphaShareBuilder (#11793)

This PR adds functions for creating maximally shared terms from
maximally shared terms. It is more efficient than creating an expression
and then invoking `shareCommon`. We are going to use these functions for
implementing the symbolic simulation primitives.

src/Lean/Meta/Sym/Main.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.SymM
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Tactic.Grind.Main
+public section
 namespace Lean.Meta.Sym
 open Grind (Params)
 

src/Lean/Meta/Tactic/Grind.lean

@@ -48,6 +48,8 @@ public import Lean.Meta.Tactic.Grind.Filter
 public import Lean.Meta.Tactic.Grind.CollectParams
 public import Lean.Meta.Tactic.Grind.Finish
 public import Lean.Meta.Tactic.Grind.RegisterCommand
+public import Lean.Meta.Tactic.Grind.AlphaShareCommon
+public import Lean.Meta.Tactic.Grind.AlphaShareBuilder
 public section
 namespace Lean
 

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

@@ -0,0 +1,85 @@
+/-
+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.Tactic.Grind.Types
+public section
+namespace Lean.Meta.Grind
+/-!
+Helper functions for constructing maximally shared expressions from maximally shared expressions.
+-/
+private def share (e : Expr) : GrindM Expr := do
+  let key : AlphaKey := ⟨e⟩
+  if let some r := (← get).scState.set.find? key then
+    return r.expr
+  else
+    modify fun s => { s with scState.set := s.scState.set.insert key }
+    return e
+
+private def assertShared (e : Expr) : GrindM Unit := do
+  assert! (← get).scState.set.contains ⟨e⟩
+
+def mkLitS (l : Literal) : GrindM Expr :=
+  share <| .lit l
+
+def mkConstS (declName : Name) (us : List Level := []) : GrindM Expr :=
+  share <| .const declName us
+
+def mkBVarS (idx : Nat) : GrindM Expr :=
+  share <| .bvar idx
+
+def mkSortS (u : Level) : GrindM Expr :=
+  share <| .sort u
+
+def mkFVarS (fvarId : FVarId) : GrindM Expr :=
+  share <| .fvar fvarId
+
+def mkMVarS (mvarId : MVarId) : GrindM Expr := do
+  share <| .mvar mvarId
+
+def mkMDataS (m : MData) (e : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared e
+  share <| .mdata m e
+
+def mkProjS (structName : Name) (idx : Nat) (struct : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared struct
+  share <| .proj structName idx struct
+
+def mkAppS (f a : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared f
+    assertShared a
+  share <| .app f a
+
+def mkLambdaS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared t
+    assertShared b
+  share <| .lam x t b bi
+
+def mkForallS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared t
+    assertShared b
+  share <| .forallE x t b bi
+
+def mkLetS (x : Name) (t : Expr) (v : Expr) (b : Expr) (nondep : Bool := false) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared t
+    assertShared v
+    assertShared b
+  share <| .letE x t v b nondep
+
+def mkHaveS (x : Name) (t : Expr) (v : Expr) (b : Expr) : GrindM Expr := do
+  if (← isDebugEnabled) then
+    assertShared t
+    assertShared v
+    assertShared b
+  share <| .letE x t v b true
+
+end Lean.Meta.Grind

tests/lean/run/grind_alphaShare_builder.lean

@@ -0,0 +1,24 @@
+import Lean.Meta.Tactic.Grind
+import Lean.Meta.Sym.Main
+open Lean Meta Grind Sym
+set_option grind.debug true
+
+def test : GrindM Unit := do
+  let f  ← mkConstS `f
+  let f₁ := mkConst `f
+  let f₂ ← mkConstS `f
+  assert! isSameExpr f f₂
+  assert! !isSameExpr f f₁
+  let x₁ ← mkBVarS 0
+  let x₂ ← mkBVarS 0
+  assert! isSameExpr
+    (← mkLambdaS `x .default (← mkConstS ``Nat) (← mkMDataS {} (← mkProjS ``Prod 0 (← mkAppS f x₁))))
+    (← mkLambdaS `y .default (← mkConstS ``Nat) (← mkMDataS {} (← mkProjS ``Prod 0 (← mkAppS f₂ x₂))))
+  assert! !isSameExpr (← mkAppS f x₁) (mkApp f x₁)
+  assert!
+    mkLambda `x .default (mkConst ``Nat) (mkMData {} (mkProj ``Prod 0 (mkApp f x₁)))
+    ==
+    (← mkLambdaS `y .default (← mkConstS ``Nat) (← mkMDataS {} (← mkProjS ``Prod 0 (← mkAppS f₂ x₂))))
+
+#eval SymM.run' do
+  test