Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Options.Lenses

Contents

- Pragma options
  - Verbosity in the local pragma options
- Command line options
  - Safe mode
  - Include directories
  - Include directories

Description

Lenses for `CommandLineOptions` and `PragmaOptions`.

Add as needed.

Nothing smart happening here.

Synopsis

- class LensPragmaOptions a where
  - getPragmaOptions :: a -> PragmaOptions
  - setPragmaOptions :: PragmaOptions -> a -> a
  - mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> a -> a
  - lensPragmaOptions :: Lens' PragmaOptions a
- modifyPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM ()
- class LensVerbosity a where
  - getVerbosity :: a -> Verbosity
  - setVerbosity :: Verbosity -> a -> a
  - mapVerbosity :: (Verbosity -> Verbosity) -> a -> a
- modifyVerbosity :: (Verbosity -> Verbosity) -> TCM ()
- putVerbosity :: Verbosity -> TCM ()
- class LensCommandLineOptions a where
  - getCommandLineOptions :: a -> CommandLineOptions
  - setCommandLineOptions :: CommandLineOptions -> a -> a
  - mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a
- modifyCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCM ()
- type SafeMode = Bool
- class LensSafeMode a where
  - getSafeMode :: a -> SafeMode
  - setSafeMode :: SafeMode -> a -> a
  - mapSafeMode :: (SafeMode -> SafeMode) -> a -> a
- modifySafeMode :: (SafeMode -> SafeMode) -> TCM ()
- putSafeMode :: SafeMode -> TCM ()
- builtinModulesWithSafePostulates :: Set FilePath
- builtinModulesWithUnsafePostulates :: Set FilePath
- primitiveModules :: Set FilePath
- builtinModules :: Set FilePath
- isBuiltinModule :: FilePath -> TCM Bool
- isBuiltinModuleWithSafePostulates :: FilePath -> TCM Bool
- 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
- modifyIncludePaths :: ([FilePath] -> [FilePath]) -> TCM ()
- putIncludePaths :: [FilePath] -> TCM ()
- modifyAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCM ()
- putAbsoluteIncludePaths :: [AbsolutePath] -> TCM ()
- type PersistentVerbosity = Verbosity
- class LensPersistentVerbosity a where
  - getPersistentVerbosity :: a -> PersistentVerbosity
  - setPersistentVerbosity :: PersistentVerbosity -> a -> a
  - mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a
- modifyPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
- putPersistentVerbosity :: PersistentVerbosity -> TCM ()

# Pragma options

class LensPragmaOptions a where Source #

Minimal complete definition

getPragmaOptions, lensPragmaOptions

Methods

getPragmaOptions :: a -> PragmaOptions Source #

setPragmaOptions :: PragmaOptions -> a -> a Source #

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

lensPragmaOptions :: Lens' PragmaOptions a Source #

Instances

LensPragmaOptions TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: TCState -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> TCState -> TCState Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState Source # lensPragmaOptions :: Lens' PragmaOptions TCState Source #
LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions Source #

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

## Verbosity in the local pragma options

class LensVerbosity a where Source #

Minimal complete definition

getVerbosity

Methods

getVerbosity :: a -> Verbosity Source #

setVerbosity :: Verbosity -> a -> a Source #

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

Instances

LensVerbosity TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: TCState -> Verbosity Source # setVerbosity :: Verbosity -> TCState -> TCState Source # mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState Source #
LensVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #

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

putVerbosity :: Verbosity -> TCM () Source #

# Command line options

class LensCommandLineOptions a where Source #

Minimal complete definition

getCommandLineOptions

Methods

getCommandLineOptions :: a -> CommandLineOptions Source #

setCommandLineOptions :: CommandLineOptions -> a -> a Source #

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

Instances

LensCommandLineOptions TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: TCState -> CommandLineOptions Source # setCommandLineOptions :: CommandLineOptions -> TCState -> TCState Source # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState Source #
LensCommandLineOptions PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: PersistentTCState -> CommandLineOptions Source # setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState Source # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> PersistentTCState -> PersistentTCState Source #

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

## Safe mode

type SafeMode = Bool Source #

class LensSafeMode a where Source #

Minimal complete definition

getSafeMode

Methods

getSafeMode :: a -> SafeMode Source #

setSafeMode :: SafeMode -> a -> a Source #

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

Instances

LensSafeMode TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: TCState -> SafeMode Source # setSafeMode :: SafeMode -> TCState -> TCState Source # mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState Source #
LensSafeMode PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
LensSafeMode PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PersistentTCState -> SafeMode Source # setSafeMode :: SafeMode -> PersistentTCState -> PersistentTCState Source # mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState Source #

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

putSafeMode :: SafeMode -> TCM () Source #

builtinModulesWithSafePostulates :: Set FilePath Source #

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

builtinModulesWithUnsafePostulates :: Set FilePath Source #

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 Source #

builtinModules :: Set FilePath Source #

isBuiltinModule :: FilePath -> TCM Bool Source #

isBuiltinModuleWithSafePostulates :: FilePath -> TCM Bool Source #

## Include directories

class LensIncludePaths a where Source #

Minimal complete definition

getIncludePaths, getAbsoluteIncludePaths

Methods

getIncludePaths :: a -> [FilePath] Source #

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

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

getAbsoluteIncludePaths :: a -> [AbsolutePath] Source #

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

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

Instances

LensIncludePaths TCState Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: TCState -> [FilePath] Source #

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

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

getAbsoluteIncludePaths :: TCState -> [AbsolutePath] Source #

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

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

LensIncludePaths CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath] Source #

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

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

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source #

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

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

LensIncludePaths PersistentTCState Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: PersistentTCState -> [FilePath] Source #

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

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

getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath] Source #

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

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

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

putIncludePaths :: [FilePath] -> TCM () Source #

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

putAbsoluteIncludePaths :: [AbsolutePath] -> TCM () Source #

## Include directories

type PersistentVerbosity = Verbosity Source #

class LensPersistentVerbosity a where Source #

Minimal complete definition

getPersistentVerbosity

Methods

getPersistentVerbosity :: a -> PersistentVerbosity Source #

setPersistentVerbosity :: PersistentVerbosity -> a -> a Source #

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

Instances

LensPersistentVerbosity TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: TCState -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCState -> TCState Source #
LensPersistentVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensPersistentVerbosity CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensPersistentVerbosity PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PersistentTCState -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PersistentTCState -> PersistentTCState Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PersistentTCState -> PersistentTCState Source #

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

putPersistentVerbosity :: PersistentVerbosity -> TCM () Source #