From 608be459e7cf44d1961658bdbbd281e02d282d74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Oct 2019 17:27:16 -0700 Subject: [PATCH] feat: add `anyM`, `allM`, `any`, and `all` --- library/Init/Data/PersistentArray/Basic.lean | 21 ++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean index a91a2d9786..a218747172 100644 --- a/library/Init/Data/PersistentArray/Basic.lean +++ b/library/Init/Data/PersistentArray/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Control.Conditional import Init.Data.Array universes u v w @@ -251,6 +252,26 @@ Id.run (t.mfoldlFrom f b ini) def toList (t : PersistentArray α) : List α := (t.foldl (fun xs x => x :: xs) []).reverse +section +variables {m : Type → Type w} [Monad m] +@[specialize] partial def anyMAux (p : α → m Bool) : PersistentArrayNode α → m Bool +| node cs => cs.anyM (fun c => anyMAux c) +| leaf vs => vs.anyM p + +@[specialize] def anyM (t : PersistentArray α) (p : α → m Bool) : m Bool := +anyMAux p t.root <||> t.tail.anyM p + +@[inline] def allM (a : PersistentArray α) (p : α → m Bool) : m Bool := +do b ← anyM a (fun v => do b ← p v; pure (not b)); pure (not b) + +end + +@[inline] def any (a : PersistentArray α) (p : α → Bool) : Bool := +Id.run $ anyM a p + +@[inline] def all (a : PersistentArray α) (p : α → Bool) : Bool := +!any a (fun v => !p v) + section variables {m : Type u → Type v} [Monad m] variable {β : Type u}