Add find, findIndex, and findIndices for Data.List (#2042)

* `find*` functions for `Data.List`

both decidable predicate and boolean function variants

* Back to `Maybe.map`

* New type for findIndices

* Add comments

* Respect style guide

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: 2 people

CHANGELOG.md

@@ -2173,6 +2173,13 @@ Other minor changes
   wordsByᵇ     : (A → Bool) → List A → List (List A)
   derunᵇ       : (A → A → Bool) → List A → List A
   deduplicateᵇ : (A → A → Bool) → List A → List A
+
+  findᵇ        : (A → Bool) → List A -> Maybe A
+  findIndexᵇ   : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs)
+  findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs)
+  find         : Decidable P → List A → Maybe A
+  findIndex    : Decidable P → (xs : List A) → Maybe $ Fin (length xs)
+  findIndices  : Decidable P → (xs : List A) → List $ Fin (length xs)
   ```
 
 * Added new functions and definitions to `Data.List.Base`:

src/Data/List/Base.agda

@@ -20,7 +20,8 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s
 open import Data.Product.Base as Prod using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
-open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
+open import Function.Base
+  using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (does; ¬?)
 open import Relation.Unary using (Pred; Decidable)
@@ -395,6 +396,26 @@ deduplicateᵇ : (A → A → Bool) → List A → List A
 deduplicateᵇ r [] = []
 deduplicateᵇ r (x ∷ xs) = x ∷ filterᵇ (not ∘ r x) (deduplicateᵇ r xs)
 
+-- Finds the first element satisfying the boolean predicate
+findᵇ : (A → Bool) → List A → Maybe A
+findᵇ p []       = nothing
+findᵇ p (x ∷ xs) = if p x then just x else findᵇ p xs
+
+-- Finds the index of the first element satisfying the boolean predicate
+findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs)
+findIndexᵇ p []       = nothing
+findIndexᵇ p (x ∷ xs) = if p x
+  then just zero
+  else Maybe.map suc (findIndexᵇ p xs)
+
+-- Finds indices of all the elements satisfying the boolean predicate
+findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs)
+findIndicesᵇ p []       = []
+findIndicesᵇ p (x ∷ xs) = if p x
+  then zero ∷ indices
+  else indices
+    where indices = map suc (findIndicesᵇ p xs)
+
 -- Equivalent functions that use a decidable predicate instead of a
 -- boolean function.
 
@@ -436,6 +457,15 @@ derun R? = derunᵇ (does ∘₂ R?)
 deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A
 deduplicate R? = deduplicateᵇ (does ∘₂ R?)
 
+find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A
+find P? = findᵇ (does ∘ P?)
+
+findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs)
+findIndex P? = findIndexᵇ (does ∘ P?)
+
+findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs)
+findIndices P? = findIndicesᵇ (does ∘ P?)
+
 ------------------------------------------------------------------------
 -- Actions on single elements
 

src/Data/List/Membership/Setoid/Properties.agda

@@ -12,7 +12,7 @@ open import Algebra using (Op₂; Selective)
 open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Fin.Properties using (suc-injective)
-open import Data.List.Base
+open import Data.List.Base hiding (find)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Relation.Unary.All as All using (All)
 import Data.List.Relation.Unary.Any.Properties as Any

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -9,7 +9,7 @@
 module Data.List.Relation.Binary.Subset.Setoid.Properties where
 
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.List.Base hiding (_∷ʳ_)
+open import Data.List.Base hiding (_∷ʳ_; find)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Relation.Unary.All as All using (All)
 import Data.List.Membership.Setoid as Membership

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List
+open import Data.List.Base as List hiding (find)
 open import Data.List.Properties using (ʳ++-defn)
 open import Data.List.Effectful as Listₑ using (monad)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)

src/Function/Base.agda

@@ -72,7 +72,7 @@ flip f = λ y x → f x y
 
 -- Application - note that _$_ is right associative, as in Haskell.
 -- If you want a left associative infix application operator, use
--- Category.Functor._<$>_ from Category.Monad.Identity.IdentityMonad.
+-- RawFunctor._<$>_ from Effect.Functor.
 
 _$_ : ∀ {A : Set a} {B : A → Set b} →
       ((x : A) → B x) → ((x : A) → B x)