From 131cb7036f3248972da554d15bfd5d9870633b87 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 28 Oct 2020 19:49:38 -0700
Subject: [PATCH] feat: add combinators for `Subarray`

---
 src/Init/Data/Array/Basic.lean    |  8 +++----
 src/Init/Data/Array/Subarray.lean | 40 +++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 0388f51b0d..9850d33195 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -388,6 +388,10 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
   else
     any as.size (Nat.leRefl _)
 
+@[inline]
+def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := do
+  return !(← as.anyM fun v => do return !(← p v))
+
 @[inline]
 def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
@@ -406,10 +410,6 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
 def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) :=
   as.findSomeRevM? fun a => do return if (← p a) then some a else none
 
-@[inline]
-def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := do
-  return !(← as.anyM fun v => do return !(← p v))
-
 @[inline]
 def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 0e651cb62f..b885d17863 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -34,6 +34,46 @@ namespace Subarray
 constant forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   pure b
 
+@[inline]
+def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
+  as.as.foldlM f (init := init) (start := as.start) (stop := as.stop)
+
+@[inline]
+def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β :=
+  as.as.foldrM f (init := init) (start := as.stop) (stop := as.start)
+
+@[inline]
+def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
+  as.as.anyM p (start := as.start) (stop := as.stop)
+
+@[inline]
+def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
+  as.as.allM p (start := as.start) (stop := as.stop)
+
+@[inline]
+def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
+  as.as.forM f (start := as.start) (stop := as.stop)
+
+@[inline]
+def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
+  as.as.forRevM f (start := as.stop) (stop := as.start)
+
+@[inline]
+def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
+  Id.run $ as.foldlM f (init := init)
+
+@[inline]
+def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
+  Id.run $ as.foldrM f (init := init)
+
+@[inline]
+def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
+  Id.run $ as.anyM p
+
+@[inline]
+def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
+  Id.run $ as.allM p
+
 end Subarray
 
 namespace Array