From 0a031fc9bbb43c274bb400f121b13711e803f56c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Dec 2022 05:17:23 -0800 Subject: [PATCH] chore: replace `Expr.forEach` with `Expr.forEachWhere` --- src/Lean/Compiler/LCNF/Closure.lean | 8 +++----- src/Lean/Elab/Deriving/Inhabited.lean | 12 ++++++------ src/Lean/Elab/Inductive.lean | 17 +++++++++-------- src/Lean/Elab/Match.lean | 8 ++++---- src/Lean/Elab/PreDefinition/Eqns.lean | 11 ++++++----- src/Lean/Expr.lean | 7 +++++-- src/Lean/Meta/Match/Basic.lean | 4 ++++ src/Lean/Meta/Tactic/Util.lean | 6 ++---- 8 files changed, 39 insertions(+), 34 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean index 7a417aad96..788e99f61b 100644 --- a/src/Lean/Compiler/LCNF/Closure.lean +++ b/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 diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 2ffab264e5..90a5956a5d 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/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 diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 2e5e22a1cd..f3d98d0587 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index b4d9883d85..8d7ad71fb8 100644 --- a/src/Lean/Elab/Match.lean +++ b/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 /-- diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index a419993c3b..ce6d9e2fbb 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/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) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 629348f10c..e83b7ff970 100644 --- a/src/Lean/Expr.lean +++ b/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 diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index 8a7109ce18..16dd830117 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index 278cbf4381..cc2e010278 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/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