From 0c7169efa9bdc3d30a2c3fe3fccc13c2e87eacea Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 12 Dec 2025 14:44:58 +0100
Subject: [PATCH] perf: more environment blocking avoidance (#11616)

---
 src/Lean/Meta/Structure.lean       |  2 +-
 src/Lean/Meta/Tactic/NormCast.lean |  2 +-
 src/Lean/MonadEnv.lean             | 37 ++++++++++++++++++++----------
 3 files changed, 27 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean
index 54baad73eb..3d278a796f 100644
--- a/src/Lean/Meta/Structure.lean
+++ b/src/Lean/Meta/Structure.lean
@@ -128,7 +128,7 @@ Each projection `x.i` can be either a native projection or from a projection fun
 -/
 def etaStruct? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do
   let .const ctor _ := e.getAppFn | return none
-  let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? ctor | return none
+  let some fVal ← isCtor? ctor | return none
   unless p fVal.induct do return none
   unless 0 < fVal.numFields && e.getAppNumArgs == fVal.numParams + fVal.numFields do return none
   let args := e.getAppArgs
diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean
index 3acd08df2b..b31c3d6cdd 100644
--- a/src/Lean/Meta/Tactic/NormCast.lean
+++ b/src/Lean/Meta/Tactic/NormCast.lean
@@ -145,7 +145,7 @@ be used by `norm_cast`.
 -/
 def addInfer (decl : Name)
     (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
-  let ty := (← getConstInfo decl).type
+  let ty := (← getConstVal decl).type
   match ← classifyType ty with
   | Label.elim => addElim decl kind prio
   | Label.squash => addSquash decl kind prio
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 1f01767990..7075b78fc7 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -104,29 +104,42 @@ def isInductive? [Monad m] [MonadEnv m] (declName : Name) : m (Option InductiveV
     | _ => unreachable!
   | _ => pure none
 
+def isDefn? [Monad m] [MonadEnv m] (constName : Name) : m (Option DefinitionVal) := do
+  match (← getEnv).findAsync? constName with
+  | some info@{ kind := .defn, .. } => match info.toConstantInfo with
+    | .defnInfo v => pure (some v)
+    | _ => unreachable!
+  | _ => pure none
+
+def isCtor? [Monad m] [MonadEnv m] (constName : Name) : m (Option ConstructorVal) := do
+  match (← getEnv).findAsync? constName with
+  | some info@{ kind := .ctor, .. } => match info.toConstantInfo with
+    | .ctorInfo v => pure (some v)
+    | _ => unreachable!
+  | _ => pure none
+
+def isRec? [Monad m] [MonadEnv m] (constName : Name) : m (Option RecursorVal) := do
+  match (← getEnv).findAsync? constName with
+  | some info@{ kind := .recursor, .. } => match info.toConstantInfo with
+    | .recInfo v => pure (some v)
+    | _ => unreachable!
+  | _ => pure none
+
 def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do
   let info ← getConstVal constName
   return mkConst constName (info.levelParams.map mkLevelParam)
 
 def getConstInfoDefn [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m DefinitionVal := do
-  match (← getConstInfo constName) with
-  | ConstantInfo.defnInfo v => pure v
-  | _                       => throwError "`{.ofConstName constName}` is not a definition"
+  (← inline <| isDefn? constName).getDM (throwError "`{.ofConstName constName}` is not a definition")
 
 def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do
-  match (← getConstInfo constName) with
-  | ConstantInfo.inductInfo v => pure v
-  | _                         => throwError "`{.ofConstName constName}` is not a inductive type"
+  (← inline <| isInductive? constName).getDM (throwError "`{.ofConstName constName}` is not an inductive type")
 
 def getConstInfoCtor [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstructorVal := do
-  match (← getConstInfo constName) with
-  | ConstantInfo.ctorInfo v => pure v
-  | _                       => throwError "`{.ofConstName constName}` is not a constructor"
+  (← inline <| isCtor? constName).getDM (throwError "`{.ofConstName constName}` is not a constructor")
 
 def getConstInfoRec [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m RecursorVal := do
-  match (← getConstInfo constName) with
-  | ConstantInfo.recInfo v => pure v
-  | _                      => throwError "`{.ofConstName constName}` is not a recursor"
+  (← inline <| isRec? constName).getDM (throwError "`{.ofConstName constName}` is not a recursor")
 
 /--
 Matches if `e` is a constant that is an inductive type with one constructor.