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

feat: add foldrRangeM

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-30 08:11:23 -08:00
parent 527c3c73b4
commit 16cb6fe759
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Data/Array/Basic.lean
View file

@ -343,6 +343,19 @@ iterateRevMAux a f a.size (Nat.leRefl _) b
@[inline] def foldrM (f : α → β → m β) (init : β) (a : Array α) : m β :=
iterateRevM a init (fun _ => f)
@[specialize] private def foldrRangeMAux (a : Array α) (f : α → β → m β) (beginIdx : Nat) : ∀ (i : Nat), i ≤ a.size → β → m β
| 0, h, b => pure b
| j+1, h, b => do
let i : Fin a.size := ⟨j, h⟩;
b ← f (a.get i) b;
if j == beginIdx then pure b else foldrRangeMAux j (Nat.leOfLt h) b
@[inline] def foldrRangeM (beginIdx endIdx : Nat) (f : α → β → m β) (ini : β) (a : Array α) : m β :=
if h : endIdx ≤ a.size then
foldrRangeMAux a f beginIdx endIdx h ini
else
foldrRangeMAux a f beginIdx a.size (Nat.leRefl _) ini
end
@[inline] def iterateRev {β} (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → β) : β :=
@ -351,6 +364,9 @@ Id.run $ iterateRevM a b f
@[inline] def foldr {β} (f : α → β → β) (init : β) (a : Array α) : β :=
Id.run $ foldrM f init a
@[inline] def foldrRange {β} (beginIdx endIdx : Nat) (f : α → β → β) (init : β) (a : Array α) : β :=
Id.run $ foldrRangeM beginIdx endIdx f init a
def toList (a : Array α) : List α :=
a.foldr List.cons []