max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: anyFVar and allFVar

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-04 08:13:51 -07:00
parent eaade5abde
commit beb923c79f
1 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Lean/Compiler/LCNF/FVarUtil.lean
View file

@ -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