Agda.TypeChecking.Monad.Options
- 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
- 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 ()
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 (
) is
interpreted as Left
[][.]
.
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. |
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.
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()
verboseBracket :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm a -> tcm a