diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..4940047ba8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -51,9 +51,19 @@ Deprecated names ∣∣-trans ↦ ∥-trans ``` +* In `Data.List.Base`: + ```agda + and ↦ Data.Bool.ListAction.and + or ↦ Data.Bool.ListAction.or + any ↦ Data.Bool.ListAction.any + all ↦ Data.Bool.ListAction.all + ``` + New modules ----------- +* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. + Additions to existing modules ----------------------------- diff --git a/src/Data/Bool/ListAction.agda b/src/Data/Bool/ListAction.agda new file mode 100644 index 0000000000..d7dc34c5a0 --- /dev/null +++ b/src/Data/Bool/ListAction.agda @@ -0,0 +1,40 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Booleans: conjunction and disjunction of lists +-- +-- Issue #2553: this is a compatibility stub module, +-- ahead of a more thorough refactoring in terms of +-- `Data.List.Effectful.Foldable.foldmap`. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Bool.ListAction where + +open import Data.Bool.Base using (Bool; _∧_; _∨_; true; false) +open import Data.List.Base using (List; map; foldr) +open import Function.Base using (_∘_) +open import Level + +private + variable + a : Level + A : Set a + + +------------------------------------------------------------------------ +-- Definitions + +and : List Bool → Bool +and = foldr _∧_ true + +or : List Bool → Bool +or = foldr _∨_ false + +any : (A → Bool) → List A → Bool +any p = or ∘ map p + +all : (A → Bool) → List A → Bool +all p = and ∘ map p + diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 0c63e34940..62a68a02ed 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool using (Bool; false; true; not; _∧_; _∨_; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_) open import Data.Product.Base as Product 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) @@ -150,18 +150,6 @@ null : List A → Bool null [] = true null (x ∷ xs) = false -and : List Bool → Bool -and = foldr _∧_ true - -or : List Bool → Bool -or = foldr _∨_ false - -any : (A → Bool) → List A → Bool -any p = or ∘ map p - -all : (A → Bool) → List A → Bool -all p = and ∘ map p - sum : List ℕ → ℕ sum = foldr _+_ 0 @@ -580,3 +568,33 @@ scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs "Warning: scanl was deprecated in v2.1. Please use Data.List.Scans.Base.scanl instead." #-} + +-- Version 2.3 + +and : List Bool → Bool +and = foldr _∧_ true + +all : (A → Bool) → List A → Bool +all p = and ∘ map p +{-# WARNING_ON_USAGE and +"Warning: and was deprecated in v2.3. +Please use Data.Bool.ListAction.and instead." +#-} +{-# WARNING_ON_USAGE all +"Warning: all was deprecated in v2.3. +Please use Data.Nat.ListAction.all instead." +#-} + +or : List Bool → Bool +or = foldr _∨_ false + +any : (A → Bool) → List A → Bool +any p = or ∘ map p +{-# WARNING_ON_USAGE or +"Warning: or was deprecated in v2.3. +Please use Data.Bool.ListAction.or instead." +#-} +{-# WARNING_ON_USAGE any +"Warning: any was deprecated in v2.3. +Please use Data.Bool.ListAction.any instead." +#-} diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index 4054afc092..a0aab051c7 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -10,8 +10,9 @@ module Data.List.Relation.Binary.Subset.Propositional.Properties where open import Data.Bool.Base using (Bool; true; false; T) +open import Data.Bool.ListAction using (any) open import Data.List.Base - using (List; []; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter) + using (List; []; map; _∷_; _++_; concat; concatMap; applyUpTo; filter) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.All using (All) import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺) diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 7411af335f..7fe50e241f 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -10,9 +10,10 @@ module Data.List.Relation.Unary.All.Properties where open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Bool.Base using (Bool; T; true; false) +open import Data.Bool.ListAction using (all) open import Data.Bool.Properties using (T-∧) open import Data.Fin.Base using (Fin; zero; suc) -open import Data.List.Base as List hiding (lookup; updateAt) +open import Data.List.Base as List hiding (lookup; updateAt; and; or; all; any) open import Data.List.Membership.Propositional using (_∈_; _≢∈_) open import Data.List.Membership.Propositional.Properties using (there-injective-≢∈; ∈-filter⁻) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 6f1df8cbcc..f9b139dfdb 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -9,10 +9,11 @@ module Data.List.Relation.Unary.Any.Properties where open import Data.Bool.Base using (Bool; false; true; T) +open import Data.Bool.ListAction using (any) 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 hiding (find) +open import Data.List.Base as List hiding (find; and; or; all; any) open import Data.List.Effectful as List using (monad) open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.List.Membership.Propositional