content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- | Lenses for 'CommandLineOptions' and 'PragmaOptions'.
  --
  --   Add as needed.
  --
  --   Nothing smart happening here.
  
  module Agda.Interaction.Options.Lenses where
  
  import Agda.TypeChecking.Monad.Base
  import Agda.TypeChecking.Monad.State
  import Agda.Interaction.Options
  
  import Agda.Utils.WithDefault (pattern Value)
  
  ---------------------------------------------------------------------------
  -- * Pragma options
  ---------------------------------------------------------------------------
  
  modifyPragmaOptions :: MonadTCState m => (PragmaOptions -> PragmaOptions) -> m ()
  modifyPragmaOptions = modifyTC . mapPragmaOptions
  
  ---------------------------------------------------------------------------
  -- ** Verbosity in the local pragma options
  ---------------------------------------------------------------------------
  
  class LensVerbosity a where
    getVerbosity :: a -> Verbosity
    setVerbosity :: Verbosity -> a -> a
    mapVerbosity :: (Verbosity -> Verbosity) -> a -> a
  
    -- default implementations
    setVerbosity     = mapVerbosity . const
    mapVerbosity f a = setVerbosity (f $ getVerbosity a) a
  
  instance LensVerbosity PragmaOptions where
    getVerbosity = _optVerbose
    setVerbosity is opts = opts { _optVerbose = is }
  
  instance LensVerbosity TCState where
    getVerbosity = getVerbosity . getPragmaOptions
    mapVerbosity = mapPragmaOptions . mapVerbosity
  
  modifyVerbosity :: MonadTCState m => (Verbosity -> Verbosity) -> m ()
  modifyVerbosity = modifyTC . mapVerbosity
  
  putVerbosity :: MonadTCState m => Verbosity -> m ()
  putVerbosity = modifyTC . setVerbosity
  
  ---------------------------------------------------------------------------
  -- * Command line options
  ---------------------------------------------------------------------------
  
  class LensCommandLineOptions a where
    getCommandLineOptions :: a -> CommandLineOptions
    setCommandLineOptions :: CommandLineOptions -> a -> a
    mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a
  
    -- default implementations
    setCommandLineOptions     = mapCommandLineOptions . const
    mapCommandLineOptions f a = setCommandLineOptions (f $ getCommandLineOptions a) a
  
  instance LensCommandLineOptions PersistentTCState where
    getCommandLineOptions = stPersistentOptions
    setCommandLineOptions opts st = st { stPersistentOptions = opts }
  
  instance LensCommandLineOptions TCState where
    getCommandLineOptions = getCommandLineOptions . stPersistentState
    mapCommandLineOptions = updatePersistentState . mapCommandLineOptions
  
  modifyCommandLineOptions :: MonadTCState m => (CommandLineOptions -> CommandLineOptions) -> m ()
  modifyCommandLineOptions = modifyTC . mapCommandLineOptions
  
  ---------------------------------------------------------------------------
  -- ** Safe mode
  ---------------------------------------------------------------------------
  
  type SafeMode = Bool
  
  class LensSafeMode a where
    getSafeMode :: a -> SafeMode
    setSafeMode :: SafeMode -> a -> a
    mapSafeMode :: (SafeMode -> SafeMode) -> a -> a
  
    -- default implementations
    setSafeMode     = mapSafeMode . const
    mapSafeMode f a = setSafeMode (f $ getSafeMode a) a
  
  instance LensSafeMode PragmaOptions where
    getSafeMode = optSafe
    setSafeMode is opts = opts { _optSafe = Value is } -- setSafeOption
  
  instance LensSafeMode CommandLineOptions where
    getSafeMode = getSafeMode . getPragmaOptions
    mapSafeMode = mapPragmaOptions . mapSafeMode
  
  instance LensSafeMode PersistentTCState where
    getSafeMode = getSafeMode . getCommandLineOptions
    mapSafeMode = mapCommandLineOptions . mapSafeMode
  
  instance LensSafeMode TCState where
    getSafeMode = getSafeMode . getCommandLineOptions
    mapSafeMode = mapCommandLineOptions . mapSafeMode
  
  modifySafeMode :: MonadTCState m => (SafeMode -> SafeMode) -> m ()
  modifySafeMode = modifyTC . mapSafeMode
  
  putSafeMode :: MonadTCState m => SafeMode -> m ()
  putSafeMode = modifyTC . setSafeMode
  
  ---------------------------------------------------------------------------
  -- ** Include directories
  ---------------------------------------------------------------------------
  
  class LensIncludePaths a where
    getAbsoluteIncludePaths :: a -> [AbsolutePath]
    setAbsoluteIncludePaths :: [AbsolutePath] -> a -> a
    mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> a -> a
  
    -- default implementations
    setAbsoluteIncludePaths     = mapAbsoluteIncludePaths . const
    mapAbsoluteIncludePaths f a = setAbsoluteIncludePaths (f $ getAbsoluteIncludePaths a) a
  
  instance LensIncludePaths CommandLineOptions where
    getAbsoluteIncludePaths = optAbsoluteIncludePaths
    setAbsoluteIncludePaths is opts = opts { optAbsoluteIncludePaths = is }
  
  instance LensIncludePaths PersistentTCState where
    getAbsoluteIncludePaths = getAbsoluteIncludePaths . getCommandLineOptions
    mapAbsoluteIncludePaths = mapCommandLineOptions . mapAbsoluteIncludePaths
  
  instance LensIncludePaths TCState where
    getAbsoluteIncludePaths = getAbsoluteIncludePaths . getCommandLineOptions
    mapAbsoluteIncludePaths = mapCommandLineOptions . mapAbsoluteIncludePaths
  
  modifyAbsoluteIncludePaths :: MonadTCState m => ([AbsolutePath] -> [AbsolutePath]) -> m ()
  modifyAbsoluteIncludePaths = modifyTC . mapAbsoluteIncludePaths
  
  putAbsoluteIncludePaths :: MonadTCState m => [AbsolutePath] -> m ()
  putAbsoluteIncludePaths = modifyTC . setAbsoluteIncludePaths
  
  ---------------------------------------------------------------------------
  -- ** Verbosity
  ---------------------------------------------------------------------------
  
  type PersistentVerbosity = Verbosity
  class LensPersistentVerbosity a where
    getPersistentVerbosity :: a -> PersistentVerbosity
    setPersistentVerbosity :: PersistentVerbosity -> a -> a
    mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a
  
    -- default implementations
    setPersistentVerbosity     = mapPersistentVerbosity . const
    mapPersistentVerbosity f a = setPersistentVerbosity (f $ getPersistentVerbosity a) a
  
  instance LensPersistentVerbosity PragmaOptions where
    getPersistentVerbosity = getVerbosity
    setPersistentVerbosity = setVerbosity
  
  instance LensPersistentVerbosity CommandLineOptions where
    getPersistentVerbosity = getPersistentVerbosity . getPragmaOptions
    mapPersistentVerbosity = mapPragmaOptions . mapPersistentVerbosity
  
  instance LensPersistentVerbosity PersistentTCState where
    getPersistentVerbosity = getPersistentVerbosity . getCommandLineOptions
    mapPersistentVerbosity = mapCommandLineOptions . mapPersistentVerbosity
  
  instance LensPersistentVerbosity TCState where
    getPersistentVerbosity = getPersistentVerbosity . getCommandLineOptions
    mapPersistentVerbosity = mapCommandLineOptions . mapPersistentVerbosity
  
  modifyPersistentVerbosity :: MonadTCState m => (PersistentVerbosity -> PersistentVerbosity) -> m ()
  modifyPersistentVerbosity = modifyTC . mapPersistentVerbosity
  
  putPersistentVerbosity :: MonadTCState m => PersistentVerbosity -> m ()
  putPersistentVerbosity = modifyTC . setPersistentVerbosity
  