diff --git a/src/Category/Applicative.agda b/src/Category/Applicative.agda new file mode 100644 index 0000000000..370a91a8fa --- /dev/null +++ b/src/Category/Applicative.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative where + +open import Effect.Applicative public + +{-# WARNING_ON_IMPORT +"Category.Applicative was deprecated in v2.0. +Use Effect.Applicative instead." +#-} diff --git a/src/Category/Applicative/Indexed.agda b/src/Category/Applicative/Indexed.agda new file mode 100644 index 0000000000..a09e2fb8cd --- /dev/null +++ b/src/Category/Applicative/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative.Indexed where + +open import Effect.Applicative.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Applicative.Indexed was deprecated in v2.0. +Use Effect.Applicative.Indexed instead." +#-} diff --git a/src/Category/Applicative/Predicate.agda b/src/Category/Applicative/Predicate.agda new file mode 100644 index 0000000000..2f69be1f05 --- /dev/null +++ b/src/Category/Applicative/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative.Predicate where + +open import Effect.Applicative.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Applicative.Predicate was deprecated in v2.0. +Use Effect.Applicative.Predicate instead." +#-} diff --git a/src/Category/Comonad.agda b/src/Category/Comonad.agda new file mode 100644 index 0000000000..7a5be7e0da --- /dev/null +++ b/src/Category/Comonad.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Comonad` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Comonad where + +open import Effect.Comonad public + +{-# WARNING_ON_IMPORT +"Category.Comonad was deprecated in v2.0. +Use Effect.Comonad instead." +#-} diff --git a/src/Category/Functor.agda b/src/Category/Functor.agda new file mode 100644 index 0000000000..4c5b6ec450 --- /dev/null +++ b/src/Category/Functor.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor where + +open import Effect.Functor public + +{-# WARNING_ON_IMPORT +"Category.Functor was deprecated in v2.0. +Use Effect.Functor instead." +#-} diff --git a/src/Category/Functor/Indexed.agda b/src/Category/Functor/Indexed.agda new file mode 100644 index 0000000000..6f02824566 --- /dev/null +++ b/src/Category/Functor/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor.Indexed where + +open import Effect.Functor.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Functor.Indexed was deprecated in v2.0. +Use Effect.Functor.Indexed instead." +#-} diff --git a/src/Category/Functor/Predicate.agda b/src/Category/Functor/Predicate.agda new file mode 100644 index 0000000000..f0d065bea7 --- /dev/null +++ b/src/Category/Functor/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor.Predicate where + +open import Effect.Functor.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Functor.Predicate was deprecated in v2.0. +Use Effect.Functor.Predicate instead." +#-} diff --git a/src/Category/Monad.agda b/src/Category/Monad.agda new file mode 100644 index 0000000000..01143536a4 --- /dev/null +++ b/src/Category/Monad.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad where + +open import Effect.Monad public + +{-# WARNING_ON_IMPORT +"Category.Monad was deprecated in v2.0. +Use Effect.Monad instead." +#-} diff --git a/src/Category/Monad/Continuation.agda b/src/Category/Monad/Continuation.agda new file mode 100644 index 0000000000..7f0bb177ec --- /dev/null +++ b/src/Category/Monad/Continuation.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Continuation` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Continuation where + +open import Effect.Monad.Continuation public + +{-# WARNING_ON_IMPORT +"Category.Monad.Continuation was deprecated in v2.0. +Use Effect.Monad.Continuation instead." +#-} diff --git a/src/Category/Monad/Indexed.agda b/src/Category/Monad/Indexed.agda new file mode 100644 index 0000000000..d5eaa29462 --- /dev/null +++ b/src/Category/Monad/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Indexed where + +open import Effect.Monad.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Monad.Indexed was deprecated in v2.0. +Use Effect.Monad.Indexed instead." +#-} diff --git a/src/Category/Monad/Partiality.agda b/src/Category/Monad/Partiality.agda new file mode 100644 index 0000000000..c580eb274e --- /dev/null +++ b/src/Category/Monad/Partiality.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality where + +open import Effect.Monad.Partiality public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality was deprecated in v2.0. +Use Effect.Monad.Partiality instead." +#-} diff --git a/src/Category/Monad/Partiality/All.agda b/src/Category/Monad/Partiality/All.agda new file mode 100644 index 0000000000..216c28e04d --- /dev/null +++ b/src/Category/Monad/Partiality/All.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality.All` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality.All where + +open import Effect.Monad.Partiality.All public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality.All was deprecated in v2.0. +Use Effect.Monad.Partiality.All instead." +#-} diff --git a/src/Category/Monad/Partiality/Instances.agda b/src/Category/Monad/Partiality/Instances.agda new file mode 100644 index 0000000000..7917c17d99 --- /dev/null +++ b/src/Category/Monad/Partiality/Instances.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality.Instances` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality.Instances where + +open import Effect.Monad.Partiality.Instances public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality.Instances was deprecated in v2.0. +Use Effect.Monad.Partiality.Instances instead." +#-} diff --git a/src/Category/Monad/Predicate.agda b/src/Category/Monad/Predicate.agda new file mode 100644 index 0000000000..df6f29c12a --- /dev/null +++ b/src/Category/Monad/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Predicate where + +open import Effect.Monad.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Monad.Predicate was deprecated in v2.0. +Use Effect.Monad.Predicate instead." +#-} diff --git a/src/Category/Monad/Reader.agda b/src/Category/Monad/Reader.agda new file mode 100644 index 0000000000..217e033d8b --- /dev/null +++ b/src/Category/Monad/Reader.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Reader` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Reader where + +open import Effect.Monad.Reader public + +{-# WARNING_ON_IMPORT +"Category.Monad.Reader was deprecated in v2.0. +Use Effect.Monad.Reader instead." +#-} diff --git a/src/Category/Monad/State.agda b/src/Category/Monad/State.agda new file mode 100644 index 0000000000..24007b3516 --- /dev/null +++ b/src/Category/Monad/State.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.State` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.State where + +open import Effect.Monad.State public + +{-# WARNING_ON_IMPORT +"Category.Monad.State was deprecated in v2.0. +Use Effect.Monad.State instead." +#-} diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index 220e862fb4..6a44c79e39 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -27,3 +27,18 @@ postulate {-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-} {-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-} {-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-} + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +return : ∀ {a} {A : Set a} → A → IO A +return = pure +{-# WARNING_ON_USAGE return +"Warning: return was deprecated in v2.0. +Please use pure instead." +#-}