From 63442ebde73ff312f37ddfcdffe20213c8b93ab0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Apr 2019 10:12:01 -0700 Subject: [PATCH] =?UTF-8?q?feat(library/init/data/array/basic):=20add=20`i?= =?UTF-8?q?terate=E2=82=82`=20and=20`foldl=E2=82=82`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- library/init/data/array/basic.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 6ce4d3d6a9..43f39001e9 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -133,6 +133,23 @@ miterate a b (λ _, f) @[inline] def mfoldlFrom (a : Array α) (b : β) (f : α → β → m β) (ini : Nat := 0) : m β := miterateAux a (λ _, f) ini b +-- TODO(Leo): justify termination using wf-rec +@[specialize] partial def miterate₂Aux (a₁ a₂ : Array α) (f : Π i : Fin a₁.size, α → α → β → m β) : Nat → β → m β +| i b := + if h₁ : i < a₁.size then + let idx₁ : Fin a₁.size := ⟨i, h₁⟩ in + if h₂ : i < a₂.size then + let idx₂ : Fin a₂.size := ⟨i, h₂⟩ in + f idx₁ (a₁.index idx₁) (a₂.index idx₂) b >>= miterate₂Aux (i+1) + else pure b + else pure b + +@[inline] def miterate₂ (a₁ a₂ : Array α) (b : β) (f : Π i : Fin a₁.size, α → α → β → m β) : m β := +miterate₂Aux a₁ a₂ f 0 b + +@[inline] def mfoldl₂ (a₁ a₂ : Array α) (b : β) (f : α → α → β → m β) : m β := +miterate₂ a₁ a₂ b (λ _, f) + local attribute [instance] monadInhabited -- TODO(Leo): justify termination using wf-rec @@ -160,6 +177,12 @@ iterate a b (λ _, f) @[inline] def foldlFrom (a : Array α) (f : α → β → β) (b : β) (ini : Nat := 0) : β := Id.run $ mfoldlFrom a b f ini +@[inline] def iterate₂ (a₁ a₂ : Array α) (b : β) (f : Π i : Fin a₁.size, α → α → β → β) : β := +Id.run $ miterate₂Aux a₁ a₂ f 0 b + +@[inline] def foldl₂ (a₁ a₂ : Array α) (f : α → α → β → β) (b : β) : β := +iterate₂ a₁ a₂ b (λ _, f) + @[inline] def find (a : Array α) (f : α → Option β) : Option β := Id.run $ mfindAux a f 0