Agda.TypeChecking.Monad.Options

Documentation

setPragmaOptions :: MonadTCM tcm => PragmaOptions -> tcm ()

Sets the pragma options.

setCommandLineOptions :: MonadTCM tcm => 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.

An empty list of relative include directories (Left []) is interpreted as [.].

pragmaOptions :: MonadTCM tcm => tcm PragmaOptions

Returns the pragma options which are currently in effect.

commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions

Returns the command line options which are currently in effect.

setOptionsFromPragma :: MonadTCM tcm => OptionsPragma -> tcm ()

enableDisplayForms :: MonadTCM tcm => tcm a -> tcm a

Disable display forms.

disableDisplayForms :: MonadTCM tcm => tcm a -> tcm a

Disable display forms.

displayFormsEnabled :: MonadTCM tcm => tcm Bool

Check if display forms are enabled.

dontEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a

Don't eta contract implicit

doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a

Do eta contract implicit

shouldEtaContractImplicit :: MonadTCM tcm => tcm Bool

dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm a

Don't reify interaction points

shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool

getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]

Gets the include directories.

Precondition: optIncludeDirs must be Right something.

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.

setIncludeDirs

Arguments

:: MonadTCM tcm

=> [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 have changed, then the state is reset.

An empty list is interpreted as [.].

setInputFile :: MonadTCM tcm => FilePath -> tcm ()

getInputFile :: MonadTCM tcm => tcm AbsolutePath

Should only be run if hasInputFile.

hasInputFile :: MonadTCM tcm => tcm Bool

proofIrrelevance :: MonadTCM tcm => tcm Bool

hasUniversePolymorphism :: MonadTCM tcm => tcm Bool

showImplicitArguments :: MonadTCM tcm => tcm Bool

setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm a

ignoreInterfaces :: MonadTCM tcm => tcm Bool

positivityCheckEnabled :: MonadTCM tcm => tcm Bool

typeInType :: MonadTCM tcm => tcm Bool

getVerbosity :: MonadTCM tcm => tcm (Trie String Int)

type VerboseKey = String

hasVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm Bool

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

Precondition: The level must be non-negative.

reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()

reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()

reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()

verboseBracket :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm a -> tcm a