Skip to content

Commit c697cc3

Browse files
committed
"\find*\ functions for \Data.List\"
both decidable predicate and boolean function variants
1 parent bfa4f8b commit c697cc3

File tree

6 files changed

+39
-5
lines changed

6 files changed

+39
-5
lines changed

CHANGELOG.md

+6
Original file line numberDiff line numberDiff line change
@@ -2145,6 +2145,12 @@ Other minor changes
21452145
wordsByᵇ : (A → Bool) → List A → List (List A)
21462146
derunᵇ : (A → A → Bool) → List A → List A
21472147
deduplicateᵇ : (A → A → Bool) → List A → List A
2148+
findᵇ : (A → Bool) → List A -> Maybe A
2149+
findIndexᵇ : (A → Bool) → (x : List A) → Maybe $ Fin (length x)
2150+
findIndicesᵇ : (A → Bool) → List A → List ℕ
2151+
find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A
2152+
findIndex : ∀ {P : Pred A p} → Decidable P → (x : List A) → Maybe $ Fin (length x)
2153+
findIndices : ∀ {P : Pred A p} → Decidable P → List A → List ℕ
21482154
```
21492155

21502156
* Added new functions and definitions to `Data.List.Base`:

src/Data/List/Base.agda

+29-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s
2020
open import Data.Product.Base as Prod using (_×_; _,_; map₁; map₂′)
2121
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
2222
open import Data.These.Base as These using (These; this; that; these)
23-
open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
23+
open import Function.Base
24+
using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip)
2425
open import Level using (Level)
2526
open import Relation.Nullary.Decidable.Core using (does; ¬?)
2627
open import Relation.Unary using (Pred; Decidable)
@@ -395,6 +396,24 @@ deduplicateᵇ : (A → A → Bool) → List A → List A
395396
deduplicateᵇ r [] = []
396397
deduplicateᵇ r (x ∷ xs) = x ∷ filterᵇ (not ∘ r x) (deduplicateᵇ r xs)
397398

399+
findᵇ : (A Bool) List A Maybe A
400+
findᵇ p [] = nothing
401+
findᵇ p (x ∷ xs) = if p x then just x else findᵇ p xs
402+
403+
findIndexᵇ : (A Bool) (x : List A) Maybe $ Fin (length x)
404+
findIndexᵇ p [] = nothing
405+
findIndexᵇ p (x ∷ xs) = if p x
406+
then just zero
407+
else mapMaybe suc (findIndexᵇ p xs)
408+
409+
findIndicesᵇ : (A Bool) List A List ℕ
410+
findIndicesᵇ {A = A} p = h 0 where
411+
h : List A List ℕ
412+
h n [] = []
413+
h n (x ∷ xs) = if p x
414+
then n ∷ h (suc n) xs
415+
else h (suc n) xs
416+
398417
-- Equivalent functions that use a decidable predicate instead of a
399418
-- boolean function.
400419

@@ -436,6 +455,15 @@ derun R? = derunᵇ (does ∘₂ R?)
436455
deduplicate : {R : Rel A p} B.Decidable R List A List A
437456
deduplicate R? = deduplicateᵇ (does ∘₂ R?)
438457

458+
find : {P : Pred A p} Decidable P List A Maybe A
459+
find P? = findᵇ (does ∘ P?)
460+
461+
findIndex : {P : Pred A p} Decidable P (x : List A) Maybe $ Fin (length x)
462+
findIndex P? = findIndexᵇ (does ∘ P?)
463+
464+
findIndices : {P : Pred A p} Decidable P List A List ℕ
465+
findIndices P? = findIndicesᵇ (does ∘ P?)
466+
439467
------------------------------------------------------------------------
440468
-- Actions on single elements
441469

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Data.List.Membership.Setoid.Properties where
1111
open import Algebra using (Op₂; Selective)
1212
open import Data.Bool.Base using (true; false)
1313
open import Data.Fin.Base using (Fin; zero; suc)
14-
open import Data.List.Base
14+
open import Data.List.Base hiding (find)
1515
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
1616
open import Data.List.Relation.Unary.All as All using (All)
1717
import Data.List.Relation.Unary.Any.Properties as Any

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
module Data.List.Relation.Binary.Subset.Setoid.Properties where
1010

1111
open import Data.Bool.Base using (Bool; true; false)
12-
open import Data.List.Base hiding (_∷ʳ_)
12+
open import Data.List.Base hiding (_∷ʳ_; find)
1313
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
1414
open import Data.List.Relation.Unary.All as All using (All)
1515
import Data.List.Membership.Setoid as Membership

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool; false; true; T)
1212
open import Data.Bool.Properties using (T-∨; T-≡)
1313
open import Data.Empty using (⊥)
1414
open import Data.Fin.Base using (Fin; zero; suc)
15-
open import Data.List.Base as List
15+
open import Data.List.Base as List hiding (find)
1616
open import Data.List.Properties using (ʳ++-defn)
1717
open import Data.List.Effectful as Listₑ using (monad)
1818
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)

src/Function/Base.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ flip f = λ y x → f x y
7272

7373
-- Application - note that _$_ is right associative, as in Haskell.
7474
-- If you want a left associative infix application operator, use
75-
-- Category.Functor._<$>_ from Category.Monad.Identity.IdentityMonad.
75+
-- RawFunctor._<$>_ from Effect.Functor.
7676

7777
_$_ : {A : Set a} {B : A Set b}
7878
((x : A) B x) ((x : A) B x)

0 commit comments

Comments
 (0)