Agda.TypeChecking.Monad.Options

Documentation

setPragmaOptions :: PragmaOptions -> TCM ()

Sets the pragma options.

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 (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' :: RelativeTo -> CommandLineOptions -> TCM ()

libToTCM :: LibM a -> TCM a

setLibraryPaths :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions

setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions

addDefaultLibraries :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions

setOptionsFromPragma :: OptionsPragma -> TCM ()

enableDisplayForms :: TCM a -> TCM a

Disable display forms.

disableDisplayForms :: TCM a -> TCM a

Disable display forms.

displayFormsEnabled :: TCM Bool

Check if display forms are enabled.

getIncludeDirs :: TCM [AbsolutePath]

Gets the include directories.

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

data RelativeTo

Which directory should form the base of relative include paths?

Constructors

ProjectRoot AbsolutePath

The root directory of the "project" containing the given file. The file needs to be syntactically correct, with a module name matching the file name.

CurrentDir

The current working directory.

getProjectRoot :: RelativeTo -> TCM AbsolutePath

setIncludeDirs

Arguments

:: [FilePath]

New include directories.

-> RelativeTo

How should relative paths be interpreted?

-> 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 ()

getInputFile :: TCM AbsolutePath

Should only be run if hasInputFile.

getInputFile' :: TCM (Maybe AbsolutePath)

Return the optInputFile as AbsolutePath, if any.

hasInputFile :: TCM Bool

proofIrrelevance :: TCM Bool

hasUniversePolymorphism :: HasOptions m => m Bool

enableCaching :: TCM Bool

showImplicitArguments :: TCM Bool

showIrrelevantArguments :: TCM Bool

withShowAllArguments :: TCM a -> TCM 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' :: Bool -> TCM a -> TCM a

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

Change PragmaOptions for a computation and restore afterwards.

ignoreInterfaces :: 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)

Retrieve the current verbosity level.

type VerboseKey = String

parseVerboseKey :: VerboseKey -> [String]

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

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

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

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

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

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

verboseS :: (MonadReader TCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m ()

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

verbosity :: VerboseKey -> Lens' Int TCState

Verbosity lens.