perf: use inShareCommon to skip preprocessing steps (#9351)

This PR optimizes the `grind` preprocessing steps by skipping steps when
the term is already present in the hash-consing table.

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean

@@ -86,7 +86,6 @@ private partial def natToInt' (e : Expr) : GoalM (Expr × Expr) := do
       -- nested instances to be marked and canonicalized
       let r ← simpCore r
       let h ← if let some h' := r.proof? then mkEqTrans h h' else pure h
-      -- TODO: we need a more efficient `markNestedSubsingleton
       let r ← markNestedSubsingletons r.expr
       return (r, h)
     else

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

@@ -163,6 +163,7 @@ partial def canon (e : Expr) : GoalM Expr := do profileitM Exception "grind cano
 where
   visit (e : Expr) : StateRefT (Std.HashMap ExprPtr Expr) GoalM Expr := do
     unless e.isApp || e.isForall do return e
+    if (← inShareCommon e) then return e
     -- Check whether it is cached
     if let some r := (← get).get? { expr := e } then
       return r

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

@@ -11,10 +11,11 @@ import Lean.Meta.Basic
 import Lean.Meta.InferType
 import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Types
 
 namespace Lean.Meta.Grind
 
-private abbrev M := StateRefT (Std.HashMap ExprPtr Expr) MetaM
+private abbrev M := StateRefT (Std.HashMap ExprPtr Expr) GrindM
 
 def isMarkedSubsingletonConst (e : Expr) : Bool := Id.run do
   let .const declName _ := e | false
@@ -35,10 +36,11 @@ Recall that the congruence closure module has special support for them.
 -/
 -- TODO: consider other subsingletons in the future? We decided to not support them to avoid the overhead of
 -- synthesizing `Subsingleton` instances.
-partial def markNestedSubsingletons (e : Expr) : MetaM Expr := do
+partial def markNestedSubsingletons (e : Expr) : GrindM Expr := do
   visit e |>.run' {}
 where
   visit (e : Expr) : M Expr := do
+    if (← inShareCommon e) then return e
     if isMarkedSubsingletonApp e then
       return e -- `e` is already marked
     -- check whether result is cached
@@ -110,7 +112,7 @@ def markNestedProof (e : Expr) : M Expr := do
 /--
 Given a proof `e`, mark it with `Lean.Grind.nestedProof`
 -/
-def markProof (e : Expr) : MetaM Expr := do
+def markProof (e : Expr) : GrindM Expr := do
   if e.isAppOf ``Grind.nestedProof then
     return e -- `e` is already marked
   else

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

@@ -19,7 +19,11 @@ namespace Lean.Meta.Grind
 def simpCore (e : Expr) : GrindM Simp.Result := do profileitM Exception "grind simp" (← getOptions) do
   let simp ← modifyGet fun s => (s.simp, { s with simp := {} })
   let ctx := (← readThe Context).simp
-  let (r, simp) ← Simp.mainCore e ctx simp (methods := (← readThe Context).simpMethods)
+  let m := (← get).scState.map
+  let skipIfInShareCommon : Simp.Simproc := fun e => if m.contains { expr := e } then return .done { expr := e } else return .continue
+  let methods := (← readThe Context).simpMethods
+  let methods := { methods with pre := skipIfInShareCommon >> methods.pre }
+  let (r, simp) ← Simp.mainCore e ctx simp (methods := methods)
   modify fun s => { s with simp }
   return r
 

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

@@ -327,6 +327,16 @@ def shareCommon (e : Expr) : GrindM Expr := do
   modify fun s => { s with scState }
   return e
 
+/--
+Returns `true` if `e` has already been hash-consed.
+Recall that we use `shareCommon` as the last step of the preprocessing
+function `preprocess`.
+Later, we create terms using new terms that have already been preprocessed,
+and we skip preprocessing steps by checking whether `inShareCommon` returns `true`
+-/
+def inShareCommon (e : Expr) : GrindM Bool := do
+  return (← get).scState.map.contains { expr := e }
+
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
   return isSameExpr e (← getTrueExpr)

tests/lean/run/grind_getLast_dropLast.lean

@@ -9,5 +9,4 @@ theorem getLast?_dropLast {xs : List α} :
   grind (splits := 23) only [List.getElem?_eq_none, List.getElem?_reverse, getLast?_eq_getElem?,
     List.head?_eq_getLast?_reverse, getElem?_dropLast, List.getLast?_reverse, List.length_dropLast,
     List.length_reverse, length_nil, List.reverse_reverse, head?_nil, List.getElem?_eq_none,
-    getLast?_nil, List.head?_reverse, List.getLast?_eq_head?_reverse,
-    → List.eq_nil_of_length_eq_zero, = List.getElem?_nil, reverse_nil, cases Or]
+    getLast?_nil, List.head?_reverse, List.getLast?_eq_head?_reverse, = List.getElem?_nil, reverse_nil, cases Or]