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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Options

Synopsis

- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
- libToTCM :: LibM a -> TCM a
- setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
- addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- setOptionsFromPragma :: OptionsPragma -> TCM ()
- enableDisplayForms :: TCM a -> TCM a
- disableDisplayForms :: TCM a -> TCM a
- displayFormsEnabled :: TCM Bool
- getIncludeDirs :: TCM [AbsolutePath]
- setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
- setInputFile :: FilePath -> TCM ()
- getInputFile :: TCM AbsolutePath
- getInputFile' :: TCM (Maybe AbsolutePath)
- hasInputFile :: TCM Bool
- isPropEnabled :: HasOptions m => m Bool
- hasUniversePolymorphism :: HasOptions m => m Bool
- enableCaching :: TCM Bool
- showImplicitArguments :: TCM Bool
- showIrrelevantArguments :: TCM Bool
- withShowAllArguments :: TCM a -> TCM a
- withShowAllArguments' :: Bool -> TCM a -> TCM a
- withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- ignoreAllInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: HasOptions m => m Bool
- etaEnabled :: TCM Bool
- maxInstanceSearchDepth :: TCM Int
- maxInversionDepth :: TCM Int
- getVerbosity :: HasOptions m => m (Trie String Int)
- type VerboseKey = String
- parseVerboseKey :: VerboseKey -> [String]
- hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
- hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
- whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
- verboseS :: (MonadTCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m ()
- verbosity :: VerboseKey -> Lens' Int TCState

# Documentation

setPragmaOptions :: PragmaOptions -> TCM () Source #

Sets the pragma options.

setCommandLineOptions :: CommandLineOptions -> TCM () Source #

Sets the command line options (both persistent and pragma options are updated).

Relative include directories are made absolute with respect to the current working directory. If the include directories have changed (thus, they are `Left` now, and were previously ``Right` something`), then the state is reset (completely, see setIncludeDirs) .

An empty list of relative include directories (``Left` []`) is interpreted as `["."]`.

setCommandLineOptions' Source #

Arguments

:: AbsolutePath | The base directory of relative paths.
-> CommandLineOptions |
-> TCM () |

libToTCM :: LibM a -> TCM a Source #

setLibraryPaths Source #

Arguments

:: AbsolutePath | The base directory of relative paths.
-> CommandLineOptions |
-> TCM CommandLineOptions |

setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions Source #

addDefaultLibraries Source #

Arguments

:: AbsolutePath | The base directory of relative paths.
-> CommandLineOptions |
-> TCM CommandLineOptions |

setOptionsFromPragma :: OptionsPragma -> TCM () Source #

enableDisplayForms :: TCM a -> TCM a Source #

Disable display forms.

disableDisplayForms :: TCM a -> TCM a Source #

Disable display forms.

displayFormsEnabled :: TCM Bool Source #

Check if display forms are enabled.

getIncludeDirs :: TCM [AbsolutePath] Source #

Gets the include directories.

Precondition: `optAbsoluteIncludePaths` must be nonempty (i.e. `setCommandLineOptions` must have run).

setIncludeDirs Source #

Arguments

:: [FilePath] | New include directories.
-> AbsolutePath | The base directory of relative paths.
-> TCM () |

Makes the given directories absolute and stores them as include directories.

If the include directories change, then the state is reset (completely, except for the include directories and `stInteractionOutputCallback`).

An empty list is interpreted as `["."]`.

setInputFile :: FilePath -> TCM () Source #

getInputFile :: TCM AbsolutePath Source #

Should only be run if `hasInputFile`.

getInputFile' :: TCM (Maybe AbsolutePath) Source #

Return the `optInputFile` as `AbsolutePath`, if any.

hasInputFile :: TCM Bool Source #

isPropEnabled :: HasOptions m => m Bool Source #

hasUniversePolymorphism :: HasOptions m => m Bool Source #

enableCaching :: TCM Bool Source #

showImplicitArguments :: TCM Bool Source #

showIrrelevantArguments :: TCM Bool Source #

withShowAllArguments :: TCM a -> TCM a Source #

Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.

Restores all `PragmaOptions` after completion. Thus, do not attempt to make persistent `PragmaOptions` changes in a `withShowAllArguments` bracket.

withShowAllArguments' :: Bool -> TCM a -> TCM a Source #

withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM a -> TCM a Source #

Change `PragmaOptions` for a computation and restore afterwards.

ignoreInterfaces :: TCM Bool Source #

ignoreAllInterfaces :: TCM Bool Source #

positivityCheckEnabled :: TCM Bool Source #

typeInType :: HasOptions m => m Bool Source #

etaEnabled :: TCM Bool Source #

maxInstanceSearchDepth :: TCM Int Source #

maxInversionDepth :: TCM Int Source #

getVerbosity :: HasOptions m => m (Trie String Int) Source #

Retrieve the current verbosity level.

type VerboseKey = String Source #

parseVerboseKey :: VerboseKey -> [String] Source #

hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool Source #

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool Source #

Check whether a certain verbosity level is activated (exact match).

whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm () Source #

Run a computation if a certain verbosity level is activated (exact match).

verboseS :: (MonadTCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m () Source #

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

verbosity :: VerboseKey -> Lens' Int TCState Source #

Verbosity lens.