Remove stale (1.x) deprecation warnings and their associated names

CHANGELOG.md

@@ -21,6 +21,33 @@ Highlights
   substantive in `Data.{Nat|Fin}.Properties` for the concrete datatypes, which
   are summarised below, but are not each documented for all affected modules.
 
+* Any v1.x deprecation has been removed entirely.
+  This involves the removal of modules:
+  - `Algebra.FunctionProperties.Consequences.Core`
+  - `Algebra.FunctionProperties.Consequences.Propositional`
+  - `Algebra.FunctionProperties.Consequences`
+  - `Algebra.Operations.CommutativeMonoid`
+  - `Algebra.Operations.Ring`
+  - `Algebra.Operations.Semiring`
+  - `Data.AVL.Indexed.WithK`
+  - `Data.AVL.NonEmpty.Propositional`
+  - `Data.AVL.Height`
+  - `Data.AVL.Indexed`
+  - `Data.AVL.IndexedMap`
+  - `Data.AVL.Key`
+  - `Data.AVL.Map`
+  - `Data.AVL.NonEmpty`
+  - `Data.AVL.Value`
+  - `Data.AVL`
+  - `Foreign.Haskell.Maybe`
+  - `Relation.Binary.OrderMorphism`
+  - `Text.Tree.Linear`
+  - `Strict`
+
+  Several Definitions from other modules have also been removed.
+
+* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from both `Function.Endomorphism.Setoid` and `Function.Endomorphism.Propositional` have been removed
+
 Bug-fixes
 ---------
 
@@ -61,6 +88,8 @@ Non-backwards compatible changes
   Data.Tree.Rose.Show
   ```
 
+* `^-semigroup-morphism` and `^-monoid-morphism` in `Data.Nat.Properties` have had their definitions and signatures updated to use `IsMagmaHomomorphism` and `IsMonoidHomomorphism` respectively, inline with the removal of 1.x deprecations.
+
 Minor improvements
 ------------------
 

GenerateEverything.hs

@@ -64,7 +64,6 @@ unsafeModules = map modToFile
   , "Foreign.Haskell"
   , "Foreign.Haskell.Coerce"
   , "Foreign.Haskell.Either"
-  , "Foreign.Haskell.Maybe"
   , "Foreign.Haskell.List.NonEmpty"
   , "Foreign.Haskell.Pair"
   , "IO"
@@ -183,7 +182,6 @@ sizedTypesModules = map modToFile
   , "Data.Trie.NonEmpty"
   , "Relation.Unary.Sized"
   , "Size"
-  , "Text.Tree.Linear"
   ]
 
 isSizedTypesModule :: FilePath -> Bool

src/Algebra/Morphism.agda

@@ -28,181 +28,3 @@ module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) w
   open MorphismDefinitions A B _≈_ public
 
 open import Algebra.Morphism.Structures public
-
-
-------------------------------------------------------------------------
--- DEPRECATED
-------------------------------------------------------------------------
--- Please use the new definitions re-exported from
--- `Algebra.Morphism.Structures` as continuing support for the below is
--- no guaranteed.
-
--- Version 1.5
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : Semigroup c₁ ℓ₁)
-         (To   : Semigroup c₂ ℓ₂) where
-
-  private
-    module F = Semigroup From
-    module T = Semigroup To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsSemigroupMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
-      ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
-
-  IsSemigroupMorphism-syntax = IsSemigroupMorphism
-  syntax IsSemigroupMorphism-syntax From To F = F Is From -Semigroup⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : Monoid c₁ ℓ₁)
-         (To   : Monoid c₂ ℓ₂) where
-
-  private
-    module F = Monoid From
-    module T = Monoid To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsMonoidMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
-      ε-homo  : Homomorphic₀ ⟦_⟧ F.ε T.ε
-
-    open IsSemigroupMorphism sm-homo public
-
-  IsMonoidMorphism-syntax = IsMonoidMorphism
-  syntax IsMonoidMorphism-syntax From To F = F Is From -Monoid⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : CommutativeMonoid c₁ ℓ₁)
-         (To   : CommutativeMonoid c₂ ℓ₂) where
-
-  private
-    module F = CommutativeMonoid From
-    module T = CommutativeMonoid To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
-
-    open IsMonoidMorphism mn-homo public
-
-  IsCommutativeMonoidMorphism-syntax = IsCommutativeMonoidMorphism
-  syntax IsCommutativeMonoidMorphism-syntax From To F = F Is From -CommutativeMonoid⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : IdempotentCommutativeMonoid c₁ ℓ₁)
-         (To   : IdempotentCommutativeMonoid c₂ ℓ₂) where
-
-  private
-    module F = IdempotentCommutativeMonoid From
-    module T = IdempotentCommutativeMonoid To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
-
-    open IsMonoidMorphism mn-homo public
-
-    isCommutativeMonoidMorphism :
-      IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧
-    isCommutativeMonoidMorphism = record { mn-homo = mn-homo }
-
-  IsIdempotentCommutativeMonoidMorphism-syntax = IsIdempotentCommutativeMonoidMorphism
-  syntax IsIdempotentCommutativeMonoidMorphism-syntax From To F = F Is From -IdempotentCommutativeMonoid⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : Group c₁ ℓ₁)
-         (To   : Group c₂ ℓ₂) where
-
-  private
-    module F = Group From
-    module T = Group To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsGroupMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
-
-    open IsMonoidMorphism mn-homo public
-
-    ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
-    ⁻¹-homo x = let open ≈-Reasoning T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
-      ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
-      ⟦ x F.⁻¹ F.∙ x ⟧     ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
-      ⟦ F.ε ⟧              ≈⟨ ε-homo ⟩
-      T.ε ∎
-
-  IsGroupMorphism-syntax = IsGroupMorphism
-  syntax IsGroupMorphism-syntax From To F = F Is From -Group⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : AbelianGroup c₁ ℓ₁)
-         (To   : AbelianGroup c₂ ℓ₂) where
-
-  private
-    module F = AbelianGroup From
-    module T = AbelianGroup To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      gp-homo : IsGroupMorphism F.group T.group ⟦_⟧
-
-    open IsGroupMorphism gp-homo public
-
-  IsAbelianGroupMorphism-syntax = IsAbelianGroupMorphism
-  syntax IsAbelianGroupMorphism-syntax From To F = F Is From -AbelianGroup⟶ To
-
-module _ {c₁ ℓ₁ c₂ ℓ₂}
-         (From : Ring c₁ ℓ₁)
-         (To   : Ring c₂ ℓ₂) where
-
-  private
-    module F = Ring From
-    module T = Ring To
-  open Definitions F.Carrier T.Carrier T._≈_
-
-  record IsRingMorphism (⟦_⟧ : Morphism) :
-         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
-    field
-      +-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup
-      *-mn-homo   : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid
-
-  IsRingMorphism-syntax = IsRingMorphism
-  syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To
-
-{-# WARNING_ON_USAGE IsSemigroupMorphism
-"Warning: IsSemigroupMorphism was deprecated in v1.5.
-Please use IsMagmaHomomorphism instead."
-#-}
-{-# WARNING_ON_USAGE IsMonoidMorphism
-"Warning: IsMonoidMorphism was deprecated in v1.5.
-Please use IsMonoidHomomorphism instead."
-#-}
-{-# WARNING_ON_USAGE IsCommutativeMonoidMorphism
-"Warning: IsCommutativeMonoidMorphism was deprecated in v1.5.
-Please use IsMonoidHomomorphism instead."
-#-}
-{-# WARNING_ON_USAGE IsIdempotentCommutativeMonoidMorphism
-"Warning: IsIdempotentCommutativeMonoidMorphism was deprecated in v1.5.
-Please use IsMonoidHomomorphism instead."
-#-}
-{-# WARNING_ON_USAGE IsGroupMorphism
-"Warning: IsGroupMorphism was deprecated in v1.5.
-Please use IsGroupHomomorphism instead."
-#-}
-{-# WARNING_ON_USAGE IsAbelianGroupMorphism
-"Warning: IsAbelianGroupMorphism was deprecated in v1.5.
-Please use IsGroupHomomorphism instead."
-#-}

src/Algebra/Morphism/Definitions.agda

@@ -28,19 +28,3 @@ Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
 
 Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _
 Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.3
-
-Morphism : Set _
-Morphism = A → B
-
-{-# WARNING_ON_USAGE Morphism
-"Warning: Morphism was deprecated in v1.3.
-Please use the standard function notation (e.g. A → B) instead."
-#-}