[ refactor ] Add Data.Bool.ListAction (#2561)

* refactor: `Bool` analogue of #2558

* fixed header comment

* bug: restored deleted `Nat` operations

* bug: restored deleted `Nat` imports

* bug: fixed imports after deprecation

* bug: fixed imports after deprecation

* no properties as such!

Author: jamesmckinna

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
 -----------------------------
 

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
+

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."
+#-}

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⁺)

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⁻)

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