{-# OPTIONS_GHC -Wunused-imports #-}

-- | Lenses for 'CommandLineOptions' and 'PragmaOptions'.
--
--   Add as needed.
--
--   Nothing smart happening here.

module Agda.Interaction.Options.Lenses where

import Control.Monad.IO.Class   ( MonadIO(..) )

import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set

import System.FilePath ((</>), joinPath, splitDirectories)

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.Library (getPrimitiveLibDir)
import Agda.Interaction.Options

import Agda.Utils.Lens        ()
import Agda.Utils.FileName
import Agda.Utils.Functor     ( (<.>) )
import Agda.Utils.WithDefault (pattern Value)

---------------------------------------------------------------------------
-- * Pragma options
---------------------------------------------------------------------------

modifyPragmaOptions :: MonadTCState m => (PragmaOptions -> PragmaOptions) -> m ()
modifyPragmaOptions :: forall (m :: * -> *).
MonadTCState m =>
(PragmaOptions -> PragmaOptions) -> m ()
modifyPragmaOptions = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ((PragmaOptions -> PragmaOptions) -> TCState -> TCState)
-> (PragmaOptions -> PragmaOptions)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PragmaOptions -> PragmaOptions) -> TCState -> TCState
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
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     = (Verbosity -> Verbosity) -> a -> a
forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity ((Verbosity -> Verbosity) -> a -> a)
-> (Verbosity -> Verbosity -> Verbosity) -> Verbosity -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Verbosity -> Verbosity -> Verbosity
forall a b. a -> b -> a
const
  mapVerbosity Verbosity -> Verbosity
f a
a = Verbosity -> a -> a
forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity (Verbosity -> Verbosity
f (Verbosity -> Verbosity) -> Verbosity -> Verbosity
forall a b. (a -> b) -> a -> b
$ a -> Verbosity
forall a. LensVerbosity a => a -> Verbosity
getVerbosity a
a) a
a

instance LensVerbosity PragmaOptions where
  getVerbosity :: PragmaOptions -> Verbosity
getVerbosity = PragmaOptions -> Verbosity
_optVerbose
  setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions
setVerbosity Verbosity
is PragmaOptions
opts = PragmaOptions
opts { _optVerbose = is }

instance LensVerbosity TCState where
  getVerbosity :: TCState -> Verbosity
getVerbosity = PragmaOptions -> Verbosity
forall a. LensVerbosity a => a -> Verbosity
getVerbosity (PragmaOptions -> Verbosity)
-> (TCState -> PragmaOptions) -> TCState -> Verbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PragmaOptions
forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState
mapVerbosity = (PragmaOptions -> PragmaOptions) -> TCState -> TCState
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions) -> TCState -> TCState)
-> ((Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions)
-> (Verbosity -> Verbosity)
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions
forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity

modifyVerbosity :: MonadTCState m => (Verbosity -> Verbosity) -> m ()
modifyVerbosity :: forall (m :: * -> *).
MonadTCState m =>
(Verbosity -> Verbosity) -> m ()
modifyVerbosity = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ((Verbosity -> Verbosity) -> TCState -> TCState)
-> (Verbosity -> Verbosity)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> TCState -> TCState
forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity

putVerbosity :: MonadTCState m => Verbosity -> m ()
putVerbosity :: forall (m :: * -> *). MonadTCState m => Verbosity -> m ()
putVerbosity = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> (Verbosity -> TCState -> TCState) -> Verbosity -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Verbosity -> TCState -> TCState
forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity

---------------------------------------------------------------------------
-- * Command line options
---------------------------------------------------------------------------

class LensCommandLineOptions a where
  getCommandLineOptions :: a -> CommandLineOptions
  setCommandLineOptions :: CommandLineOptions -> a -> a
  mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a

  -- default implementations
  setCommandLineOptions     = (CommandLineOptions -> CommandLineOptions) -> a -> a
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions) -> a -> a)
-> (CommandLineOptions -> CommandLineOptions -> CommandLineOptions)
-> CommandLineOptions
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> CommandLineOptions -> CommandLineOptions
forall a b. a -> b -> a
const
  mapCommandLineOptions CommandLineOptions -> CommandLineOptions
f a
a = CommandLineOptions -> a -> a
forall a. LensCommandLineOptions a => CommandLineOptions -> a -> a
setCommandLineOptions (CommandLineOptions -> CommandLineOptions
f (CommandLineOptions -> CommandLineOptions)
-> CommandLineOptions -> CommandLineOptions
forall a b. (a -> b) -> a -> b
$ a -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions a
a) a
a

instance LensCommandLineOptions PersistentTCState where
  getCommandLineOptions :: PersistentTCState -> CommandLineOptions
getCommandLineOptions = PersistentTCState -> CommandLineOptions
stPersistentOptions
  setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState
setCommandLineOptions CommandLineOptions
opts PersistentTCState
st = PersistentTCState
st { stPersistentOptions = opts }

instance LensCommandLineOptions TCState where
  getCommandLineOptions :: TCState -> CommandLineOptions
getCommandLineOptions = PersistentTCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
  mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
mapCommandLineOptions = (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
-> ((CommandLineOptions -> CommandLineOptions)
    -> PersistentTCState -> PersistentTCState)
-> (CommandLineOptions -> CommandLineOptions)
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CommandLineOptions -> CommandLineOptions)
-> PersistentTCState -> PersistentTCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions

modifyCommandLineOptions :: MonadTCState m => (CommandLineOptions -> CommandLineOptions) -> m ()
modifyCommandLineOptions :: forall (m :: * -> *).
MonadTCState m =>
(CommandLineOptions -> CommandLineOptions) -> m ()
modifyCommandLineOptions = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ((CommandLineOptions -> CommandLineOptions)
    -> TCState -> TCState)
-> (CommandLineOptions -> CommandLineOptions)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
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     = (SafeMode -> SafeMode) -> a -> a
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode ((SafeMode -> SafeMode) -> a -> a)
-> (SafeMode -> SafeMode -> SafeMode) -> SafeMode -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeMode -> SafeMode -> SafeMode
forall a b. a -> b -> a
const
  mapSafeMode SafeMode -> SafeMode
f a
a = SafeMode -> a -> a
forall a. LensSafeMode a => SafeMode -> a -> a
setSafeMode (SafeMode -> SafeMode
f (SafeMode -> SafeMode) -> SafeMode -> SafeMode
forall a b. (a -> b) -> a -> b
$ a -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
getSafeMode a
a) a
a

instance LensSafeMode PragmaOptions where
  getSafeMode :: PragmaOptions -> SafeMode
getSafeMode = PragmaOptions -> SafeMode
optSafe
  setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions
setSafeMode SafeMode
is PragmaOptions
opts = PragmaOptions
opts { _optSafe = Value is } -- setSafeOption

instance LensSafeMode CommandLineOptions where
  getSafeMode :: CommandLineOptions -> SafeMode
getSafeMode = PragmaOptions -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
getSafeMode (PragmaOptions -> SafeMode)
-> (CommandLineOptions -> PragmaOptions)
-> CommandLineOptions
-> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> PragmaOptions
forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions
mapSafeMode = (PragmaOptions -> PragmaOptions)
-> CommandLineOptions -> CommandLineOptions
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions)
 -> CommandLineOptions -> CommandLineOptions)
-> ((SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions)
-> (SafeMode -> SafeMode)
-> CommandLineOptions
-> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

instance LensSafeMode PersistentTCState where
  getSafeMode :: PersistentTCState -> SafeMode
getSafeMode = CommandLineOptions -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
getSafeMode (CommandLineOptions -> SafeMode)
-> (PersistentTCState -> CommandLineOptions)
-> PersistentTCState
-> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState
mapSafeMode = (CommandLineOptions -> CommandLineOptions)
-> PersistentTCState -> PersistentTCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions)
 -> PersistentTCState -> PersistentTCState)
-> ((SafeMode -> SafeMode)
    -> CommandLineOptions -> CommandLineOptions)
-> (SafeMode -> SafeMode)
-> PersistentTCState
-> PersistentTCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

instance LensSafeMode TCState where
  getSafeMode :: TCState -> SafeMode
getSafeMode = CommandLineOptions -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
getSafeMode (CommandLineOptions -> SafeMode)
-> (TCState -> CommandLineOptions) -> TCState -> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState
mapSafeMode = (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions) -> TCState -> TCState)
-> ((SafeMode -> SafeMode)
    -> CommandLineOptions -> CommandLineOptions)
-> (SafeMode -> SafeMode)
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

modifySafeMode :: MonadTCState m => (SafeMode -> SafeMode) -> m ()
modifySafeMode :: forall (m :: * -> *).
MonadTCState m =>
(SafeMode -> SafeMode) -> m ()
modifySafeMode = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ((SafeMode -> SafeMode) -> TCState -> TCState)
-> (SafeMode -> SafeMode)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SafeMode -> SafeMode) -> TCState -> TCState
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

putSafeMode :: MonadTCState m => SafeMode -> m ()
putSafeMode :: forall (m :: * -> *). MonadTCState m => SafeMode -> m ()
putSafeMode = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> (SafeMode -> TCState -> TCState) -> SafeMode -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeMode -> TCState -> TCState
forall a. LensSafeMode a => SafeMode -> a -> a
setSafeMode

-- | These builtins may use postulates, and are still considered --safe

builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates =
  Set FilePath
primitiveModules Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ([FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Bool.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Char.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Char" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Coinduction.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Equiv.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Glue.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"HCompU.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Id.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Path.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Sub.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Erase.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Float.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Float" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromNat.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromNeg.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromString.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Int.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"IO.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"List.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Maybe.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Nat.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"External.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Sigma.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Size.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Strict.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"String.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"String" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Unit.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Word.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Word" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  ])

-- | These builtins may not use postulates under --safe. They are not
--   automatically unsafe, but will be if they use an unsafe feature.

builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates = [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"TrustMe.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Rewrite.agda"
  ]

primitiveModules :: Set FilePath
primitiveModules :: Set FilePath
primitiveModules = [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical.agda"
  ]

builtinModules :: Set FilePath
builtinModules :: Set FilePath
builtinModules = Set FilePath
builtinModulesWithSafePostulates Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union`
                 Set FilePath
builtinModulesWithUnsafePostulates

isPrimitiveModule :: MonadIO m => FilePath -> m Bool
isPrimitiveModule :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isPrimitiveModule = Set FilePath -> FilePath -> m SafeMode
forall (m :: * -> *).
MonadIO m =>
Set FilePath -> FilePath -> m SafeMode
isPrimitiveModuleFrom Set FilePath
primitiveModules

isBuiltinModule :: MonadIO m => FilePath -> m Bool
isBuiltinModule :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isBuiltinModule = Set FilePath -> FilePath -> m SafeMode
forall (m :: * -> *).
MonadIO m =>
Set FilePath -> FilePath -> m SafeMode
isPrimitiveModuleFrom Set FilePath
builtinModules

isBuiltinModuleWithSafePostulates :: MonadIO m => FilePath -> m Bool
isBuiltinModuleWithSafePostulates :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isBuiltinModuleWithSafePostulates = Set FilePath -> FilePath -> m SafeMode
forall (m :: * -> *).
MonadIO m =>
Set FilePath -> FilePath -> m SafeMode
isPrimitiveModuleFrom Set FilePath
builtinModulesWithSafePostulates

-- | Check whether a 'FilePath' is one of the primitive modules mentioned in @Set FilePath@.
--
isPrimitiveModuleFrom :: MonadIO m => Set FilePath -> FilePath -> m Bool
isPrimitiveModuleFrom :: forall (m :: * -> *).
MonadIO m =>
Set FilePath -> FilePath -> m SafeMode
isPrimitiveModuleFrom Set FilePath
s = SafeMode -> (FilePath -> SafeMode) -> Maybe FilePath -> SafeMode
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SafeMode
False (FilePath -> Set FilePath -> SafeMode
forall a. Ord a => a -> Set a -> SafeMode
`Set.member` Set FilePath
s) (Maybe FilePath -> SafeMode)
-> (FilePath -> m (Maybe FilePath)) -> FilePath -> m SafeMode
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> FilePath -> m (Maybe FilePath)
forall (m :: * -> *). MonadIO m => FilePath -> m (Maybe FilePath)
stripPrimitiveLibDir

-- | Strip the 'getPrimitiveLibDir' off the given 'FilePath',
--   returning the suffix if successful.
--
stripPrimitiveLibDir :: MonadIO m => FilePath -> m (Maybe FilePath)
stripPrimitiveLibDir :: forall (m :: * -> *). MonadIO m => FilePath -> m (Maybe FilePath)
stripPrimitiveLibDir FilePath
file = IO (Maybe FilePath) -> m (Maybe FilePath)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe FilePath) -> m (Maybe FilePath))
-> IO (Maybe FilePath) -> m (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ do
  primPath <- FilePath -> [FilePath]
splitDirectories (FilePath -> [FilePath]) -> IO FilePath -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath
getPrimitiveLibDir
  let filePath = FilePath -> [FilePath]
splitDirectories FilePath
file
  return $ fmap joinPath $ List.stripPrefix primPath filePath


---------------------------------------------------------------------------
-- ** Include directories
---------------------------------------------------------------------------

class LensIncludePaths a where
  getIncludePaths :: a -> [FilePath]
  setIncludePaths :: [FilePath] -> a -> a
  mapIncludePaths :: ([FilePath] -> [FilePath]) -> a -> a

  getAbsoluteIncludePaths :: a -> [AbsolutePath]
  setAbsoluteIncludePaths :: [AbsolutePath] -> a -> a
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> a -> a

  -- default implementations
  setIncludePaths     = ([FilePath] -> [FilePath]) -> a -> a
forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths (([FilePath] -> [FilePath]) -> a -> a)
-> ([FilePath] -> [FilePath] -> [FilePath]) -> [FilePath] -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> [FilePath] -> [FilePath]
forall a b. a -> b -> a
const
  mapIncludePaths [FilePath] -> [FilePath]
f a
a = [FilePath] -> a -> a
forall a. LensIncludePaths a => [FilePath] -> a -> a
setIncludePaths ([FilePath] -> [FilePath]
f ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ a -> [FilePath]
forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths a
a) a
a
  setAbsoluteIncludePaths     = ([AbsolutePath] -> [AbsolutePath]) -> a -> a
forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths (([AbsolutePath] -> [AbsolutePath]) -> a -> a)
-> ([AbsolutePath] -> [AbsolutePath] -> [AbsolutePath])
-> [AbsolutePath]
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AbsolutePath] -> [AbsolutePath] -> [AbsolutePath]
forall a b. a -> b -> a
const
  mapAbsoluteIncludePaths [AbsolutePath] -> [AbsolutePath]
f a
a = [AbsolutePath] -> a -> a
forall a. LensIncludePaths a => [AbsolutePath] -> a -> a
setAbsoluteIncludePaths ([AbsolutePath] -> [AbsolutePath]
f ([AbsolutePath] -> [AbsolutePath])
-> [AbsolutePath] -> [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ a -> [AbsolutePath]
forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths a
a) a
a

instance LensIncludePaths CommandLineOptions where
  getIncludePaths :: CommandLineOptions -> [FilePath]
getIncludePaths = CommandLineOptions -> [FilePath]
optIncludePaths
  setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions
setIncludePaths [FilePath]
is CommandLineOptions
opts = CommandLineOptions
opts { optIncludePaths = is }
  getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath]
getAbsoluteIncludePaths = CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths
  setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions
setAbsoluteIncludePaths [AbsolutePath]
is CommandLineOptions
opts = CommandLineOptions
opts { optAbsoluteIncludePaths = is }

instance LensIncludePaths PersistentTCState where
  getIncludePaths :: PersistentTCState -> [FilePath]
getIncludePaths = CommandLineOptions -> [FilePath]
forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths (CommandLineOptions -> [FilePath])
-> (PersistentTCState -> CommandLineOptions)
-> PersistentTCState
-> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapIncludePaths :: ([FilePath] -> [FilePath])
-> PersistentTCState -> PersistentTCState
mapIncludePaths = (CommandLineOptions -> CommandLineOptions)
-> PersistentTCState -> PersistentTCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions)
 -> PersistentTCState -> PersistentTCState)
-> (([FilePath] -> [FilePath])
    -> CommandLineOptions -> CommandLineOptions)
-> ([FilePath] -> [FilePath])
-> PersistentTCState
-> PersistentTCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FilePath] -> [FilePath])
-> CommandLineOptions -> CommandLineOptions
forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths
  getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath]
getAbsoluteIncludePaths = CommandLineOptions -> [AbsolutePath]
forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths (CommandLineOptions -> [AbsolutePath])
-> (PersistentTCState -> CommandLineOptions)
-> PersistentTCState
-> [AbsolutePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath])
-> PersistentTCState -> PersistentTCState
mapAbsoluteIncludePaths = (CommandLineOptions -> CommandLineOptions)
-> PersistentTCState -> PersistentTCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions)
 -> PersistentTCState -> PersistentTCState)
-> (([AbsolutePath] -> [AbsolutePath])
    -> CommandLineOptions -> CommandLineOptions)
-> ([AbsolutePath] -> [AbsolutePath])
-> PersistentTCState
-> PersistentTCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([AbsolutePath] -> [AbsolutePath])
-> CommandLineOptions -> CommandLineOptions
forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

instance LensIncludePaths TCState where
  getIncludePaths :: TCState -> [FilePath]
getIncludePaths = CommandLineOptions -> [FilePath]
forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths (CommandLineOptions -> [FilePath])
-> (TCState -> CommandLineOptions) -> TCState -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState
mapIncludePaths = (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions) -> TCState -> TCState)
-> (([FilePath] -> [FilePath])
    -> CommandLineOptions -> CommandLineOptions)
-> ([FilePath] -> [FilePath])
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FilePath] -> [FilePath])
-> CommandLineOptions -> CommandLineOptions
forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths
  getAbsoluteIncludePaths :: TCState -> [AbsolutePath]
getAbsoluteIncludePaths = CommandLineOptions -> [AbsolutePath]
forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths (CommandLineOptions -> [AbsolutePath])
-> (TCState -> CommandLineOptions) -> TCState -> [AbsolutePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState
mapAbsoluteIncludePaths = (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions) -> TCState -> TCState)
-> (([AbsolutePath] -> [AbsolutePath])
    -> CommandLineOptions -> CommandLineOptions)
-> ([AbsolutePath] -> [AbsolutePath])
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([AbsolutePath] -> [AbsolutePath])
-> CommandLineOptions -> CommandLineOptions
forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

modifyIncludePaths :: MonadTCState m => ([FilePath] -> [FilePath]) -> m ()
modifyIncludePaths :: forall (m :: * -> *).
MonadTCState m =>
([FilePath] -> [FilePath]) -> m ()
modifyIncludePaths = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> (([FilePath] -> [FilePath]) -> TCState -> TCState)
-> ([FilePath] -> [FilePath])
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FilePath] -> [FilePath]) -> TCState -> TCState
forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths

putIncludePaths :: MonadTCState m => [FilePath] -> m ()
putIncludePaths :: forall (m :: * -> *). MonadTCState m => [FilePath] -> m ()
putIncludePaths = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ([FilePath] -> TCState -> TCState) -> [FilePath] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> TCState -> TCState
forall a. LensIncludePaths a => [FilePath] -> a -> a
setIncludePaths

modifyAbsoluteIncludePaths :: MonadTCState m => ([AbsolutePath] -> [AbsolutePath]) -> m ()
modifyAbsoluteIncludePaths :: forall (m :: * -> *).
MonadTCState m =>
([AbsolutePath] -> [AbsolutePath]) -> m ()
modifyAbsoluteIncludePaths = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> (([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState)
-> ([AbsolutePath] -> [AbsolutePath])
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState
forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

putAbsoluteIncludePaths :: MonadTCState m => [AbsolutePath] -> m ()
putAbsoluteIncludePaths :: forall (m :: * -> *). MonadTCState m => [AbsolutePath] -> m ()
putAbsoluteIncludePaths = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ([AbsolutePath] -> TCState -> TCState) -> [AbsolutePath] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AbsolutePath] -> TCState -> TCState
forall a. LensIncludePaths a => [AbsolutePath] -> a -> a
setAbsoluteIncludePaths

---------------------------------------------------------------------------
-- ** Include directories
---------------------------------------------------------------------------

type PersistentVerbosity = Verbosity
class LensPersistentVerbosity a where
  getPersistentVerbosity :: a -> PersistentVerbosity
  setPersistentVerbosity :: PersistentVerbosity -> a -> a
  mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a

  -- default implementations
  setPersistentVerbosity     = (Verbosity -> Verbosity) -> a -> a
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity ((Verbosity -> Verbosity) -> a -> a)
-> (Verbosity -> Verbosity -> Verbosity) -> Verbosity -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Verbosity -> Verbosity -> Verbosity
forall a b. a -> b -> a
const
  mapPersistentVerbosity Verbosity -> Verbosity
f a
a = Verbosity -> a -> a
forall a. LensPersistentVerbosity a => Verbosity -> a -> a
setPersistentVerbosity (Verbosity -> Verbosity
f (Verbosity -> Verbosity) -> Verbosity -> Verbosity
forall a b. (a -> b) -> a -> b
$ a -> Verbosity
forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity a
a) a
a

instance LensPersistentVerbosity PragmaOptions where
  getPersistentVerbosity :: PragmaOptions -> Verbosity
getPersistentVerbosity = PragmaOptions -> Verbosity
forall a. LensVerbosity a => a -> Verbosity
getVerbosity
  setPersistentVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions
setPersistentVerbosity = Verbosity -> PragmaOptions -> PragmaOptions
forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity

instance LensPersistentVerbosity CommandLineOptions where
  getPersistentVerbosity :: CommandLineOptions -> Verbosity
getPersistentVerbosity = PragmaOptions -> Verbosity
forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity (PragmaOptions -> Verbosity)
-> (CommandLineOptions -> PragmaOptions)
-> CommandLineOptions
-> Verbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> PragmaOptions
forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity)
-> CommandLineOptions -> CommandLineOptions
mapPersistentVerbosity = (PragmaOptions -> PragmaOptions)
-> CommandLineOptions -> CommandLineOptions
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions)
 -> CommandLineOptions -> CommandLineOptions)
-> ((Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions)
-> (Verbosity -> Verbosity)
-> CommandLineOptions
-> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

instance LensPersistentVerbosity PersistentTCState where
  getPersistentVerbosity :: PersistentTCState -> Verbosity
getPersistentVerbosity = CommandLineOptions -> Verbosity
forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity (CommandLineOptions -> Verbosity)
-> (PersistentTCState -> CommandLineOptions)
-> PersistentTCState
-> Verbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity) -> PersistentTCState -> PersistentTCState
mapPersistentVerbosity = (CommandLineOptions -> CommandLineOptions)
-> PersistentTCState -> PersistentTCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions)
 -> PersistentTCState -> PersistentTCState)
-> ((Verbosity -> Verbosity)
    -> CommandLineOptions -> CommandLineOptions)
-> (Verbosity -> Verbosity)
-> PersistentTCState
-> PersistentTCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity)
-> CommandLineOptions -> CommandLineOptions
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

instance LensPersistentVerbosity TCState where
  getPersistentVerbosity :: TCState -> Verbosity
getPersistentVerbosity = CommandLineOptions -> Verbosity
forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity (CommandLineOptions -> Verbosity)
-> (TCState -> CommandLineOptions) -> TCState -> Verbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> CommandLineOptions
forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState
mapPersistentVerbosity = (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions ((CommandLineOptions -> CommandLineOptions) -> TCState -> TCState)
-> ((Verbosity -> Verbosity)
    -> CommandLineOptions -> CommandLineOptions)
-> (Verbosity -> Verbosity)
-> TCState
-> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity)
-> CommandLineOptions -> CommandLineOptions
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

modifyPersistentVerbosity :: MonadTCState m => (PersistentVerbosity -> PersistentVerbosity) -> m ()
modifyPersistentVerbosity :: forall (m :: * -> *).
MonadTCState m =>
(Verbosity -> Verbosity) -> m ()
modifyPersistentVerbosity = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> ((Verbosity -> Verbosity) -> TCState -> TCState)
-> (Verbosity -> Verbosity)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> TCState -> TCState
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

putPersistentVerbosity :: MonadTCState m => PersistentVerbosity -> m ()
putPersistentVerbosity :: forall (m :: * -> *). MonadTCState m => Verbosity -> m ()
putPersistentVerbosity = (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ())
-> (Verbosity -> TCState -> TCState) -> Verbosity -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Verbosity -> TCState -> TCState
forall a. LensPersistentVerbosity a => Verbosity -> a -> a
setPersistentVerbosity