chore: cleanup

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -22,8 +22,9 @@ structure Context extends Tactic.Context where
 open Meta.Grind (Goal)
 
 structure State where
-  state : Meta.Grind.State
-  goals : List Goal
+  symState   : Meta.Sym.State
+  grindState : Meta.Grind.State
+  goals      : List Goal
 
 structure SavedState where
   term   : Term.SavedState
@@ -288,8 +289,8 @@ open Grind
 def liftGrindM (k : GrindM α) : GrindTacticM α := do
   let ctx ← read
   let s ← get
-  let (a, state) ← liftMetaM <| (Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.state
-  modify fun s => { s with state }
+  let ((a, grindState), symState) ← liftMetaM <| StateRefT'.run ((Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.grindState) s.symState
+  modify fun s => { s with grindState, symState }
   return a
 
 def replaceMainGoal (goals : List Goal) : GrindTacticM Unit := do
@@ -358,15 +359,17 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
     let methods ← getMethods
     let grindCtx ← readThe Meta.Grind.Context
     let grindState ← get
+    let symState ← getThe Sym.State
     -- **Note**: we discard changes to `Term.State`
-    let (subgoals, grindState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
+    let (subgoals, grindState', symState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
       let (_, s) ← GrindTacticM.run
             (ctx := { recover := false, methods, ctx := grindCtx, params, elaborator })
-            (s := { state := grindState, goals := [goal] }) do
+            (s := { grindState, symState, goals := [goal] }) do
         evalGrindTactic stx.raw
         pruneSolvedGoals
-      return (s.goals, s.state)
+      return (s.goals, s.grindState, s.symState)
     set grindState'
+    set symState'
     return subgoals
   return eval
 
@@ -389,8 +392,9 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
       let ctx ← readThe Meta.Grind.Context
       /- Restore original config -/
       let ctx := { ctx with config := params.config }
-      let state ← get
-      pure (methods, ctx, { state, goals })
+      let grindState ← get
+      let symState ← getThe Sym.State
+      return (methods, ctx, { grindState, symState, goals })
   let tctx ← read
   k { tctx with methods, ctx, params } |>.run state
 

src/Lean/Meta/Sym.lean

@@ -5,9 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Sym.AlphaShareBuilder
+public import Lean.Meta.Sym.AlphaShareCommon
+public import Lean.Meta.Sym.ExprPtr
 public import Lean.Meta.Sym.SymM
-public import Lean.Meta.Sym.Main
-public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.MaxFVar
 public import Lean.Meta.Sym.ReplaceS
 public import Lean.Meta.Sym.LooseBVarsS
@@ -21,7 +22,7 @@ public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.InferType
 public import Lean.Meta.Sym.Simp
-
+public import Lean.Meta.Sym.Util
 
 /-!
 # Symbolic simulation support.

src/Lean/Meta/Sym/AbstractS.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.ReplaceS
 namespace Lean.Meta.Sym
-open Grind
+open Internal
 
 /--
 Helper function for implementing `abstractFVars` (and possible variants in the future).

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -5,37 +5,45 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.SymM
 public section
-namespace Lean.Meta.Grind
+namespace Lean.Meta.Sym.Internal
 /-!
 Helper functions for constructing maximally shared expressions from maximally shared expressions.
+That is, `mkAppS f a` assumes that `f` and `a` are maximally shared.
+
+These functions are in the `Internal` namespace because they can be easily misused.
+We use them to construct safe functions.
 -/
-protected def Grind.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
-
-protected def Grind.assertShared (e : Expr) : GrindM Unit := do
-  assert! (← get).scState.set.contains ⟨e⟩
-
 class MonadShareCommon (m : Type → Type) where
-  share : Expr → m Expr
+  share1 : Expr → m Expr
   assertShared : Expr → m Unit
   isDebugEnabled : m Bool
 
 @[always_inline]
 instance (m n) [MonadLift m n] [MonadShareCommon m] : MonadShareCommon n where
-  share e := liftM (MonadShareCommon.share e : m Expr)
+  share1 e := liftM (MonadShareCommon.share1 e : m Expr)
   assertShared e := liftM (MonadShareCommon.assertShared e : m Unit)
   isDebugEnabled := liftM (MonadShareCommon.isDebugEnabled : m Bool)
 
-instance : MonadShareCommon GrindM where
-  share := Grind.share
-  assertShared := Grind.assertShared
+private def dummy : AlphaKey := { expr := mkConst `__dummy__}
+
+protected def Sym.share1 (e : Expr) : SymM Expr := do
+  let prev := (← get).share.set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` is new
+    modify fun s => { s with share.set := s.share.set.insert { expr := e } }
+    return e
+  else
+    return prev.expr
+
+protected def Sym.assertShared (e : Expr) : SymM Unit := do
+  let prev := (← get).share.set.findD { expr := e } dummy
+  assert! isSameExpr prev.expr e
+
+instance : MonadShareCommon SymM where
+  share1 := Sym.share1
+  assertShared := Sym.assertShared
   isDebugEnabled := isDebugEnabled
 
 /--
@@ -47,92 +55,93 @@ abbrev AlphaShareBuilderM := ReaderT Bool AlphaShareCommonM
 /--
 Helper function for lifting a `AlphaShareBuilderM` action to `GrindM`
 -/
-abbrev liftBuilderM (k : AlphaShareBuilderM α) : GrindM α := do
-  let scState ← modifyGet fun s => (s.scState, { s with scState := {} })
-  let (a, scState) := k (← isDebugEnabled) scState
-  modify fun s => { s with scState }
+abbrev liftBuilderM (k : AlphaShareBuilderM α) : SymM α := do
+  let share ← modifyGet fun s => (s.share, { s with share := {} })
+  let (a, share) := k (← isDebugEnabled) share
+  modify fun s => { s with share }
   return a
 
-protected def Builder.share (e : Expr) : AlphaShareBuilderM Expr := do
-  let key : AlphaKey := ⟨e⟩
-  if let some r := (← get).set.find? key then
-    return r.expr
-  else
-    modify fun s => { s with set := s.set.insert key }
+protected def Builder.share1 (e : Expr) : AlphaShareBuilderM Expr := do
+  let prev := (← get).set.findD { expr := e } dummy
+  if isSameExpr prev.expr dummy.expr then
+    -- `e` is new
+    modify fun { set := set } => { set := set.insert { expr := e } }
     return e
+  else
+    return prev.expr
 
 protected def Builder.assertShared (e : Expr) : AlphaShareBuilderM Unit := do
   assert! (← get).set.contains ⟨e⟩
 
 instance : MonadShareCommon AlphaShareBuilderM where
-  share := Builder.share
+  share1 := Builder.share1
   assertShared := Builder.assertShared
   isDebugEnabled := read
 
-open MonadShareCommon (share assertShared)
+open MonadShareCommon (share1 assertShared)
 
 variable [MonadShareCommon m]
 
 def mkLitS (l : Literal) : m Expr :=
-  share <| .lit l
+  share1 <| .lit l
 
 def mkConstS (declName : Name) (us : List Level := []) : m Expr :=
-  share <| .const declName us
+  share1 <| .const declName us
 
 def mkBVarS (idx : Nat) : m Expr :=
-  share <| .bvar idx
+  share1 <| .bvar idx
 
 def mkSortS (u : Level) : m Expr :=
-  share <| .sort u
+  share1 <| .sort u
 
 def mkFVarS (fvarId : FVarId) : m Expr :=
-  share <| .fvar fvarId
+  share1 <| .fvar fvarId
 
 def mkMVarS (mvarId : MVarId) : m Expr :=
-  share <| .mvar mvarId
+  share1 <| .mvar mvarId
 
 variable [Monad m]
 
 def mkMDataS (d : MData) (e : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared e
-  share <| .mdata d e
+  share1 <| .mdata d e
 
 def mkProjS (structName : Name) (idx : Nat) (struct : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared struct
-  share <| .proj structName idx struct
+  share1 <| .proj structName idx struct
 
 def mkAppS (f a : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared f
     assertShared a
-  share <| .app f a
+  share1 <| .app f a
 
 def mkLambdaS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared t
     assertShared b
-  share <| .lam x t b bi
+  share1 <| .lam x t b bi
 
 def mkForallS (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared t
     assertShared b
-  share <| .forallE x t b bi
+  share1 <| .forallE x t b bi
 
 def mkLetS (x : Name) (t : Expr) (v : Expr) (b : Expr) (nondep : Bool := false) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared t
     assertShared v
     assertShared b
-  share <| .letE x t v b nondep
+  share1 <| .letE x t v b nondep
 
 def mkHaveS (x : Name) (t : Expr) (v : Expr) (b : Expr) : m Expr := do
   if (← MonadShareCommon.isDebugEnabled) then
     assertShared t
     assertShared v
     assertShared b
-  share <| .letE x t v b true
+  share1 <| .letE x t v b true
 
-end Lean.Meta.Grind
+end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/AlphaShareCommon.lean

@@ -5,9 +5,9 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.ExprPtr
+public import Lean.Meta.Sym.ExprPtr
 public section
-namespace Lean.Meta.Grind
+namespace Lean.Meta.Sym
 
 private def hashChild (e : Expr) : UInt64 :=
   match e with
@@ -180,4 +180,4 @@ where
   | .mdata _ b => visitInc e (return e.updateMData! (← go b))
   | .proj _ _ b => visitInc e (return e.updateProj! (← go b))
 
-end Lean.Meta.Grind
+end Lean.Meta.Sym

src/Lean/Meta/Sym/Apply.lean

@@ -105,14 +105,13 @@ Applies a backward rule to a goal, returning new subgoals.
 
 Throws an error if unification fails.
 -/
-public def BackwardRule.apply (goal : Goal) (rule : BackwardRule) : SymM (List Goal) := goal.withContext do
-  let type ← goal.mvarId.getType
-  if let some result ← rule.pattern.unify? type then
-    goal.mvarId.assign (mkValue rule.expr rule.pattern result)
+public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId) := mvarId.withContext do
+  let decl ← mvarId.getDecl
+  if let some result ← rule.pattern.unify? decl.type then
+    mvarId.assign (mkValue rule.expr rule.pattern result)
     return rule.resultPos.map fun i =>
-      let mvarId := result.args[i]!.mvarId!
-      { goal with mvarId }
+      result.args[i]!.mvarId!
   else
-    throwError "rule is not applicable to goal{goal.mvarId}rule:{indentExpr rule.expr}"
+    throwError "rule is not applicable to goal{mvarId}rule:{indentExpr rule.expr}"
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/ExprPtr.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Lean.Expr
 public section
-namespace Lean.Meta.Grind
+namespace Lean.Meta.Sym
 
 @[inline] def isSameExpr (a b : Expr) : Bool :=
   -- It is safe to use pointer equality because we hashcons all expressions
@@ -31,4 +31,4 @@ instance : Hashable ExprPtr where
 instance : BEq ExprPtr where
   beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
 
-end Lean.Meta.Grind
+end Lean.Meta.Sym

src/Lean/Meta/Sym/InferType.lean

@@ -21,7 +21,7 @@ public def inferType (e : Expr) : SymM Expr := do
   if let some type := (← get).inferType.find? { expr := e } then
     return type
   else
-    let type ← Grind.shareCommonInc (← inferTypeWithoutCache e)
+    let type ← shareCommonInc (← inferTypeWithoutCache e)
     modify fun s => { s with inferType := s.inferType.insert { expr := e } type }
     return type
 

src/Lean/Meta/Sym/InstantiateMVarsS.lean

@@ -14,7 +14,7 @@ Instantiates metavariables occurring in `e`, and returns a maximally shared term
 public def instantiateMVarsS (e : Expr) : SymM Expr := do
   if e.hasMVar then
     -- **Note**: If this is a bottleneck, write a new function that combines both steps.
-    Grind.shareCommon (← instantiateMVars e)
+    shareCommon (← instantiateMVars e)
   else
     return e
 

src/Lean/Meta/Sym/InstantiateS.lean

@@ -10,8 +10,7 @@ import Lean.Meta.Sym.ReplaceS
 import Lean.Meta.Sym.LooseBVarsS
 import Init.Grind
 namespace Lean.Meta.Sym
-open Grind
-
+open Internal
 /--
 Similar to `Lean.Expr.instantiateRevRange`.
 It assumes the input is maximally shared, and ensures the output is too.
@@ -68,7 +67,7 @@ def instantiateRangeS' (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) :
           let v := subst[idx - s₁]
           liftLooseBVarsS' v 0 offset
         else
-          Grind.mkBVarS (idx - n)
+          mkBVarS (idx - n)
       else
         return some e
     | .lit _ | .mvar _ | .fvar _ | .const _ _ | .sort _ =>

src/Lean/Meta/Sym/Intro.lean

@@ -8,16 +8,15 @@ prelude
 public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.IsClass
-import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+import Lean.Meta.Sym.AlphaShareBuilder
 namespace Lean.Meta.Sym
-
+open Internal
 /--
 Efficient `intro` for symbolic simulation.
 -/
-def introCore (goal : Goal) (max : Nat) (names : Array Name) : SymM (Array FVarId × Goal) := do
-  if max == 0 then return (#[], goal)
+def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) : SymM (Array FVarId × MVarId) := do
+  if max == 0 then return (#[], mvarId)
   let env ← getEnv
-  let mvarId := goal.mvarId
   let mvarDecl ← mvarId.getDecl
   /-
   Helper function for constructing a value to assign to `mvarId`. We don't need max sharing here.
@@ -73,7 +72,7 @@ def introCore (goal : Goal) (max : Nat) (names : Array Name) : SymM (Array FVarI
       let type       ← instantiateRevS type fvars
       let fvarId     ← mkFreshFVarId
       let lctx       := lctx.mkLocalDecl fvarId (← mkName n i) type bi
-      let fvar       ← Grind.mkFVarS fvarId
+      let fvar       ← mkFVarS fvarId
       let fvars      := fvars.push fvar
       let localInsts := updateLocalInsts localInsts fvar type
       visit (i+1) lctx localInsts fvars body
@@ -87,13 +86,13 @@ def introCore (goal : Goal) (max : Nat) (names : Array Name) : SymM (Array FVarI
       **Note**: If `type` is a proposition we could use a `cdecl`.
       -/
       let lctx       := lctx.mkLetDecl fvarId (← mkName n i) type value
-      let fvar       ← Grind.mkFVarS fvarId
+      let fvar       ← mkFVarS fvarId
       let fvars      := fvars.push fvar
       let localInsts := updateLocalInsts localInsts fvar type
       visit (i+1) lctx localInsts fvars body
     | _ => finalize lctx localInsts fvars type
   let (fvars, mvarId') ← visit 0 mvarDecl.lctx mvarDecl.localInstances #[] mvarDecl.type
-  return (fvars.map (·.fvarId!), { goal with mvarId := mvarId' })
+  return (fvars.map (·.fvarId!), mvarId')
 
 def hugeNat := 1000000
 
@@ -107,11 +106,11 @@ Returns the introduced free variable Ids and the updated goal.
 
 Throws an error if the target type does not have a leading binder.
 -/
-public def intros (goal : Goal) (names : Array Name := #[]) : SymM (Array FVarId × Goal) := do
+public def intros (mvarId : MVarId) (names : Array Name := #[]) : SymM (Array FVarId × MVarId) := do
   let result ← if names.isEmpty then
-    introCore goal hugeNat #[]
+    introCore mvarId hugeNat #[]
   else
-    introCore goal names.size names
+    introCore mvarId  names.size names
   if result.1.isEmpty then
     throwError "`intros` failed, binder expected"
   return result
@@ -122,8 +121,8 @@ Introduces a single binder from the goal's target type with the given name.
 Returns the introduced free variable ID and the updated goal.
 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]
+public def intro (mvarId : MVarId) (name : Name) : SymM (FVarId × MVarId) := do
+  let (fvarIds, goal') ← introCore mvarId 1 #[name]
   if h : 0 < fvarIds.size then
     return (fvarIds[0], goal')
   else
@@ -135,8 +134,8 @@ Introduces exactly `num` binders from the goal's target type.
 Returns the introduced free variable IDs and the updated goal.
 Throws an error if the target type has fewer than `num` leading binders.
 -/
-public def introN (goal : Goal) (num : Nat) : SymM (Array FVarId × Goal) := do
-  let result ← introCore goal num #[]
+public def introN (mvarId : MVarId) (num : Nat) : SymM (Array FVarId × MVarId) := do
+  let result ← introCore mvarId num #[]
   unless result.1.size == num do
     throwError "`introN` failed, insufficient number of binders"
   return result

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
+open Internal
 /--
 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)`.

src/Lean/Meta/Sym/Main.lean

@@ -1,35 +0,0 @@
-/-
-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 import Lean.Meta.Sym.Util
-public import Lean.Meta.Tactic.Grind.Main
-public section
-namespace Lean.Meta.Sym
-open Grind (Params)
-
-def SymM.run (x : SymM α) (params : Params) : MetaM α := do
-  x params |>.run' {} |>.run params
-
-def SymM.run' (x : SymM α) (config : Grind.Config := {}) : MetaM α := do
-  let params ← Grind.mkDefaultParams config
-  x.run params
-
-/-- Creates a new goal using the given metavariable -/
-def mkGoal (mvarId : MVarId) : SymM Goal := do
-  let mvarId ← preprocessMVar mvarId
-  Grind.mkGoal mvarId
-
-/-- Internalizes the next `num` hypotheses into `grind`. -/
-def internalizeNumHypotheses (goal : Goal) (num : Nat) : SymM Goal := do
-  Grind.processHypotheses goal (some num)
-
-/-- Internalizes all pending hypotheses into `grind`. -/
-def internalizeAllHypotheses (goal : Goal) : SymM Goal := do
-  Grind.processHypotheses goal none
-
-end Lean.Meta.Sym

src/Lean/Meta/Sym/Pattern.lean

@@ -6,16 +6,18 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.SymM
+public import Lean.Data.AssocList
 import Lean.Util.FoldConsts
+import Lean.Meta.SynthInstance
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.AbstractS
 import Lean.Meta.Sym.InstantiateMVarsS
 import Lean.Meta.Sym.IsClass
 import Lean.Meta.Sym.MaxFVar
 import Lean.Meta.Sym.ProofInstInfo
-import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+import Lean.Meta.Sym.AlphaShareBuilder
 namespace Lean.Meta.Sym
-open Grind
+open Internal
 
 /-!
 This module implements efficient pattern matching and unification module for the symbolic simulation
@@ -235,8 +237,7 @@ partial def process (p : Expr) (e : Expr) : UnifyM Bool := do
     pushPending p e
     return true
   | .proj .. =>
-    reportIssue! "unexpected kernel projection term during unification/matching{indentExpr e}\npre-process and fold them as projection applications"
-    return false
+    throwError "unexpected kernel projection term during unification/matching{indentExpr e}\npre-process and fold them as projection applications"
   | .fvar _ =>
     /-
     **Note**: Most patterns do not have free variables since they are created from
@@ -606,10 +607,10 @@ def isDefEqMainImpl (t : Expr) (s : Expr) : DefEqM Bool := do
       return false
   | .bvar _, _ | _, .bvar _ => unreachable!
   | .proj .., _ | _, .proj .. =>
-    reportIssue! "unexpected kernel projection term during structural definitional equality{indentExpr t}\nand{indentExpr s}\npre-process and fold them as projection applications"
+    throwError "unexpected kernel projection term during structural definitional equality{indentExpr t}\nand{indentExpr s}\npre-process and fold them as projection applications"
     return false
   | .letE .., _ | _, .letE .. =>
-    reportIssue! "unexpected let-declaration term during structural definitional equality{indentExpr t}\nand{indentExpr s}\npre-process and zeta-reduce them"
+    throwError "unexpected let-declaration term during structural definitional equality{indentExpr t}\nand{indentExpr s}\npre-process and zeta-reduce them"
     return false
   | _, _ =>
     let tFn := t.getAppFn

src/Lean/Meta/Sym/ProofInstInfo.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.IsClass
+import Lean.Meta.Tactic.Grind.Util
 namespace Lean.Meta.Sym
 
 /--

src/Lean/Meta/Sym/ReplaceS.lean

@@ -6,16 +6,15 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.SymM
-public import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+public import Lean.Meta.Sym.AlphaShareBuilder
 namespace Lean.Meta.Sym
+open Internal
 /-!
 A version of `replace_fn.h` that ensures the resulting expression is maximally shared.
 -/
 open Grind
 abbrev M := StateT (Std.HashMap (ExprPtr × Nat) Expr) AlphaShareBuilderM
 
-export Grind (AlphaShareBuilderM liftBuilderM)
-
 def save (key : ExprPtr × Nat) (r : Expr) : M Expr := do
   modify fun cache => cache.insert key r
   return r

src/Lean/Meta/Sym/Simp/Congr.lean

@@ -6,12 +6,12 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
-import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.Simp.Result
 import Lean.Meta.Sym.Simp.CongrInfo
 namespace Lean.Meta.Sym.Simp
-open Grind
+open Internal
 
 /-!
 # Simplifying Application Arguments and Congruence Lemma Application

src/Lean/Meta/Sym/Simp/CongrInfo.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.SymM
+import Lean.Meta.FunInfo
 namespace Lean.Meta.Sym
 
 def isFixedPrefix? (argKinds : Array CongrArgKind) : Option Nat :=

src/Lean/Meta/Sym/Simp/DiscrTree.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Pattern
-import Lean.Meta.DiscrTree.Basic
+public import Lean.Meta.DiscrTree.Basic
 namespace Lean.Meta.Sym
 open DiscrTree
 

src/Lean/Meta/Sym/Simp/Main.lean

@@ -6,14 +6,14 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
-import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.Simp.Result
 import Lean.Meta.Sym.Simp.Simproc
 import Lean.Meta.Sym.Simp.Congr
 import Lean.Meta.Sym.Simp.Funext
 namespace Lean.Meta.Sym.Simp
-open Grind
+open Internal
 
 def simpLambda (e : Expr) : SimpM Result := do
   -- **TODO**: Add free variable reuse
@@ -52,8 +52,7 @@ def simpStep : Simproc := fun e => do
   match e with
   | .lit _ | .sort _ | .bvar _ | .const .. | .fvar _  | .mvar _ => return .rfl
   | .proj .. =>
-    reportIssue! "unexpected kernel projection term during simplification{indentExpr e}\npre-process and fold them as projection applications"
-    return .rfl
+    throwError "unexpected kernel projection term during simplification{indentExpr e}\npre-process and fold them as projection applications"
   | .mdata m b =>
     let r ← simp b
     match r with

src/Lean/Meta/Sym/Simp/Simproc.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Sym.Simp.Result
 namespace Lean.Meta.Sym.Simp
-open Grind
 
 public abbrev Simproc.andThen (f g : Simproc) : Simproc := fun e₁ => do
   let r ← f e₁

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Pattern
+public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
 public section
 namespace Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/SymM.lean

@@ -5,11 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Main
+public import Lean.Meta.Basic
+public import Lean.Meta.Sym.AlphaShareCommon
+public import Lean.Meta.CongrTheorems
 public section
 namespace Lean.Meta.Sym
-export Grind (ExprPtr Goal)
+
+register_builtin_option sym.debug : Bool := {
+  defValue := false
+  descr    := "check invariants"
+}
 
 /--
 Information about a single argument position in a function's type signature.
@@ -80,6 +85,8 @@ inductive CongrInfo where
 
 /-- Mutable state for the symbolic simulator framework. -/
 structure State where
+  /-- `ShareCommon` (aka `Hash-consing`) state. -/
+  share : AlphaShareCommon.State := {}
   /--
   Maps expressions to their maximal free variable (by declaration index).
 
@@ -111,7 +118,54 @@ structure State where
   -/
   getLevel : PHashMap ExprPtr Level := {}
   congrInfo : PHashMap ExprPtr CongrInfo := {}
+  debug : Bool := false
 
-abbrev SymM := ReaderT Grind.Params StateRefT State Grind.GrindM
+abbrev SymM := StateRefT State MetaM
+
+def SymM.run (x : SymM α) : MetaM α := do
+  let debug := sym.debug.get (← getOptions)
+  x |>.run' { debug }
+
+/--
+Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
+been hash-consed. We perform this step before we internalize expressions.
+-/
+def shareCommon (e : Expr) : SymM Expr := do
+  let share ← modifyGet fun s => (s.share, { s with share := {} })
+  let (e, share) := shareCommonAlpha e share
+  modify fun s => { s with share }
+  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) : SymM Expr := do
+  let share ← modifyGet fun s => (s.share, { s with share := {} })
+  let (e, share) := shareCommonAlphaInc e share
+  modify fun s => { s with share }
+  return e
+
+@[inherit_doc shareCommonInc]
+abbrev share (e : Expr) : SymM Expr :=
+  shareCommonInc e
+
+/-- Returns `true` if `sym.debug` is set -/
+@[inline] def isDebugEnabled : SymM Bool :=
+  return (← get).debug
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Util.lean

@@ -5,21 +5,20 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.SymM
 namespace Lean.Meta.Sym
 open Grind
-
 /--
-Instantiates metavariables and applies `shareCommon`.
+Instantiates metavariables, unfold reducible, and applies `shareCommon`.
 -/
-def preprocessExpr (e : Expr) : GrindM Expr := do
+def preprocessExpr (e : Expr) : SymM Expr := do
   shareCommon (← instantiateMVars e)
 
 /--
 Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.
 Gaps are `none` cells at `lctx.decls`. In `SymM`, we assume these cells don't exist.
 -/
-def preprocessLCtx (lctx : LocalContext) : GrindM LocalContext := do
+def preprocessLCtx (lctx : LocalContext) : SymM LocalContext := do
   let auxDeclToFullName := lctx.auxDeclToFullName
   let mut fvarIdToDecl := {}
   let mut decls := {}
@@ -41,7 +40,7 @@ def preprocessLCtx (lctx : LocalContext) : GrindM LocalContext := do
 Instantiates assigned metavariables, applies `shareCommon`, and eliminates holes (aka `none` cells)
 in the local context.
 -/
-public def preprocessMVar (mvarId : MVarId) : GrindM MVarId := do
+public def preprocessMVar (mvarId : MVarId) : SymM MVarId := do
   let mvarDecl ← mvarId.getDecl
   let lctx ← preprocessLCtx mvarDecl.lctx
   let type ← preprocessExpr mvarDecl.type

src/Lean/Meta/Tactic/Grind.lean

@@ -48,8 +48,6 @@ 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/Arith/Cutsat/Types.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Data.Int.Linear
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
-import Lean.Meta.Tactic.Grind.ExprPtr
+import Lean.Meta.Sym.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat

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

@@ -104,17 +104,20 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
   else
     return none
 
-def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := do
-  let (falseExpr, scState)  := shareCommonAlpha (mkConst ``False) {}
-  let (trueExpr, scState)   := shareCommonAlpha (mkConst ``True) scState
-  let (bfalseExpr, scState) := shareCommonAlpha (mkConst ``Bool.false) scState
-  let (btrueExpr, scState)  := shareCommonAlpha (mkConst ``Bool.true) scState
-  let (natZExpr, scState)   := shareCommonAlpha (mkNatLit 0) scState
-  let (ordEqExpr, scState)  := shareCommonAlpha (mkConst ``Ordering.eq) scState
-  let (intExpr, scState)    := shareCommonAlpha Int.mkType scState
-  let simprocs := params.normProcs
+open Sym
+
+def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := Sym.SymM.run do
+  let falseExpr  ← share <| mkConst ``False
+  let trueExpr   ← share <| mkConst ``True
+  let bfalseExpr ← share <| mkConst ``Bool.false
+  let btrueExpr  ← share <| mkConst ``Bool.true
+  let natZExpr   ← share <| mkNatLit 0
+  let ordEqExpr  ← share <| mkConst ``Ordering.eq
+  let intExpr    ← share <| Int.mkType
+  /- **Note**: Consider using `Sym.simp` in the future. -/
+  let simprocs  := params.normProcs
   let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
-  let simp := params.norm
+  let simp   := params.norm
   let config := params.config
   let symPrios := params.symPrios
   let extensions := params.extensions
@@ -124,7 +127,7 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti
     { config, anchorRefs?, simpMethods, simp, extensions, symPrios
       trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr
       debug }
-    |>.run' { scState }
+    |>.run' {}
 
 private def mkCleanState (mvarId : MVarId) : GrindM Clean.State := mvarId.withContext do
   let config ← getConfig

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

@@ -7,7 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Util
-import Lean.Meta.Tactic.Grind.ExprPtr
+import Lean.Meta.Sym.ExprPtr
 import Lean.Meta.Tactic.Grind.Util
 public section
 namespace Lean.Meta.Grind

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

@@ -5,13 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Sym.SymM
 public import Lean.Meta.Tactic.Simp.Types
-public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
 public import Lean.Meta.Tactic.Grind.CheckResult
 public import Lean.Meta.Tactic.Grind.Extension
 public import Init.Data.Queue
-import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.HeadIndex
 import Lean.Meta.Tactic.Grind.ExtAttr
 import Lean.Meta.AbstractNestedProofs
@@ -20,6 +19,7 @@ import Lean.PrettyPrinter
 meta import Lean.Parser.Do
 public section
 namespace Lean.Meta.Grind
+export Sym (isSameExpr hashPtrExpr ExprPtr shareCommon shareCommonInc)
 
 /-- We use this auxiliary constant to mark delayed congruence proofs. -/
 def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
@@ -203,8 +203,6 @@ structure SplitDiagInfo where
 
 /-- State for the `GrindM` monad. -/
 structure State where
-  /-- `ShareCommon` (aka `Hash-consing`) state. -/
-  scState    : AlphaShareCommon.State := {}
   /--
   Congruence theorems generated so far. Recall that for constant symbols
   we rely on the reserved name feature (i.e., `mkHCongrWithArityForConst?`).
@@ -248,7 +246,7 @@ private opaque MethodsRefPointed : NonemptyType.{0}
 def MethodsRef : Type := MethodsRefPointed.type
 instance : Nonempty MethodsRef := by exact MethodsRefPointed.property
 
-abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
+abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State Sym.SymM
 
 @[inline] def mapGrindM [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α} (x : m α) : m α :=
   controlAt GrindM fun runInBase => f <| runInBase x
@@ -414,44 +412,6 @@ Abstracts nested proofs in `e`. This is a preprocessing step performed before in
 def abstractNestedProofs (e : Expr) : GrindM Expr :=
   Meta.abstractNestedProofs e
 
-/--
-Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
-been hash-consed. We perform this step before we internalize expressions.
--/
-def shareCommon (e : Expr) : GrindM Expr := do
-  let scState ← modifyGet fun s => (s.scState, { s with scState := {} })
-  let (e, scState) := shareCommonAlpha e scState
-  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/bench/sym/simp_1.lean

@@ -18,7 +18,7 @@ def mkSimpMethods : MetaM Sym.Simp.Methods := do
   let thms := thms.insert thm
   return { post := thms.rewrite }
 
-def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run' do
+def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
   let e ← Grind.shareCommon e
   let methods ← mkSimpMethods
   let startTime ← IO.monoNanosNow

tests/bench/sym/simp_2.lean

@@ -18,7 +18,7 @@ def mkSimpMethods : MetaM Sym.Simp.Methods := do
   let thms := thms.insert thm
   return { post := thms.rewrite }
 
-def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run' do
+def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
   let e ← Grind.shareCommon e
   let methods ← mkSimpMethods
   let startTime ← IO.monoNanosNow

tests/lean/run/grind_alphaShare_builder.lean

@@ -1,9 +1,8 @@
-import Lean.Meta.Tactic.Grind
-import Lean.Meta.Sym.Main
-open Lean Meta Grind Sym
+import Lean.Meta.Sym
+open Lean Meta Sym Internal
 set_option grind.debug true
 
-def test : GrindM Unit := do
+def test : SymM Unit := do
   let f  ← mkConstS `f
   let f₁ := mkConst `f
   let f₂ ← mkConstS `f
@@ -20,5 +19,5 @@ def test : GrindM Unit := do
     ==
     (← mkLambdaS `y .default (← mkConstS ``Nat) (← mkMDataS {} (← mkProjS ``Prod 0 (← mkAppS f₂ x₂))))
 
-#eval SymM.run' do
+#eval SymM.run do
   test

tests/lean/run/sym_congrInfo.lean

@@ -27,7 +27,7 @@ info: @Eq.refl ↦ none
 info: @congrArg ↦ none
 -/
 #guard_msgs in
-run_meta SymM.run' do
+run_meta SymM.run do
   logCongrInfo <| mkConst ``HAdd.hAdd [0, 0, 0]
   logCongrInfo <| mkConst ``And
   logCongrInfo <| mkConst ``Eq [1]

tests/lean/run/sym_getMaxFVar.lean

@@ -1,7 +1,6 @@
 import Lean.Meta.Sym
-import Lean.Meta.Tactic.Grind.AlphaShareBuilder
-open Lean Meta Grind Sym
-
+open Lean Meta Sym
+open Internal
 def checkMaxFVar (e : Expr) (x : Expr) : SymM Unit := do
   let some fvarId ← getMaxFVar? e | unreachable!
   assert! x.fvarId! == fvarId
@@ -13,7 +12,7 @@ def test1 : MetaM Unit := do
   withLocalDeclD `y nat fun y => do
   let m₂ ← mkFreshExprMVar nat
   withLocalDeclD `z nat fun z => do
-  SymM.run' do
+  SymM.run do
   let x ← shareCommon x
   let y ← shareCommon y
   let z ← shareCommon z

tests/lean/run/sym_instantiate.lean

@@ -1,7 +1,7 @@
 import Lean.Meta.Sym
-set_option grind.debug true
-open Lean Meta Grind Sym
-
+set_option sym.debug true
+open Lean Meta Sym
+open Internal
 def tst1 : SymM Unit := do
   let f ← mkConstS `f
   let e ← mkAppS (← mkAppS (← mkAppS f (← mkBVarS 0)) (← mkBVarS 1)) (← shareCommon (mkNatLit 1))
@@ -31,7 +31,7 @@ info: fun x => f x b 1
 info: fun x => f x a 1
 -/
 #guard_msgs in
-#eval SymM.run' tst1
+#eval SymM.run tst1
 
 def tst2 : SymM Unit := do
   let f ← mkConstS `f
@@ -64,4 +64,4 @@ info: f #0 x w
 info: fun (x y : Nat) => f y x w
 -/
 #guard_msgs in
-#eval SymM.run' tst2
+#eval SymM.run tst2

tests/lean/run/sym_intro.lean

@@ -1,4 +1,4 @@
-import Lean.Meta.Sym
+import Lean
 
 macro "gen_term" n:num : term => do
   let mut stx ← `(True)
@@ -9,10 +9,9 @@ macro "gen_term" n:num : term => do
 open Lean Meta Sym Elab Tactic
 
 def test (mvarId : MVarId) : MetaM MVarId := do
-  SymM.run' do
-    let goal ← mkGoal mvarId
-    let (_, goal) ← intros goal
-    return goal.mvarId
+  SymM.run do
+    let (_, mvarId) ← intros mvarId
+    return mvarId
 
 /--
 trace: z✝² : Nat := 0

tests/lean/run/sym_intro_have.lean

@@ -16,14 +16,13 @@ y : Nat := x + 1
 ⊢ x ≤ 2 * y
 -/
 #guard_msgs in
-run_meta SymM.run' do
+run_meta SymM.run do
   withLocalDeclD `x Nat.mkType fun x => do
   let m ← mkFreshExprMVar <| mkNatLE x (mkApp (mkConst ``f) x)
   let mvarId := m.mvarId!
   let mvarId ← unfoldTarget mvarId ``f
   let mvarId ← mvarId.liftLets
-  let goal ← mkGoal mvarId
-  logInfo goal.mvarId
-  let (_, goal) ← intro goal `y
-  logInfo goal.mvarId
+  logInfo mvarId
+  let (_, mvarId) ← intro mvarId `y
+  logInfo mvarId
   return ()

tests/lean/run/sym_liftLower.lean

@@ -1,6 +1,6 @@
 import Lean.Meta.Sym
+open Lean Meta Sym Internal
 
-open Lean Meta Grind Sym
 
 def tst1 : SymM Unit := do
   let x1 ← mkBVarS 0
@@ -20,4 +20,4 @@ forall (x : Nat), f x #1
 forall (x : Nat), f x #0
 -/
 #guard_msgs in
-#eval SymM.run' tst1
+#eval SymM.run tst1

tests/lean/run/sym_pattern.lean

@@ -1,6 +1,6 @@
 import Lean.Meta.Sym
 open Lean Meta Sym Grind
-set_option grind.debug true
+set_option sym.debug true
 opaque p : Nat → Prop
 opaque q : Nat → Nat → Prop
 axiom pax : p x
@@ -27,7 +27,7 @@ info: @Eq.refl Nat Nat.zero
 -/
 #guard_msgs in
 set_option pp.explicit true in
-#eval SymM.run' test1
+#eval SymM.run test1
 
 def test2 : SymM Unit := do
   let ruleEx   ← mkBackwardRuleFromDecl ``Exists.intro
@@ -35,11 +35,11 @@ def test2 : SymM Unit := do
   let ruleRefl ← mkBackwardRuleFromDecl ``Eq.refl
   let rulePax  ← mkBackwardRuleFromDecl ``pax
   let mvar ← mkFreshExprMVar (← getConstInfo ``ex).value!
-  let goal ← Sym.mkGoal mvar.mvarId!
-  let [goal, _] ← ruleEx.apply goal | throwError "Failed"
-  let [goal₁, goal₂] ← ruleAnd.apply goal | throwError "Failed"
-  let [] ← rulePax.apply goal₁ | throwError "Failed"
-  let [] ← ruleRefl.apply goal₂ | throwError "Failed"
+  let mvarId ← preprocessMVar mvar.mvarId!
+  let [mvarId, _] ← ruleEx.apply mvarId | throwError "Failed"
+  let [mvarId₁, mvarId₂] ← ruleAnd.apply mvarId | throwError "Failed"
+  let [] ← rulePax.apply mvarId₁ | throwError "Failed"
+  let [] ← ruleRefl.apply mvarId₂ | throwError "Failed"
   logInfo mvar
 
 /--
@@ -48,7 +48,7 @@ info: @Exists.intro Nat (fun x => And (p x) (@Eq Nat x Nat.zero)) Nat.zero
 -/
 #guard_msgs in
 set_option pp.explicit true in
-#eval SymM.run' test2
+#eval SymM.run test2
 
 opaque a : Nat
 opaque bla : Nat → Nat → Nat
@@ -60,14 +60,14 @@ def test3 : SymM Unit := do
   withLetDecl `y (mkConst ``Nat) (mkNatLit 1) fun y => do
   let target := mkApp (mkConst ``p) (mkApp2 (mkConst ``foo) x (mkApp2 (mkConst ``bla) (mkNatAdd (mkNatLit 3) y) y))
   let mvar ← mkFreshExprMVar target
-  let goal ← Sym.mkGoal mvar.mvarId!
+  let mvarId ← preprocessMVar mvar.mvarId!
   let rule ← mkBackwardRuleFromDecl ``pFoo
-  let [] ← rule.apply goal | throwError "failed"
+  let [] ← rule.apply mvarId | throwError "failed"
   logInfo mvar
 
 /-- info: pFoo (3 + y) -/
 #guard_msgs in
-#eval SymM.run' test3
+#eval SymM.run test3
 
 def test4 : SymM Unit := do
   withLetDecl `x (.sort 1) (.sort 0) fun x =>
@@ -83,4 +83,4 @@ def test4 : SymM Unit := do
 
 /-- info: pFoo (3 + y) -/
 #guard_msgs in
-#eval SymM.run' test4
+#eval SymM.run test4

tests/lean/run/sym_pattern_2.lean

@@ -1,7 +1,8 @@
+import Std.Data.HashMap
 import Lean.Meta.Sym
 import Lean.Meta.DiscrTree.Basic
 open Lean Meta Sym Grind
-set_option grind.debug true
+set_option sym.debug true
 opaque p [Ring α] : α → α → Prop
 axiom pax [CommRing α] [NoNatZeroDivisors α] (x y : α) : p x y → p (y + 1) x
 opaque a : Int
@@ -23,7 +24,7 @@ info: pax b a ?m.1
 info: #[Int, instCommRingInt, instNoNatZeroDivisorsInt, b, a, ?m.1]
 -/
 #guard_msgs in
-#eval SymM.run' test₁
+#eval SymM.run test₁
 
 theorem mk_forall_and (P Q : α → Prop) : (∀ x, P x) → (∀ x, Q x) → (∀ x, P x ∧ Q x) := by
   grind
@@ -58,7 +59,7 @@ info: ∀ (x : Nat), q x 0
 info: ∀ (x : Nat), q (f (f x)) (f x + f (f 1))
 -/
 #guard_msgs in
-#eval SymM.run' test₂
+#eval SymM.run test₂
 
 theorem forall_and_eq (P Q : α → Prop) : (∀ x, P x ∧ Q x) = ((∀ x, P x) ∧ (∀ x, Q x)):= by
   grind
@@ -113,7 +114,7 @@ info: [Std.HashMap.insertMany,
 info: [GetElem.getElem, Std.HashMap, *, *, *, *, *, *, ◾, *, Std.HashMap.insert, *, *, *, *, *, *, *, *, *]
 -/
 #guard_msgs in
-#eval SymM.run' do
+#eval SymM.run do
   logPatternKeyFor ``Nat.zero_add
   logPatternKeyFor ``Grind.Semiring.zero_mul
   logPatternKeyFor ``forall_and_eq

tests/lean/sym/perf_sym_apply.lean

@@ -23,7 +23,7 @@ def genTerm (n : Nat) : Expr := Id.run do
 
 set_option maxRecDepth 10000000
 
-def tryIntros? (goals : List Goal) : SymM (Option (List Goal)) := do
+def tryIntros? (goals : List MVarId) : SymM (Option (List MVarId)) := do
   try
     let goal :: goals := goals | return none
     let (_, goal') ← intros goal
@@ -31,7 +31,7 @@ def tryIntros? (goals : List Goal) : SymM (Option (List Goal)) := do
   catch _ =>
     return none
 
-def tryApply? (rule : BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do
+def tryApply? (rule : BackwardRule) (goals : List MVarId) : SymM (Option (List MVarId)) := do
   let goal :: goals := goals | return none
   try
     let goals' ← rule.apply goal
@@ -39,7 +39,7 @@ def tryApply? (rule : BackwardRule) (goals : List Goal) : SymM (Option (List Goa
   catch _ =>
     return none
 
-def tryApplyAny? (rules : List BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do
+def tryApplyAny? (rules : List BackwardRule) (goals : List MVarId) : SymM (Option (List MVarId)) := do
   match rules with
   | [] => return none
   | rule :: rules =>
@@ -48,17 +48,17 @@ def tryApplyAny? (rules : List BackwardRule) (goals : List Goal) : SymM (Option
     else
       tryApplyAny? rules goals
 
-def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") <| SymM.run' do
+def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") <| SymM.run do
   let mvarId := (← mkFreshExprMVar type).mvarId!
   let rules ← [``Exists.intro, ``And.intro, ``Eq.refl, ``True.intro].mapM fun declName => mkBackwardRuleFromDecl declName
-  let goal ← mkGoal mvarId
+  let goal ← preprocessMVar mvarId
   discard <| go 10000000 rules [goal]
   return ()
 where
-  go (fuel : Nat) (rules : List BackwardRule) (goals : List Goal) : SymM Bool := do
+  go (fuel : Nat) (rules : List BackwardRule) (goals : List MVarId) : SymM Bool := do
     let fuel + 1 := fuel | throwError "out of fuel"
     let goal :: goals' := goals | return true
-    if (← goal.mvarId.isAssigned) then
+    if (← goal.isAssigned) then
       go fuel rules goals'
     else
       if let some goals' ← tryIntros? goals then
@@ -66,7 +66,7 @@ where
       else if let some goals' ← tryApplyAny? rules goals then
         go fuel rules goals'
       else
-        throwError "Stuck at {goal.mvarId}"
+        throwError "Stuck at {goal}"
 
 def test (n : Nat) : MetaM Unit := do
   let e := genTerm n