Agda-2.4.2.5: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Options

Synopsis

Documentation

setPragmaOptions :: PragmaOptions -> TCM () Source

Sets the pragma options.

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 (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 ["."].

class (Functor m, Applicative m, Monad m) => HasOptions m where Source

Methods

pragmaOptions :: m PragmaOptions Source

Returns the pragma options which are currently in effect.

commandLineOptions :: m CommandLineOptions Source

Returns the command line options which are currently in effect.

enableDisplayForms :: TCM a -> TCM a Source

Disable display forms.

disableDisplayForms :: TCM a -> TCM a Source

Disable display forms.

displayFormsEnabled :: TCM Bool Source

Check if display forms are enabled.

dontEtaContractImplicit :: TCM a -> TCM a Source

Don't eta contract implicit

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

Do eta contract implicit

dontReifyInteractionPoints :: TCM a -> TCM a Source

Don't reify interaction points

getIncludeDirs :: TCM [AbsolutePath] Source

Gets the include directories.

Precondition: optIncludeDirs must be Right something.

data RelativeTo Source

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 Source

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 ["."].

withShowAllArguments :: TCM a -> TCM a Source

Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.

getVerbosity :: HasOptions m => m (Trie String Int) Source

Retrieve the current verbosity level.

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

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

displayDebugMessage Source

Arguments

:: MonadTCM tcm 
=> Int

The message's debug level.

-> String

Message.

-> tcm () 

Displays a debug message in a suitable way.

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

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

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

Conditionally print debug string.

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

Conditionally println debug string.

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

Conditionally render debug Doc and print it.

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

Print brackets around debug messages issued by a computation.