{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Interaction.Options.HasOptions
  ( HasOptions (pragmaOptions, commandLineOptions)
  ) where

import Control.Monad.Except (ExceptT)
import Control.Monad.Reader (ReaderT)
import Control.Monad.State (StateT)
import Control.Monad.Trans ( MonadTrans, lift )
import Control.Monad.Trans.Identity (IdentityT)
import Control.Monad.Trans.Maybe (MaybeT)
import Control.Monad.Writer (WriterT)

import Agda.Interaction.Options.Types (PragmaOptions, CommandLineOptions)
import Agda.Utils.Update (ChangeT)
import Agda.Utils.ListT (ListT)
import Agda.Utils.StrictReader qualified as Strict
import Agda.Utils.StrictWriter qualified as Strict
import Agda.Utils.StrictState  qualified as Strict

class (Functor m, Applicative m, Monad m) => HasOptions m where
  -- | Returns the pragma options which are currently in effect.
  pragmaOptions      :: m PragmaOptions
  -- | Returns the command line options which are currently in effect.
  commandLineOptions :: m CommandLineOptions

  default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions
  pragmaOptions      = n PragmaOptions -> t n PragmaOptions
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions
  commandLineOptions = n CommandLineOptions -> t n CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

-- HasOptions lifts through monad transformers
-- (see default signatures in the HasOptions class).

instance HasOptions m => HasOptions (ChangeT m)
instance HasOptions m => HasOptions (ExceptT e m)
instance HasOptions m => HasOptions (IdentityT m)
instance HasOptions m => HasOptions (ListT m)
instance HasOptions m => HasOptions (MaybeT m)
instance HasOptions m => HasOptions (ReaderT r m)
instance HasOptions m => HasOptions (StateT s m)
instance (HasOptions m, Monoid w) => HasOptions (WriterT w m)
instance HasOptions m => HasOptions (Strict.ReaderT r m)
instance HasOptions m => HasOptions (Strict.StateT s m)
instance (HasOptions m, Monoid w) => HasOptions (Strict.WriterT w m)