[ refactor ] fix #2865 for v2.4 (#2954)

* [ refactor ] fix #2865

* refactor: another round of renaming

* fix: revert changes to `List.Relation.Unary.Any`

* add: comment documenting downstream intentions to make changes

* add: additional content to the deprecation warning

Author: jamesmckinna

CHANGELOG.md

@@ -104,6 +104,11 @@ Deprecated names
   witness   ↦   satisfiable
   ```
 
+* In `Data.List.Relation.Unary.Any`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
@@ -321,7 +326,7 @@ Additions to existing modules
 
 * In `Data.List.NonEmpty.Relation.Unary.All`:
   ```
-  map : P ⊆ Q → All P xs → All Q xs
+  map : P ⊆ Q → All P ⊆ All Q
   ```
 
 * In `Data.List.Properties`:
@@ -331,6 +336,11 @@ Additions to existing modules
   filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
   ```
 
+* In `Data.List.Relation.Unary.Any`:
+  ```agda
+  satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
+  ```
+
 * In `Data.Nat.Divisibility`:
   ```agda
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o

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

@@ -42,6 +42,6 @@ map g (there pxs) = there (List.map g pxs)
 ------------------------------------------------------------------------
 -- Predicates
 
-satisfied : Any P xs → Satisfiable P
-satisfied (here px)  = _ , px
-satisfied (there pxs) = List.satisfied pxs
+satisfiable : Any P xs → Satisfiable P
+satisfiable (here px)  = _ , px
+satisfiable (there pxs) = List.satisfied pxs

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

@@ -69,7 +69,11 @@ infixl 4 _─_
 _─_ : {P : Pred A p} → ∀ xs → Any P xs → List A
 xs ─ x∈xs = removeAt xs (index x∈xs)
 
--- If any element satisfies P, then P is satisfied.
+-- If any element satisfies P, then P is satisfiable.
+
+-- v2.4 `satisfied` is being retained for compatibility reasons,
+--      while `satisfiable` below is renamed to `satisfiable⁺`
+-- v3.0 `satisfied` will be renamed to `satisfiable`
 
 satisfied : Any P xs → Satisfiable P
 satisfied (here px)   = _ , px
@@ -90,12 +94,16 @@ any? : Decidable P → Decidable (Any P)
 any? P? []       = no λ()
 any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs)
 
-satisfiable : Satisfiable P → Satisfiable (Any P)
-satisfiable (x , Px) = [ x ] , here Px
+satisfiable⁺ : Satisfiable P → Satisfiable (Any P)
+satisfiable⁺ (x , Px) = [ x ] , here Px
+
+satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
+satisfiable⁻ (x ∷ _  , here px)   = x , px
+satisfiable⁻ (_ ∷ xs , there pxs) = satisfiable⁻ (xs , pxs)
 
 
 ------------------------------------------------------------------------
--- DEPRECATED
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
@@ -107,3 +115,14 @@ any = any?
 "Warning: any was deprecated in v1.4.
 Please use any? instead."
 #-}
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}