Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Monad.Options
Synopsis
setPragmaOptions :: MonadTCM tcm => PragmaOptions -> tcm ()
setCommandLineOptions :: MonadTCM tcm => CommandLineOptions -> tcm ()
pragmaOptions :: MonadTCM tcm => tcm PragmaOptions
commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions
setOptionsFromPragma :: MonadTCM tcm => OptionsPragma -> tcm ()
enableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
disableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
displayFormsEnabled :: MonadTCM tcm => tcm Bool
dontEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
shouldEtaContractImplicit :: MonadTCM tcm => tcm Bool
dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm a
shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool
getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]
data RelativeTo
= ProjectRoot AbsolutePath
| CurrentDir
setIncludeDirs :: MonadTCM tcm => [FilePath] -> RelativeTo -> tcm ()
setInputFile :: MonadTCM tcm => FilePath -> tcm ()
getInputFile :: MonadTCM tcm => tcm AbsolutePath
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 ()
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
Documentation
setPragmaOptions :: MonadTCM tcm => PragmaOptions -> tcm ()Source
Sets the pragma options.
setCommandLineOptions :: MonadTCM tcm => 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, then the state is reset.

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

pragmaOptions :: MonadTCM tcm => tcm PragmaOptionsSource
Returns the pragma options which are currently in effect.
commandLineOptions :: MonadTCM tcm => tcm CommandLineOptionsSource
Returns the command line options which are currently in effect.
setOptionsFromPragma :: MonadTCM tcm => OptionsPragma -> tcm ()Source
enableDisplayForms :: MonadTCM tcm => tcm a -> tcm aSource
Disable display forms.
disableDisplayForms :: MonadTCM tcm => tcm a -> tcm aSource
Disable display forms.
displayFormsEnabled :: MonadTCM tcm => tcm BoolSource
Check if display forms are enabled.
dontEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm aSource
Don't eta contract implicit
doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm aSource
Do eta contract implicit
shouldEtaContractImplicit :: MonadTCM tcm => tcm BoolSource
dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm aSource
Don't reify interaction points
shouldReifyInteractionPoints :: MonadTCM tcm => tcm BoolSource
getIncludeDirs :: MonadTCM tcm => 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 AbsolutePathThe root directory of the "project" containing the given file. The file needs to be syntactically correct, with a module name matching the file name.
CurrentDirThe current working directory.
setIncludeDirsSource
:: MonadTCM tcm
=> [FilePath]New include directories.
-> RelativeToHow 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 ()Source
getInputFile :: MonadTCM tcm => tcm AbsolutePathSource
Should only be run if hasInputFile.
hasInputFile :: MonadTCM tcm => tcm BoolSource
proofIrrelevance :: MonadTCM tcm => tcm BoolSource
hasUniversePolymorphism :: MonadTCM tcm => tcm BoolSource
showImplicitArguments :: MonadTCM tcm => tcm BoolSource
setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm aSource
ignoreInterfaces :: MonadTCM tcm => tcm BoolSource
positivityCheckEnabled :: MonadTCM tcm => tcm BoolSource
typeInType :: MonadTCM tcm => tcm BoolSource
getVerbosity :: MonadTCM tcm => tcm (Trie String Int)Source
type VerboseKey = StringSource
hasVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm BoolSource
verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()Source
Precondition: The level must be non-negative.
reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()Source
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()Source
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()Source
verboseBracket :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm a -> tcm aSource
Produced by Haddock version 2.6.1