find* functions for Data.List

both decidable predicate and boolean function variants

Author: Saransh-cpp

CHANGELOG.md

@@ -2145,6 +2145,12 @@ 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) → (x : List A) → Maybe $ Fin (length x)
+  findIndicesᵇ : (A → Bool) → List A → List ℕ
+  find         : ∀ {P : Pred A p} → Decidable P → List A → Maybe A
+  findIndex    : ∀ {P : Pred A p} → Decidable P → (x : List A) → Maybe $ Fin (length x)
+  findIndices  : ∀ {P : Pred A p} → Decidable P → List A → List ℕ
   ```
 
 * 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,24 @@ deduplicateᵇ : (A → A → Bool) → List A → List A
 deduplicateᵇ r [] = []
 deduplicateᵇ r (x ∷ xs) = x ∷ filterᵇ (not ∘ r x) (deduplicateᵇ r xs)
 
+findᵇ : (A → Bool) → List A → Maybe A
+findᵇ p [] = nothing
+findᵇ p (x ∷ xs) = if p x then just x else findᵇ p xs
+
+findIndexᵇ : (A → Bool) → (x : List A) → Maybe $ Fin (length x)
+findIndexᵇ p [] = nothing
+findIndexᵇ p (x ∷ xs) = if p x
+  then just zero
+  else mapMaybe suc (findIndexᵇ p xs)
+
+findIndicesᵇ : (A → Bool) → List A → List ℕ
+findIndicesᵇ {A = A} p = h 0 where
+  h : ℕ → List A → List ℕ
+  h n [] = []
+  h n (x ∷ xs) = if p x
+    then n ∷ h (suc n) xs
+    else h (suc n) xs
+
 -- Equivalent functions that use a decidable predicate instead of a
 -- boolean function.
 
@@ -436,6 +455,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 → (x : List A) → Maybe $ Fin (length x)
+findIndex P? = findIndexᵇ (does ∘ P?)
+
+findIndices : ∀ {P : Pred A p} → Decidable P → List A → List ℕ
+findIndices P? = findIndicesᵇ (does ∘ P?)
+
 ------------------------------------------------------------------------
 -- Actions on single elements
 

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

@@ -11,7 +11,7 @@ module Data.List.Membership.Setoid.Properties where
 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.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)