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

module Agda.Interaction.Options.Lenses where

import Control.Monad.State

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

import System.FilePath ((</>))

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.Options

import Agda.Utils.Lens
import Agda.Utils.FileName

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

class LensPragmaOptions a where
  getPragmaOptions  :: a -> PragmaOptions
  setPragmaOptions  :: PragmaOptions -> a -> a
  mapPragmaOptions  :: (PragmaOptions -> PragmaOptions) -> a -> a
  lensPragmaOptions :: Lens' PragmaOptions a
  -- lensPragmaOptions :: forall f. Functor f => (PragmaOptions -> f PragmaOptions) -> a -> f a

  -- default implementations
  setPragmaOptions     = (PragmaOptions -> PragmaOptions) -> a -> a
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions) -> a -> a)
-> (PragmaOptions -> PragmaOptions -> PragmaOptions)
-> PragmaOptions
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> PragmaOptions -> PragmaOptions
forall a b. a -> b -> a
const
  mapPragmaOptions PragmaOptions -> PragmaOptions
f a
a = PragmaOptions -> a -> a
forall a. LensPragmaOptions a => PragmaOptions -> a -> a
setPragmaOptions (PragmaOptions -> PragmaOptions
f (PragmaOptions -> PragmaOptions) -> PragmaOptions -> PragmaOptions
forall a b. (a -> b) -> a -> b
$ a -> PragmaOptions
forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions a
a) a
a

instance LensPragmaOptions CommandLineOptions where
  getPragmaOptions :: CommandLineOptions -> PragmaOptions
getPragmaOptions = CommandLineOptions -> PragmaOptions
optPragmaOptions
  setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions
setPragmaOptions PragmaOptions
opts CommandLineOptions
st = CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }
  lensPragmaOptions :: (PragmaOptions -> f PragmaOptions)
-> CommandLineOptions -> f CommandLineOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) f PragmaOptions
-> (PragmaOptions -> CommandLineOptions) -> f CommandLineOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }

instance LensPragmaOptions TCState where
  getPragmaOptions :: TCState -> PragmaOptions
getPragmaOptions = (TCState -> Lens' PragmaOptions TCState -> PragmaOptions
forall o i. o -> Lens' i o -> i
^.Lens' PragmaOptions TCState
stPragmaOptions)
  setPragmaOptions :: PragmaOptions -> TCState -> TCState
setPragmaOptions = Lens' PragmaOptions TCState -> PragmaOptions -> TCState -> TCState
forall i o. Lens' i o -> LensSet i o
set Lens' PragmaOptions TCState
stPragmaOptions
  lensPragmaOptions :: (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
lensPragmaOptions = (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' PragmaOptions TCState
stPragmaOptions

modifyPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM ()
modifyPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM ()
modifyPragmaOptions = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((PragmaOptions -> PragmaOptions) -> TCState -> TCState)
-> (PragmaOptions -> PragmaOptions)
-> TCM ()
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 :: Verbosity
optVerbose = Verbosity
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 :: (Verbosity -> Verbosity) -> TCM ()
modifyVerbosity :: (Verbosity -> Verbosity) -> TCM ()
modifyVerbosity = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((Verbosity -> Verbosity) -> TCState -> TCState)
-> (Verbosity -> Verbosity)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> TCState -> TCState
forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity

putVerbosity :: Verbosity -> TCM ()
putVerbosity :: Verbosity -> TCM ()
putVerbosity = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> (Verbosity -> TCState -> TCState) -> Verbosity -> TCM ()
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 :: CommandLineOptions
stPersistentOptions = CommandLineOptions
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 :: (CommandLineOptions -> CommandLineOptions) -> TCM ()
modifyCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCM ()
modifyCommandLineOptions = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((CommandLineOptions -> CommandLineOptions)
    -> TCState -> TCState)
-> (CommandLineOptions -> CommandLineOptions)
-> TCM ()
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 :: SafeMode
optSafe = SafeMode
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 :: (SafeMode -> SafeMode) -> TCM ()
modifySafeMode :: (SafeMode -> SafeMode) -> TCM ()
modifySafeMode = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((SafeMode -> SafeMode) -> TCState -> TCState)
-> (SafeMode -> SafeMode)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SafeMode -> SafeMode) -> TCState -> TCState
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

putSafeMode :: SafeMode -> TCM ()
putSafeMode :: SafeMode -> TCM ()
putSafeMode = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> (SafeMode -> TCState -> TCState) -> SafeMode -> TCM ()
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
"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
"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
"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

isBuiltinModule :: FilePath -> TCM Bool
isBuiltinModule :: FilePath -> TCM SafeMode
isBuiltinModule FilePath
file = do
  FilePath
libdirPrim <- (FilePath -> FilePath -> FilePath
</> FilePath
"prim") (FilePath -> FilePath) -> TCMT IO FilePath -> TCMT IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath -> TCMT IO FilePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
defaultLibDir
  SafeMode -> TCM SafeMode
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
file FilePath -> Set FilePath -> SafeMode
forall a. Ord a => a -> Set a -> SafeMode
`Set.member` (FilePath -> FilePath) -> Set FilePath -> Set FilePath
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath
libdirPrim FilePath -> FilePath -> FilePath
</>) Set FilePath
builtinModules)

isBuiltinModuleWithSafePostulates :: FilePath -> TCM Bool
isBuiltinModuleWithSafePostulates :: FilePath -> TCM SafeMode
isBuiltinModuleWithSafePostulates FilePath
file = do
  FilePath
libdirPrim <- (FilePath -> FilePath -> FilePath
</> FilePath
"prim") (FilePath -> FilePath) -> TCMT IO FilePath -> TCMT IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath -> TCMT IO FilePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
defaultLibDir
  let safeBuiltins :: Set FilePath
safeBuiltins   = (FilePath -> FilePath) -> Set FilePath -> Set FilePath
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath
libdirPrim FilePath -> FilePath -> FilePath
</>) Set FilePath
builtinModulesWithSafePostulates
  SafeMode -> TCM SafeMode
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
file FilePath -> Set FilePath -> SafeMode
forall a. Ord a => a -> Set a -> SafeMode
`Set.member` Set FilePath
safeBuiltins)

---------------------------------------------------------------------------
-- ** 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 :: [FilePath]
optIncludePaths = [FilePath]
is }
  getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath]
getAbsoluteIncludePaths = CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths
  setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions
setAbsoluteIncludePaths [AbsolutePath]
is CommandLineOptions
opts = CommandLineOptions
opts { optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths = [AbsolutePath]
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 :: ([FilePath] -> [FilePath]) -> TCM ()
modifyIncludePaths :: ([FilePath] -> [FilePath]) -> TCM ()
modifyIncludePaths = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> (([FilePath] -> [FilePath]) -> TCState -> TCState)
-> ([FilePath] -> [FilePath])
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FilePath] -> [FilePath]) -> TCState -> TCState
forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths

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

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

putAbsoluteIncludePaths :: [AbsolutePath] -> TCM ()
putAbsoluteIncludePaths :: [AbsolutePath] -> TCM ()
putAbsoluteIncludePaths = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ([AbsolutePath] -> TCState -> TCState)
-> [AbsolutePath]
-> TCM ()
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 :: (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
modifyPersistentVerbosity :: (Verbosity -> Verbosity) -> TCM ()
modifyPersistentVerbosity = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((Verbosity -> Verbosity) -> TCState -> TCState)
-> (Verbosity -> Verbosity)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> Verbosity) -> TCState -> TCState
forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

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