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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Options

Synopsis

- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
- libToTCM :: LibM a -> TCM a
- getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile]
- getLibraryOptions :: FilePath -> TCM [OptionsPragma]
- setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
- addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- addTrustedExecutables :: CommandLineOptions -> TCM CommandLineOptions
- setOptionsFromPragma :: OptionsPragma -> TCM ()
- enableDisplayForms :: MonadTCEnv m => m a -> m a
- disableDisplayForms :: MonadTCEnv m => m a -> m a
- displayFormsEnabled :: MonadTCEnv m => m Bool
- getIncludeDirs :: HasOptions m => m [AbsolutePath]
- setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
- isPropEnabled :: HasOptions m => m Bool
- isTwoLevelEnabled :: HasOptions m => m Bool
- hasUniversePolymorphism :: HasOptions m => m Bool
- showImplicitArguments :: HasOptions m => m Bool
- showIrrelevantArguments :: HasOptions m => m Bool
- showIdentitySubstitutions :: HasOptions m => m Bool
- withShowAllArguments :: ReadTCState m => m a -> m a
- withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
- withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
- positivityCheckEnabled :: HasOptions m => m Bool
- typeInType :: HasOptions m => m Bool
- etaEnabled :: HasOptions m => m Bool
- maxInstanceSearchDepth :: HasOptions m => m Int
- maxInversionDepth :: HasOptions m => m Int
- getLanguage :: HasOptions m => m Language

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

getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile] Source #

getLibraryOptions :: FilePath -> TCM [OptionsPragma] 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 |

addTrustedExecutables :: CommandLineOptions -> TCM CommandLineOptions Source #

setOptionsFromPragma :: OptionsPragma -> TCM () Source #

enableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

disableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

displayFormsEnabled :: MonadTCEnv m => m Bool Source #

Check if display forms are enabled.

getIncludeDirs :: HasOptions m => m [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 some other things).

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

isPropEnabled :: HasOptions m => m Bool Source #

isTwoLevelEnabled :: HasOptions m => m Bool Source #

hasUniversePolymorphism :: HasOptions m => m Bool Source #

showImplicitArguments :: HasOptions m => m Bool Source #

showIrrelevantArguments :: HasOptions m => m Bool Source #

showIdentitySubstitutions :: HasOptions m => m Bool Source #

withShowAllArguments :: ReadTCState m => m a -> m 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' :: ReadTCState m => Bool -> m a -> m a Source #

withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a Source #

Change `PragmaOptions` for a computation and restore afterwards.

positivityCheckEnabled :: HasOptions m => m Bool Source #

typeInType :: HasOptions m => m Bool Source #

etaEnabled :: HasOptions m => m Bool Source #

maxInstanceSearchDepth :: HasOptions m => m Int Source #

maxInversionDepth :: HasOptions m => m Int Source #

getLanguage :: HasOptions m => m Language Source #

Returns the `Language` currently in effect.