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 :: AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
getLibraryOptions :: AbsolutePath -> TopLevelModuleName -> 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. Checks for unsafe combinations.

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 then the state is reset (partly, 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 Source #

Arguments

:: AbsolutePath	The file name.
-> TopLevelModuleName	The top-level module name.
-> TCM [AgdaLibFile]

Returns the library files for a given file.

getLibraryOptions Source #

Arguments

:: AbsolutePath	The file name.
-> TopLevelModuleName	The top-level module name.
-> TCM [OptionsPragma]

Returns the library options for a given file.

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.