Agda.Interaction.Options.Lenses

Lenses for CommandLineOptions and PragmaOptions.

Add as needed.

Nothing smart happening here.

Pragma options

class LensPragmaOptions a where

Minimal complete definition

getPragmaOptions, lensPragmaOptions

Methods

getPragmaOptions :: a -> PragmaOptions

setPragmaOptions :: PragmaOptions -> a -> a

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> a -> a

lensPragmaOptions :: Lens' PragmaOptions a

Instances

LensPragmaOptions TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getPragmaOptions :: TCState -> PragmaOptions

setPragmaOptions :: PragmaOptions -> TCState -> TCState

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState

lensPragmaOptions :: Lens' PragmaOptions TCState

LensPragmaOptions CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPragmaOptions :: CommandLineOptions -> PragmaOptions

setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions

lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions

modifyPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM ()

Verbosity in the local pragma options

class LensVerbosity a where

Minimal complete definition

getVerbosity

Methods

getVerbosity :: a -> Verbosity

setVerbosity :: Verbosity -> a -> a

mapVerbosity :: (Verbosity -> Verbosity) -> a -> a

Instances

LensVerbosity TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getVerbosity :: TCState -> Verbosity

setVerbosity :: Verbosity -> TCState -> TCState

mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState

LensVerbosity PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getVerbosity :: PragmaOptions -> Verbosity

setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions

mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions

modifyVerbosity :: (Verbosity -> Verbosity) -> TCM ()

putVerbosity :: Verbosity -> TCM ()

Command line options

class LensCommandLineOptions a where

Minimal complete definition

getCommandLineOptions

Methods

getCommandLineOptions :: a -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> a -> a

mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a

Instances

LensCommandLineOptions TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getCommandLineOptions :: TCState -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> TCState -> TCState

mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState

LensCommandLineOptions PersistentTCState

Defined in Agda.Interaction.Options.Lenses

Methods

getCommandLineOptions :: PersistentTCState -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState

mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> PersistentTCState -> PersistentTCState

modifyCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCM ()

Safe mode

type SafeMode = Bool

class LensSafeMode a where

Minimal complete definition

getSafeMode

Methods

getSafeMode :: a -> SafeMode

setSafeMode :: SafeMode -> a -> a

mapSafeMode :: (SafeMode -> SafeMode) -> a -> a

Instances

LensSafeMode TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: TCState -> SafeMode

setSafeMode :: SafeMode -> TCState -> TCState

mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState

LensSafeMode PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: PragmaOptions -> SafeMode

setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions

mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions

LensSafeMode CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: CommandLineOptions -> SafeMode

setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions

mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions

LensSafeMode PersistentTCState

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: PersistentTCState -> SafeMode

setSafeMode :: SafeMode -> PersistentTCState -> PersistentTCState

mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState

modifySafeMode :: (SafeMode -> SafeMode) -> TCM ()

putSafeMode :: SafeMode -> TCM ()

builtinModulesWithSafePostulates :: Set FilePath

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

builtinModulesWithUnsafePostulates :: Set FilePath

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

primitiveModules :: Set FilePath

builtinModules :: Set FilePath

isBuiltinModule :: FilePath -> TCM Bool

isBuiltinModuleWithSafePostulates :: FilePath -> TCM Bool

Include directories

class LensIncludePaths a where

Minimal complete definition

getIncludePaths, getAbsoluteIncludePaths

Methods

getIncludePaths :: a -> [FilePath]

setIncludePaths :: [FilePath] -> a -> a

mapIncludePaths :: ([FilePath] -> [FilePath]) -> a -> a

getAbsoluteIncludePaths :: a -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> a -> a

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

Instances

LensIncludePaths TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: TCState -> [FilePath]

setIncludePaths :: [FilePath] -> TCState -> TCState

mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState

getAbsoluteIncludePaths :: TCState -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> TCState -> TCState

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState

LensIncludePaths CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath]

setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions

mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions

LensIncludePaths PersistentTCState

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: PersistentTCState -> [FilePath]

setIncludePaths :: [FilePath] -> PersistentTCState -> PersistentTCState

mapIncludePaths :: ([FilePath] -> [FilePath]) -> PersistentTCState -> PersistentTCState

getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> PersistentTCState -> PersistentTCState

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> PersistentTCState -> PersistentTCState

modifyIncludePaths :: ([FilePath] -> [FilePath]) -> TCM ()

putIncludePaths :: [FilePath] -> TCM ()

modifyAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCM ()

putAbsoluteIncludePaths :: [AbsolutePath] -> TCM ()

Include directories

type PersistentVerbosity = Verbosity

class LensPersistentVerbosity a where

Minimal complete definition

getPersistentVerbosity

Methods

getPersistentVerbosity :: a -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> a -> a

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a

Instances

LensPersistentVerbosity TCState

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: TCState -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCState -> TCState

LensPersistentVerbosity PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions

LensPersistentVerbosity CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions

LensPersistentVerbosity PersistentTCState

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: PersistentTCState -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> PersistentTCState -> PersistentTCState

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PersistentTCState -> PersistentTCState

modifyPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCM ()

putPersistentVerbosity :: PersistentVerbosity -> TCM ()