From bcc6fb54c2081153a4e8221d4591fad65f394f22 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2025 21:53:49 -0700 Subject: [PATCH] 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 | 1 - src/Lean/Meta/Tactic/Grind/Canon.lean | 1 + .../Meta/Tactic/Grind/MarkNestedSubsingletons.lean | 8 +++++--- src/Lean/Meta/Tactic/Grind/Simp.lean | 6 +++++- src/Lean/Meta/Tactic/Grind/Types.lean | 10 ++++++++++ tests/lean/run/grind_getLast_dropLast.lean | 3 +-- 6 files changed, 22 insertions(+), 7 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean index 6576a1ca2f..f7a77fb3c0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 4cb432bcbe..ca486bd1b9 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean index cc4c6911f3..2c3d40c009 100644 --- a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean index b25881b80a..8190cbad0f 100644 --- a/src/Lean/Meta/Tactic/Grind/Simp.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 279c257ebf..84a041f9c7 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/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) diff --git a/tests/lean/run/grind_getLast_dropLast.lean b/tests/lean/run/grind_getLast_dropLast.lean index 3254f0bfa0..e01620e5b5 100644 --- a/tests/lean/run/grind_getLast_dropLast.lean +++ b/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]