Backward compatibility with v1.7.1/2 for the IO Monad

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}

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."
+#-}