Agda.TypeChecking.Monad.Options

Documentation

setPragmaOptions :: PragmaOptions -> TCM ()

Sets the pragma options. Checks for unsafe combinations.

setCommandLineOptions :: CommandLineOptions -> TCM ()

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'

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions

-> TCM ()

libToTCM :: LibM a -> TCM a

getAgdaLibFiles

Arguments

:: AbsolutePath

The file name.

-> TopLevelModuleName

The top-level module name.

-> TCM [AgdaLibFile]

Returns the library files for a given file.

Nothing is returned if optUseLibs is False.

An error is raised if optUseLibs is True and a library file is located too far down the directory hierarchy (see checkLibraryFileNotTooFarDown).

getAgdaLibFilesWithoutTopLevelModuleName

Arguments

:: AbsolutePath

The file.

-> TCM [AgdaLibFile]

Returns potential library files for a file without a known top-level module name.

Once the top-level module name is known one can use checkLibraryFileNotTooFarDown to check that the potential library files were not located too far down the directory hierarchy.

Nothing is returned if optUseLibs is False.

checkLibraryFileNotTooFarDown :: TopLevelModuleName -> AgdaLibFile -> TCM ()

Checks that a library file for the module A.B.C (say) in the directory dirAB is located at least two directories above the file (not in dir/A or dirAB).

getLibraryOptions

Arguments

:: AbsolutePath

The file name.

-> TopLevelModuleName

The top-level module name.

-> TCM [OptionsPragma]

Returns the library options for a given file.

setLibraryPaths

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions

-> TCM CommandLineOptions

setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions

addDefaultLibraries

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions

-> TCM CommandLineOptions

addTrustedExecutables :: CommandLineOptions -> TCM CommandLineOptions

setOptionsFromPragma :: OptionsPragma -> TCM ()

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

Disable display forms.

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

Disable display forms.

displayFormsEnabled :: MonadTCEnv m => m Bool

Check if display forms are enabled.

getIncludeDirs :: HasOptions m => m [AbsolutePath]

Gets the include directories.

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

setIncludeDirs

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

isLevelUniverseEnabled :: HasOptions m => m Bool

isTwoLevelEnabled :: HasOptions m => m Bool

hasUniversePolymorphism :: HasOptions m => m Bool

showImplicitArguments :: HasOptions m => m Bool

showGeneralizedArguments :: HasOptions m => m Bool

showIrrelevantArguments :: HasOptions m => m Bool

showIdentitySubstitutions :: HasOptions m => m Bool

withShowAllArguments :: ReadTCState m => m a -> m a

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

withoutPrintingGeneralization :: ReadTCState m => m a -> m a

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

Change PragmaOptions for a computation and restore afterwards.

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

Returns the Language currently in effect.