Restore deleted *.Categorical.* as deprecated modules (#1946)

* restored `Categorical` modules towards deprecation

* updated `CHANGELOG`

* updated `GenerateEverything`

CHANGELOG.md

@@ -88,8 +88,7 @@ Non-backwards compatible changes
  such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, as this
  obstructs the importing of the `agda-categories` development into the Standard Library,
  and moreover needlessly restricts the applicability of categorical concepts to this
- (highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*`
- which exploited these structures for effectful programming have been renamed `*.Effectful`.
+ (highly specific) mode of use. Correspondingly, client modules grouped under `*.Categorical.*` which exploit such structure for effectful programming have been renamed `*.Effectful`, with the originals being deprecated.
 
 ### Improvements to pretty printing and regexes
 
@@ -871,6 +870,43 @@ Deprecated modules
  Algebra.Morphism.LatticeMonomorphism ↦ Algebra.Lattice.Morphism.LatticeMonomorphism
  ```
 
+### Moving `*.Catgeorical.*` files
+
+* As discussed above the following files have been moved:
+ ```agda
+ Codata.Sized.Colist.Categorical ↦ Codata.Sized.Colist.Effectful
+ Codata.Sized.Covec.Categorical ↦ Codata.Sized.Covec.Effectful
+ Codata.Sized.Delay.Categorical ↦ Codata.Sized.Delay.Effectful
+ Codata.Sized.Stream.Categorical ↦ Codata.Sized.Stream.Effectful
+ Data.List.Categorical ↦ Data.List.Effectful
+ Data.List.Categorical.Transformer ↦ Data.List.Effectful.Transformer
+ Data.List.NonEmpty.Categorical ↦ Data.List.NonEmpty.Effectful
+ Data.List.NonEmpty.Categorical.Transformer ↦ Data.List.NonEmpty.Effectful.Transformer
+ Data.Maybe.Categorical ↦ Data.Maybe.Effectful
+ Data.Maybe.Categorical.Transformer ↦ Data.Maybe.Effectful.Transformer
+ Data.Product.Categorical.Examples ↦ Data.Product.Effectful.Examples
+ Data.Product.Categorical.Left ↦ Data.Product.Effectful.Left
+ Data.Product.Categorical.Left.Base ↦ Data.Product.Effectful.Left.Base
+ Data.Product.Categorical.Right ↦ Data.Product.Effectful.Right
+ Data.Product.Categorical.Right.Base ↦ Data.Product.Effectful.Right.Base
+ Data.Sum.Categorical.Examples ↦ Data.Sum.Effectful.Examples
+ Data.Sum.Categorical.Left ↦ Data.Sum.Effectful.Left
+ Data.Sum.Categorical.Left.Transformer ↦ Data.Sum.Effectful.Left.Transformer
+ Data.Sum.Categorical.Right ↦ Data.Sum.Effectful.Right
+ Data.Sum.Categorical.Right.Transformer ↦ Data.Sum.Effectful.Right.Transformer
+ Data.These.Categorical.Examples ↦ Data.These.Effectful.Examples
+ Data.These.Categorical.Left ↦ Data.These.Effectful.Left
+ Data.These.Categorical.Left.Base ↦ Data.These.Effectful.Left.Base
+ Data.These.Categorical.Right ↦ Data.These.Effectful.Right
+ Data.These.Categorical.Right.Base ↦ Data.These.Effectful.Right.Base
+ Data.Vec.Categorical ↦ Data.Vec.Effectful
+ Data.Vec.Categorical.Transformer ↦ Data.Vec.Effectful.Transformer
+ Data.Vec.Recursive.Categorical ↦ Data.Vec.Recursive.Effectful
+ Function.Identity.Categorical ↦ Function.Identity.Effectful
+ IO.Categorical ↦ IO.Effectful
+ Reflection.TCM.Categorical ↦ Reflection.TCM.Effectful
+ ```
+
 ### Moving `Relation.Binary.Properties.XLattice` files
 
 * The following files have been moved:

GenerateEverything.hs

@@ -53,6 +53,7 @@ unsafeModules = map modToFile
  , "Foreign.Haskell.Pair"
  , "IO"
  , "IO.Base"
+ , "IO.Categorical"
  , "IO.Infinite"
  , "IO.Instances"
  , "IO.Effectful"
@@ -121,6 +122,7 @@ sizedTypesModules = map modToFile
  , "Codata.Sized.Cofin.Literals"
  , "Codata.Sized.Colist"
  , "Codata.Sized.Colist.Bisimilarity"
+ , "Codata.Sized.Colist.Categorical"
  , "Codata.Sized.Colist.Effectful"
  , "Codata.Sized.Colist.Properties"
  , "Codata.Sized.Conat"
@@ -129,20 +131,23 @@ sizedTypesModules = map modToFile
  , "Codata.Sized.Conat.Properties"
  , "Codata.Sized.Covec"
  , "Codata.Sized.Covec.Bisimilarity"
+ , "Codata.Sized.Covec.Categorical"
  , "Codata.Sized.Covec.Effectful"
  , "Codata.Sized.Covec.Instances"
  , "Codata.Sized.Covec.Properties"
  , "Codata.Sized.Cowriter"
  , "Codata.Sized.Cowriter.Bisimilarity"
  , "Codata.Sized.Delay"
  , "Codata.Sized.Delay.Bisimilarity"
+ , "Codata.Sized.Delay.Categorical"
  , "Codata.Sized.Delay.Effectful"
  , "Codata.Sized.Delay.Properties"
  , "Codata.Sized.M"
  , "Codata.Sized.M.Bisimilarity"
  , "Codata.Sized.M.Properties"
  , "Codata.Sized.Stream"
  , "Codata.Sized.Stream.Bisimilarity"
+ , "Codata.Sized.Stream.Categorical"
  , "Codata.Sized.Stream.Effectful"
  , "Codata.Sized.Stream.Instances"
  , "Codata.Sized.Stream.Properties"

src/Codata/Sized/Colist/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Colist.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Colist.Categorical where
+
+open import Codata.Sized.Colist.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Colist.Categorical was deprecated in v2.0.
+Use Codata.Sized.Colist.Effectful instead."
+#-}

src/Codata/Sized/Covec/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Covec.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Covec.Categorical where
+
+open import Codata.Sized.Covec.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Covec.Categorical was deprecated in v2.0.
+Use Codata.Sized.Covec.Effectful instead."
+#-}

src/Codata/Sized/Delay/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Delay.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Delay.Categorical where
+
+open import Codata.Sized.Delay.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Delay.Categorical was deprecated in v2.0.
+Use Codata.Sized.Delay.Effectful instead."
+#-}

src/Codata/Sized/Stream/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Stream.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Stream.Categorical where
+
+open import Codata.Sized.Stream.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Stream.Categorical was deprecated in v2.0.
+Use Codata.Sized.Stream.Effectful instead."
+#-}

src/Data/List/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Categorical where
+
+open import Data.List.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.List.Categorical was deprecated in v2.0.
+Use Data.List.Effectful instead."
+#-}

src/Data/List/Categorical/Transformer.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Categorical.Transformer where
+
+open import Data.List.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.List.Categorical.Transformer was deprecated in v2.0.
+Use Data.List.Effectful.Transformer instead."
+#-}

src/Data/List/NonEmpty/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.NonEmpty.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Categorical where
+
+open import Data.List.NonEmpty.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.List.NonEmpty.Categorical was deprecated in v2.0.
+Use Data.List.NonEmpty.Effectful instead."
+#-}

src/Data/List/NonEmpty/Categorical/Transformer.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.NonEmpty.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Categorical.Transformer where
+
+open import Data.List.NonEmpty.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.List.NonEmpty.Categorical.Transformer was deprecated in v2.0.
+Use Data.List.NonEmpty.Effectful.Transformer instead."
+#-}

src/Data/Maybe/Categorical.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Maybe.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Maybe.Categorical where
+
+open import Data.Maybe.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.Maybe.Categorical was deprecated in v2.0.
+Use Data.Maybe.Effectful instead."
+#-}

src/Data/Maybe/Categorical/Transformer.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Maybe.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Maybe.Categorical.Transformer where
+
+open import Data.Maybe.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.Maybe.Categorical.Transformer was deprecated in v2.0.
+Use Data.Maybe.Effectful.Transformer instead."
+#-}

src/Data/Product/Categorical/Examples.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Examples` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Examples where
+
+open import Data.Product.Effectful.Examples public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Examples was deprecated in v2.0.
+Use Data.Product.Effectful.Examples instead."
+#-}

src/Data/Product/Categorical/Left.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Left` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Left where
+
+open import Data.Product.Effectful.Left public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Left was deprecated in v2.0.
+Use Data.Product.Effectful.Left instead."
+#-}

src/Data/Product/Categorical/Left/Base.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Left.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Left.Base where
+
+open import Data.Product.Effectful.Left.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Left.Base was deprecated in v2.0.
+Use Data.Product.Effectful.Left.Base instead."
+#-}

src/Data/Product/Categorical/Right.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Right` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Right where
+
+open import Data.Product.Effectful.Right public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Right was deprecated in v2.0.
+Use Data.Product.Effectful.Right instead."
+#-}

src/Data/Product/Categorical/Right/Base.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Right.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Right.Base where
+
+open import Data.Product.Effectful.Right.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Right.Base was deprecated in v2.0.
+Use Data.Product.Effectful.Right.Base instead."
+#-}

src/Data/Sum/Categorical/Examples.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Examples` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Examples where
+
+open import Data.Sum.Effectful.Examples public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Examples was deprecated in v2.0.
+Use Data.Sum.Effectful.Examples instead."
+#-}

src/Data/Sum/Categorical/Left.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Left` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Left where
+
+open import Data.Sum.Effectful.Left public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Left was deprecated in v2.0.
+Use Data.Sum.Effectful.Left instead."
+#-}