diff --git a/CHANGELOG.md b/CHANGELOG.md index 5138c4017f..895d9684f8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2169,6 +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) → (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 2b25ece003..9817cf8648 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,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 diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 4072da5ed8..0dcca71055 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/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 diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 551b721d8d..abf5bdc86f 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 b50b962e26..d51a5cba64 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)