Skip to content

Commit cd70bc2

Browse files
jamesmckinnajamesmckinna
authored
Restore deleted *.Categorical.* as deprecated modules (#1946)
* restored `Categorical` modules towards deprecation * updated `CHANGELOG` * updated `GenerateEverything`
1 parent 2839cec commit cd70bc2

File tree

32 files changed

+553
-2
lines changed

32 files changed

+553
-2
lines changed

‎CHANGELOG.md‎

Lines changed: 38 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,8 +88,7 @@ Non-backwards compatible changes
8888
such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, as this
8989
obstructs the importing of the `agda-categories` development into the Standard Library,
9090
and moreover needlessly restricts the applicability of categorical concepts to this
91-
(highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*`
92-
which exploited these structures for effectful programming have been renamed `*.Effectful`.
91+
(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.
9392

9493
### Improvements to pretty printing and regexes
9594

@@ -871,6 +870,43 @@ Deprecated modules
871870
Algebra.Morphism.LatticeMonomorphism ↦ Algebra.Lattice.Morphism.LatticeMonomorphism
872871
```
873872

873+
### Moving `*.Catgeorical.*` files
874+
875+
* As discussed above the following files have been moved:
876+
```agda
877+
Codata.Sized.Colist.Categorical ↦ Codata.Sized.Colist.Effectful
878+
Codata.Sized.Covec.Categorical ↦ Codata.Sized.Covec.Effectful
879+
Codata.Sized.Delay.Categorical ↦ Codata.Sized.Delay.Effectful
880+
Codata.Sized.Stream.Categorical ↦ Codata.Sized.Stream.Effectful
881+
Data.List.Categorical ↦ Data.List.Effectful
882+
Data.List.Categorical.Transformer ↦ Data.List.Effectful.Transformer
883+
Data.List.NonEmpty.Categorical ↦ Data.List.NonEmpty.Effectful
884+
Data.List.NonEmpty.Categorical.Transformer ↦ Data.List.NonEmpty.Effectful.Transformer
885+
Data.Maybe.Categorical ↦ Data.Maybe.Effectful
886+
Data.Maybe.Categorical.Transformer ↦ Data.Maybe.Effectful.Transformer
887+
Data.Product.Categorical.Examples ↦ Data.Product.Effectful.Examples
888+
Data.Product.Categorical.Left ↦ Data.Product.Effectful.Left
889+
Data.Product.Categorical.Left.Base ↦ Data.Product.Effectful.Left.Base
890+
Data.Product.Categorical.Right ↦ Data.Product.Effectful.Right
891+
Data.Product.Categorical.Right.Base ↦ Data.Product.Effectful.Right.Base
892+
Data.Sum.Categorical.Examples ↦ Data.Sum.Effectful.Examples
893+
Data.Sum.Categorical.Left ↦ Data.Sum.Effectful.Left
894+
Data.Sum.Categorical.Left.Transformer ↦ Data.Sum.Effectful.Left.Transformer
895+
Data.Sum.Categorical.Right ↦ Data.Sum.Effectful.Right
896+
Data.Sum.Categorical.Right.Transformer ↦ Data.Sum.Effectful.Right.Transformer
897+
Data.These.Categorical.Examples ↦ Data.These.Effectful.Examples
898+
Data.These.Categorical.Left ↦ Data.These.Effectful.Left
899+
Data.These.Categorical.Left.Base ↦ Data.These.Effectful.Left.Base
900+
Data.These.Categorical.Right ↦ Data.These.Effectful.Right
901+
Data.These.Categorical.Right.Base ↦ Data.These.Effectful.Right.Base
902+
Data.Vec.Categorical ↦ Data.Vec.Effectful
903+
Data.Vec.Categorical.Transformer ↦ Data.Vec.Effectful.Transformer
904+
Data.Vec.Recursive.Categorical ↦ Data.Vec.Recursive.Effectful
905+
Function.Identity.Categorical ↦ Function.Identity.Effectful
906+
IO.Categorical ↦ IO.Effectful
907+
Reflection.TCM.Categorical ↦ Reflection.TCM.Effectful
908+
```
909+
874910
### Moving `Relation.Binary.Properties.XLattice` files
875911

876912
* The following files have been moved:

‎GenerateEverything.hs‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ unsafeModules = map modToFile
5353
, "Foreign.Haskell.Pair"
5454
, "IO"
5555
, "IO.Base"
56+
, "IO.Categorical"
5657
, "IO.Infinite"
5758
, "IO.Instances"
5859
, "IO.Effectful"
@@ -121,6 +122,7 @@ sizedTypesModules = map modToFile
121122
, "Codata.Sized.Cofin.Literals"
122123
, "Codata.Sized.Colist"
123124
, "Codata.Sized.Colist.Bisimilarity"
125+
, "Codata.Sized.Colist.Categorical"
124126
, "Codata.Sized.Colist.Effectful"
125127
, "Codata.Sized.Colist.Properties"
126128
, "Codata.Sized.Conat"
@@ -129,20 +131,23 @@ sizedTypesModules = map modToFile
129131
, "Codata.Sized.Conat.Properties"
130132
, "Codata.Sized.Covec"
131133
, "Codata.Sized.Covec.Bisimilarity"
134+
, "Codata.Sized.Covec.Categorical"
132135
, "Codata.Sized.Covec.Effectful"
133136
, "Codata.Sized.Covec.Instances"
134137
, "Codata.Sized.Covec.Properties"
135138
, "Codata.Sized.Cowriter"
136139
, "Codata.Sized.Cowriter.Bisimilarity"
137140
, "Codata.Sized.Delay"
138141
, "Codata.Sized.Delay.Bisimilarity"
142+
, "Codata.Sized.Delay.Categorical"
139143
, "Codata.Sized.Delay.Effectful"
140144
, "Codata.Sized.Delay.Properties"
141145
, "Codata.Sized.M"
142146
, "Codata.Sized.M.Bisimilarity"
143147
, "Codata.Sized.M.Properties"
144148
, "Codata.Sized.Stream"
145149
, "Codata.Sized.Stream.Bisimilarity"
150+
, "Codata.Sized.Stream.Categorical"
146151
, "Codata.Sized.Stream.Effectful"
147152
, "Codata.Sized.Stream.Instances"
148153
, "Codata.Sized.Stream.Properties"

‎src/Codata/Sized/Colist/Categorical.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Codata.Sized.Colist.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --sized-types #-}
9+
10+
module Codata.Sized.Colist.Categorical where
11+
12+
open import Codata.Sized.Colist.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Codata.Sized.Colist.Categorical was deprecated in v2.0.
16+
Use Codata.Sized.Colist.Effectful instead."
17+
#-}

‎src/Codata/Sized/Covec/Categorical.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Codata.Sized.Covec.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --sized-types #-}
9+
10+
module Codata.Sized.Covec.Categorical where
11+
12+
open import Codata.Sized.Covec.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Codata.Sized.Covec.Categorical was deprecated in v2.0.
16+
Use Codata.Sized.Covec.Effectful instead."
17+
#-}

‎src/Codata/Sized/Delay/Categorical.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Codata.Sized.Delay.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --sized-types #-}
9+
10+
module Codata.Sized.Delay.Categorical where
11+
12+
open import Codata.Sized.Delay.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Codata.Sized.Delay.Categorical was deprecated in v2.0.
16+
Use Codata.Sized.Delay.Effectful instead."
17+
#-}

‎src/Codata/Sized/Stream/Categorical.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Codata.Sized.Stream.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --sized-types #-}
9+
10+
module Codata.Sized.Stream.Categorical where
11+
12+
open import Codata.Sized.Stream.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Codata.Sized.Stream.Categorical was deprecated in v2.0.
16+
Use Codata.Sized.Stream.Effectful instead."
17+
#-}

‎src/Data/List/Categorical.agda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Data.List.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --safe #-}
9+
10+
module Data.List.Categorical where
11+
12+
open import Data.List.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Data.List.Categorical was deprecated in v2.0.
16+
Use Data.List.Effectful instead."
17+
#-}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Data.List.Effectful.Transformer` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --safe #-}
9+
10+
module Data.List.Categorical.Transformer where
11+
12+
open import Data.List.Effectful.Transformer public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Data.List.Categorical.Transformer was deprecated in v2.0.
16+
Use Data.List.Effectful.Transformer instead."
17+
#-}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Data.List.NonEmpty.Effectful` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --safe #-}
9+
10+
module Data.List.NonEmpty.Categorical where
11+
12+
open import Data.List.NonEmpty.Effectful public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Data.List.NonEmpty.Categorical was deprecated in v2.0.
16+
Use Data.List.NonEmpty.Effectful instead."
17+
#-}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module is DEPRECATED. Please use
5+
-- `Data.List.NonEmpty.Effectful.Transformer` instead.
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --cubical-compatible --safe #-}
9+
10+
module Data.List.NonEmpty.Categorical.Transformer where
11+
12+
open import Data.List.NonEmpty.Effectful.Transformer public
13+
14+
{-# WARNING_ON_IMPORT
15+
"Data.List.NonEmpty.Categorical.Transformer was deprecated in v2.0.
16+
Use Data.List.NonEmpty.Effectful.Transformer instead."
17+
#-}

0 commit comments

Comments
 (0)