From e5bed9f4013508de2519c5e69be3591d94f96484 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 3 Aug 2023 12:42:31 -0400
Subject: [PATCH 1/5] `find*` functions for `Data.List`

both decidable predicate and boolean function variants
---
 CHANGELOG.md                                  |  6 ++++
 src/Data/List/Base.agda                       | 30 ++++++++++++++++++-
 .../List/Membership/Setoid/Properties.agda    |  2 +-
 .../Binary/Subset/Setoid/Properties.agda      |  2 +-
 .../List/Relation/Unary/Any/Properties.agda   |  2 +-
 src/Function/Base.agda                        |  2 +-
 6 files changed, 39 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3818f1a6f7..728907102a 100644
--- a/CHANGELOG.md
+++ b/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`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 2b25ece003..13050a6e06 100644
--- a/src/Data/List/Base.agda
+++ b/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
 
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 47768eed76..f741d3736f 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/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
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 2a700e468f..293108a19b 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/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
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6a0020d269..e799bcf3ae 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/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)
diff --git a/src/Function/Base.agda b/src/Function/Base.agda
index 69ab60bed0..9bdb996dc8 100644
--- a/src/Function/Base.agda
+++ b/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)

From b2c9e8951dbe3d603c34f66a463b0eaf346c3d65 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 3 Aug 2023 12:58:48 -0400
Subject: [PATCH 2/5] Back to `Maybe.map`

---
 src/Data/List/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 13050a6e06..a2a9e712d7 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -404,7 +404,7 @@ 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)
+  else Maybe.map suc (findIndexᵇ p xs)
 
 findIndicesᵇ : (A → Bool) → List A → List ℕ
 findIndicesᵇ {A = A} p = h 0 where

From 1bf08895c611bca52505e0f93f716bbb7401de01 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 22 Aug 2023 20:37:26 -0400
Subject: [PATCH 3/5] New type for findIndices

---
 CHANGELOG.md            | 11 ++++++-----
 src/Data/List/Base.agda | 23 +++++++++++------------
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9553825e78..895d9684f8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2169,12 +2169,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) → (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 ℕ
+  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`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index a2a9e712d7..e7b4f7d80d 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -397,22 +397,21 @@ 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 []       = 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ᵇ : (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)
 
-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
+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.
@@ -458,10 +457,10 @@ 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 : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs)
 findIndex P? = findIndexᵇ (does ∘ P?)
 
-findIndices : ∀ {P : Pred A p} → Decidable P → List A → List ℕ
+findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs)
 findIndices P? = findIndicesᵇ (does ∘ P?)
 
 ------------------------------------------------------------------------

From 215471843e3ff1349343ef4f21fab7ebeed24925 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 31 Aug 2023 00:28:25 +0530
Subject: [PATCH 4/5] Add comments

---
 src/Data/List/Base.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index e7b4f7d80d..61ab719e11 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -396,16 +396,19 @@ 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

From 223b1dfa83220fc37dfce6ef2edf2ba74c5e70e4 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 31 Aug 2023 10:39:32 +0530
Subject: [PATCH 5/5] Respect style guide

---
 src/Data/List/Base.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 61ab719e11..9817cf8648 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -396,19 +396,19 @@ 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
+-- 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
+-- 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
+-- 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