From df84868ab4735832add512baee5e5e3488c22dac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Apr 2019 09:58:36 -0700
Subject: [PATCH] feat(library/init/data/array/basic): array helper functions

---
 library/init/data/array/basic.lean           | 40 ++++++++++++++++++++
 tests/compiler/array_test2.lean              | 15 ++++++++
 tests/compiler/array_test2.lean.expected.out |  0
 3 files changed, 55 insertions(+)
 create mode 100644 tests/compiler/array_test2.lean
 create mode 100644 tests/compiler/array_test2.lean.expected.out

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 714f39bbd6..6ce4d3d6a9 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -163,6 +163,21 @@ Id.run $ mfoldlFrom a b f ini
 @[inline] def find (a : Array α) (f : α → Option β) : Option β :=
 Id.run $ mfindAux a f 0
 
+@[specialize] partial def anyAux (a : Array α) (p : α → Bool) : Nat → Bool
+| i :=
+  if h : i < a.size then
+     let idx : Fin a.size := ⟨i, h⟩ in
+     match p (a.index idx) with
+     | true  := true
+     | false := anyAux (i+1)
+  else false
+
+@[inline] def any (a : Array α) (p : α → Bool) : Bool :=
+anyAux a p 0
+
+@[inline] def all (a : Array α) (p : α → Bool) : Bool :=
+!any a (λ v, !p v)
+
 @[specialize] private def revIterateAux (a : Array α) (f : Π i : Fin a.size, α → β → β) : Π (i : Nat), i ≤ a.size → β → β
 | 0     h b := b
 | (j+1) h b :=
@@ -240,6 +255,31 @@ let r : Array α := mkEmpty (e - b) in
 if h : e ≤ a.size then extractAux a b e h r
 else r
 
+@[inline] protected def append (a : Array α) (b : Array α) : Array α :=
+b.foldl (λ v a, a.push v) a
+
+instance : HasAppend (Array α) := ⟨Array.append⟩
+
+-- TODO(Leo): justify termination using wf-rec
+partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) : Nat → Bool
+| i :=
+  if h : i < a.size then
+     let aidx : Fin a.size := ⟨i, h⟩ in
+     let bidx : Fin b.size := ⟨i, hsz ▸ h⟩ in
+     match p (a.index aidx) (b.index bidx) with
+     | true  := isEqvAux (i+1)
+     | false := false
+  else
+    true
+
+@[specialize] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
+if h : a.size = b.size then
+  isEqvAux a b h p 0
+else
+  false
+
+instance [HasBeq α] : HasBeq (Array α) :=
+⟨λ a b, isEqv a b (==)⟩
 end Array
 
 export Array (mkArray)
diff --git a/tests/compiler/array_test2.lean b/tests/compiler/array_test2.lean
new file mode 100644
index 0000000000..df9c14ee0c
--- /dev/null
+++ b/tests/compiler/array_test2.lean
@@ -0,0 +1,15 @@
+def check (b : Bool) : IO Unit :=
+unless b $ IO.println "failed"
+
+
+def main : IO Unit :=
+let a1 := [2, 3, 5].toArray in
+let a2 := [4, 7, 9].toArray in
+let a3 := [4, 7, 8].toArray in
+do
+ check (Array.isEqv a1 a2 (λ v w, v % 2 == w % 2)),
+ check (!Array.isEqv a1 a3 (λ v w, v % 2 == w % 2)),
+ check (a1 ++ a2 == [2, 3, 5, 4, 7, 9].toArray),
+ check (a1.any (>4)),
+ check (!a1.any (>10)),
+ check (a1.all (<10))
diff --git a/tests/compiler/array_test2.lean.expected.out b/tests/compiler/array_test2.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2