chore: replace Expr.forEach with Expr.forEachWhere

src/Lean/Compiler/LCNF/Closure.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Util.ForEachExpr
+import Lean.Util.ForEachExprWhere
 import Lean.Compiler.LCNF.CompilerM
 
 namespace Lean.Compiler.LCNF
@@ -141,10 +141,8 @@ mutual
 
   /-- Collect dependencies of the given expression. -/
   partial def collectType (type : Expr) : ClosureM Unit := do
-    type.forEach fun e => do
-      match e with
-      | .fvar fvarId => collectFVar fvarId
-      | _ => pure ()
+    type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
+
 end
 
 def run (x : ClosureM α) (inScope : FVarId → Bool) (abstract : FVarId → Bool := fun _ => true) : CompilerM (α × Array Param × Array CodeDecl) := do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.ForEachExprWhere
 import Lean.Elab.Deriving.Basic
 
 namespace Lean.Elab
@@ -47,12 +48,11 @@ where
       usedInstIdxs
     else
       let visit {ω} : StateRefT IndexSet (ST ω) Unit :=
-        e.forEach fun
-          | Expr.fvar fvarId =>
-            match localInst2Index.find? fvarId with
-            | some idx => modify (·.insert idx)
-            | none => pure ()
-          | _ => pure ()
+        e.forEachWhere Expr.isFVar fun e =>
+          let fvarId := e.fvarId!
+          match localInst2Index.find? fvarId with
+          | some idx => modify (·.insert idx)
+          | none => pure ()
       runST (fun _ => visit |>.run usedInstIdxs) |>.2
 
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters

src/Lean/Elab/Inductive.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.ForEachExprWhere
 import Lean.Util.ReplaceLevel
 import Lean.Util.ReplaceExpr
 import Lean.Util.CollectLevelParams
@@ -679,15 +680,15 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
               maskRef.modify fun mask => mask.set! i false
           for x in xs[numParams:] do
             let xType ← inferType x
-            xType.forEach fun e => do
-              if indFVars.any (fun indFVar => e.getAppFn == indFVar) && e.getAppNumArgs > numParams then
-                let eArgs := e.getAppArgs
-                for i in [numParams:eArgs.size] do
-                  if i >= typeArgs.size then
+            let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar) && e.getAppNumArgs > numParams
+            xType.forEachWhere cond fun e => do
+              let eArgs := e.getAppArgs
+              for i in [numParams:eArgs.size] do
+                if i >= typeArgs.size then
+                  maskRef.modify (resetMaskAt · i)
+                else
+                  unless eArgs[i]! == typeArgs[i]! do
                     maskRef.modify (resetMaskAt · i)
-                  else
-                    unless eArgs[i]! == typeArgs[i]! do
-                      maskRef.modify (resetMaskAt · i)
         go ctors
     go indType.ctors
 

src/Lean/Elab/Match.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.ForEachExprWhere
 import Lean.Meta.Match.Match
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.ForEachExpr
@@ -408,10 +409,9 @@ private def mkPatternRefMap (e : Expr) : ExprMap Expr :=
 where
   go (σ) : ST σ (ExprMap Expr) := do
    let map : ST.Ref σ (ExprMap Expr) ← ST.mkRef {}
-   e.forEach fun e => do
-     match patternWithRef? e with
-     | some (_, b) => map.modify (·.insert b e)
-     | none => return ()
+   e.forEachWhere isPatternWithRef fun e => do
+     let some (_, b) := patternWithRef? e | unreachable!
+     map.modify (·.insert b e)
    map.get
 
 /--

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Eqns
 import Lean.Util.CollectFVars
+import Lean.Util.ForEachExprWhere
 import Lean.Meta.Tactic.Split
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Refl
@@ -139,11 +140,11 @@ where
   collect (e : Expr) : FVarIdSet :=
     let go (e : Expr) (ω) : ST ω FVarIdSet := do
       let ref ← ST.mkRef {}
-      e.forEach fun e => do
-        if let some e := Match.isNamedPattern? e then
-          let arg := e.appArg!.consumeMData
-          if arg.isFVar then
-            ST.Prim.Ref.modify ref (·.insert arg.fvarId!)
+      e.forEachWhere Match.isNamedPattern fun e => do
+        let some e := Match.isNamedPattern? e | unreachable!
+        let arg := e.appArg!.consumeMData
+        if arg.isFVar then
+          ST.Prim.Ref.modify ref (·.insert arg.fvarId!)
       ST.Prim.Ref.get ref
     runST (go e)
 

src/Lean/Expr.lean

@@ -1698,11 +1698,14 @@ are annotated with `Syntax` objects. This function returns `some (stx, p')` if
 -/
 def patternWithRef? (p : Expr) : Option (Syntax × Expr) :=
   match p with
-  | Expr.mdata d _ =>
+  | .mdata d _ =>
     match d.find patternRefAnnotationKey with
     | some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!)
     | _ => none
-  | _                => none
+  | _ => none
+
+def isPatternWithRef (p : Expr) : Bool :=
+  patternWithRef? p |>.isSome
 
 /--
 Annotate the pattern `p` with `stx`. This is an auxiliary annotation

src/Lean/Meta/Match/Basic.lean

@@ -13,6 +13,10 @@ namespace Lean.Meta.Match
 def mkNamedPattern (x h p : Expr) : MetaM Expr :=
   mkAppM ``namedPattern #[x, p, h]
 
+def isNamedPattern (e : Expr) : Bool :=
+  let e := e.consumeMData
+  e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern
+
 def isNamedPattern? (e : Expr) : Option Expr :=
   let e := e.consumeMData
   if e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern then

src/Lean/Meta/Tactic/Util.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Util.ForEachExpr
+import Lean.Util.ForEachExprWhere
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.PPGoal
@@ -97,9 +97,7 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
   let removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do
     let e ← instantiateMVars e
     let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do
-      e.forEach fun
-        | Expr.fvar fvarId => modify fun s => s.erase fvarId
-        | _ => pure ()
+      e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId!
       get
     visit |>.run' candidates
   mvarId.withContext do