[ cleanup ] imports in the Effect.Monad modules (#2371)

Author: gallais

src/Effect/Monad/Continuation.agda

@@ -8,13 +8,12 @@
 
 module Effect.Monad.Continuation where
 
-open import Effect.Applicative
-open import Effect.Applicative.Indexed
-open import Effect.Monad
+open import Effect.Applicative.Indexed using (IFun)
+open import Effect.Monad using (RawMonad)
 open import Function.Identity.Effectful as Id using (Identity)
-open import Effect.Monad.Indexed
+open import Effect.Monad.Indexed using (RawIMonad)
 open import Function.Base using (flip)
-open import Level
+open import Level using (Level; _⊔_; suc)
 
 private
   variable

src/Effect/Monad/Error/Transformer.agda

@@ -6,16 +6,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level
+open import Level using (Level; _⊔_; suc)
 
 module Effect.Monad.Error.Transformer {e} (E : Set e) (a : Level) where
 
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
+open import Effect.Monad using (RawMonad)
+open import Function.Base using (_∘′_; _$_)
 
 private
   variable

src/Effect/Monad/IO.agda

@@ -6,15 +6,13 @@
 
 {-# OPTIONS --cubical-compatible --guardedness #-}
 
-open import Level
-
 module Effect.Monad.IO where
 
 open import Data.Product.Base using (_,_)
-open import Function.Base
+open import Effect.Functor using (RawFunctor)
+open import Function.Base using (id)
 open import IO.Base using (IO)
-open import Effect.Functor
-open import Effect.Monad
+open import Level using (Level; suc)
 
 private
   variable

src/Effect/Monad/Identity.agda

@@ -8,12 +8,12 @@
 
 module Effect.Monad.Identity where
 
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Effect.Comonad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
+open import Effect.Comonad using (RawComonad)
 open import Function.Base using (id; _∘′_; _|>′_; _$′_; flip)
-open import Level
+open import Level using (Level)
 
 private
   variable

src/Effect/Monad/Partiality.agda

@@ -9,13 +9,13 @@
 module Effect.Monad.Partiality where
 
 open import Codata.Musical.Notation using (∞; ♯_; ♭)
-open import Effect.Functor using (RawFunctor)
-open import Effect.Applicative using (RawApplicative)
-open import Effect.Monad using (RawMonad; module Join)
 open import Data.Bool.Base using (Bool; false; true)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
 open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)

src/Effect/Monad/Predicate.agda

@@ -10,10 +10,10 @@
 
 module Effect.Monad.Predicate where
 
-open import Effect.Monad.Indexed using (RawIMonad)
 open import Data.Product.Base using (_,_)
+open import Effect.Monad.Indexed using (RawIMonad)
 open import Function.Base using (const; id; _∘_)
-open import Level using (Level; suc; _⊔_)
+open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 open import Relation.Unary using (_⊆_; _⇒_; _∈_; _∩_; ｛_｝)
 open import Relation.Unary.PredicateTransformer using (Pt)
@@ -24,7 +24,7 @@ private
 
 ------------------------------------------------------------------------
 
-record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc i ⊔ suc ℓ) where
+record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc (i ⊔ ℓ)) where
 
   infixl 1 _?>=_ _?>_ _>?>_ _?>=′_
   infixr 1 _=<?_ _<?<_

src/Effect/Monad/Reader.agda

@@ -6,15 +6,11 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level
-
 module Effect.Monad.Reader where
 
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
 open import Effect.Monad.Identity as Id using (Identity; runIdentity)
 open import Level using (Level)
 

src/Effect/Monad/Reader/Transformer.agda

@@ -10,11 +10,11 @@
 module Effect.Monad.Reader.Transformer where
 
 open import Algebra using (RawMonoid)
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
+open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
 open import Function.Base using (_∘′_; const; _$_)
 open import Level using (Level; _⊔_)
 

src/Effect/Monad/State.agda

@@ -6,18 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-
 module Effect.Monad.State where
 
 open import Data.Product.Base using (_×_)
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
 open import Effect.Monad.Identity as Id using (Identity; runIdentity)
-open import Function.Base
-open import Level
+open import Level using (Level)
 
 import Effect.Monad.State.Transformer as Trans
 

src/Effect/Monad/State/Transformer.agda

@@ -6,21 +6,20 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level using (Level; suc; _⊔_)
 
 module Effect.Monad.State.Transformer where
 
 open import Algebra using (RawMonoid)
 open import Data.Product.Base using (_×_; _,_; map₂; proj₁; proj₂)
-open import Data.Unit.Polymorphic.Base
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
-
-open import Effect.Monad.Reader.Transformer using (RawMonadReader)
+open import Data.Unit.Polymorphic.Base using (tt)
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
+open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT; RawMonadTd)
+open import Function.Base using (_∘′_; _$_; const)
+open import Level using (Level; _⊔_)
+
 
 private
   variable

src/Effect/Monad/Writer.agda

@@ -10,13 +10,10 @@ module Effect.Monad.Writer where
 
 open import Algebra using (RawMonoid)
 open import Data.Product.Base using (_×_)
-open import Effect.Applicative
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Monad
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Monad using (RawMonad; module Join)
 open import Effect.Monad.Identity as Id using (Identity; runIdentity)
-open import Function.Base using (_∘′_)
 open import Level using (Level)
 
 import Effect.Monad.Writer.Transformer as Trans

src/Effect/Monad/Writer/Transformer.agda

@@ -11,13 +11,13 @@ module Effect.Monad.Writer.Transformer where
 
 open import Algebra using (RawMonoid)
 open import Data.Product.Base using (_×_; _,_; proj₂; map₂)
-open import Effect.Applicative
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Monad
+open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
 open import Function.Base using (_∘′_; const; _$_)
-open import Level using (Level; _⊔_; suc)
+open import Level using (Level)
 
 private
   variable