From beb923c79fe663e707cd19af19d8990f3f5da1e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Nov 2022 08:13:51 -0700 Subject: [PATCH] chore: `anyFVar` and `allFVar` --- src/Lean/Compiler/LCNF/FVarUtil.lean | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/Lean/Compiler/LCNF/FVarUtil.lean b/src/Lean/Compiler/LCNF/FVarUtil.lean index 26dd03ade8..7c0ae7415a 100644 --- a/src/Lean/Compiler/LCNF/FVarUtil.lean +++ b/src/Lean/Compiler/LCNF/FVarUtil.lean @@ -192,19 +192,21 @@ instance : TraverseFVar Alt where | .default c => Code.forFVarM f c def anyFVarM [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool := do - let (_, res) ← TraverseFVar.forFVarM go x |>.run false - return res + return (← TraverseFVar.forFVarM go x |>.run) matches none where - -- TODO: StateRefT, early return? - go (fvar : FVarId) : StateT Bool m Unit := do - if (← f fvar) then set true + go (fvar : FVarId) : OptionT m Unit := do + if (← f fvar) then failure def allFVarM [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool := do - let (_, res) ← TraverseFVar.forFVarM go x |>.run true - return res + return (← TraverseFVar.forFVarM go x |>.run) matches .some .. where - -- TODO: StateRefT, early return? - go (fvar : FVarId) : StateT Bool m Unit := do - if !(← f fvar) then set false + go (fvar : FVarId) : OptionT m Unit := do + if !(← f fvar) then failure + +def anyFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool := + Id.run <| anyFVarM f x + +def allFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool := + Id.run <| allFVarM f x end Lean.Compiler.LCNF