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 (and were previously Right something), then the state is reset (completely) .

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

pragmaOptions :: TCM PragmaOptions

Returns the pragma options which are currently in effect.

commandLineOptions :: TCM CommandLineOptions

Returns the command line options which are currently in effect.

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.

dontEtaContractImplicit :: TCM a -> TCM a

Don't eta contract implicit

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

Do eta contract implicit

shouldEtaContractImplicit :: TCM Bool

dontReifyInteractionPoints :: TCM a -> TCM a

Don't reify interaction points

shouldReifyInteractionPoints :: TCM Bool

getIncludeDirs :: 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

:: [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 (and they were previously Right something), 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.

hasInputFile :: TCM Bool

proofIrrelevance :: TCM Bool

hasUniversePolymorphism :: 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.

ignoreInterfaces :: TCM Bool

positivityCheckEnabled :: TCM Bool

typeInType :: TCM Bool

getVerbosity :: TCM (Trie String Int)

type VerboseKey = String

hasVerbosity :: VerboseKey -> Int -> TCM Bool

emacsifyDebugMessage

Arguments

:: String

The debug message.

-> TCM String

If this command is run under the Emacs mode, then it formats the debug message in such a way that the Emacs mode can understand it.

displayDebugMessage :: String -> TCM ()

Displays a debug message in a suitable way.

verboseS :: VerboseKey -> Int -> TCM () -> TCM ()

Precondition: The level must be non-negative.

reportS :: VerboseKey -> Int -> String -> TCM ()

reportSLn :: VerboseKey -> Int -> String -> TCM ()

reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM ()

verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM a