| 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
An empty list of relative include directories (Left []["."].
setCommandLineOptions' Source #
Arguments
| :: AbsolutePath | The base directory of relative paths. |
| -> CommandLineOptions | |
| -> TCM () |
getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile] Source #
getLibraryOptions :: FilePath -> TCM [OptionsPragma] Source #
Arguments
| :: AbsolutePath | The base directory of relative paths. |
| -> CommandLineOptions | |
| -> TCM CommandLineOptions |
Arguments
| :: AbsolutePath | The base directory of relative paths. |
| -> CommandLineOptions | |
| -> TCM CommandLineOptions |
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).
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 ["."].
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.