Safe Haskell | None |
---|
Agda.TypeChecking.Monad.Options
- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- pragmaOptions :: TCM PragmaOptions
- commandLineOptions :: TCM CommandLineOptions
- setOptionsFromPragma :: OptionsPragma -> TCM ()
- enableDisplayForms :: TCM a -> TCM a
- disableDisplayForms :: TCM a -> TCM a
- displayFormsEnabled :: TCM Bool
- dontEtaContractImplicit :: TCM a -> TCM a
- doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
- shouldEtaContractImplicit :: TCM Bool
- dontReifyInteractionPoints :: TCM a -> TCM a
- shouldReifyInteractionPoints :: TCM Bool
- getIncludeDirs :: TCM [AbsolutePath]
- data RelativeTo
- setIncludeDirs :: [FilePath] -> RelativeTo -> TCM ()
- setInputFile :: FilePath -> TCM ()
- getInputFile :: TCM AbsolutePath
- hasInputFile :: TCM Bool
- proofIrrelevance :: TCM Bool
- hasUniversePolymorphism :: TCM Bool
- showImplicitArguments :: TCM Bool
- showIrrelevantArguments :: TCM Bool
- withShowAllArguments :: TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: TCM Bool
- getVerbosity :: TCM (Trie String Int)
- type VerboseKey = String
- hasVerbosity :: VerboseKey -> Int -> TCM Bool
- emacsifyDebugMessage :: String -> TCM String
- displayDebugMessage :: String -> TCM ()
- verboseS :: VerboseKey -> Int -> TCM () -> TCM ()
- reportS :: VerboseKey -> Int -> String -> TCM ()
- reportSLn :: VerboseKey -> Int -> String -> TCM ()
- reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM ()
- verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM a
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
), then the state is reset
(completely) .
Right
something
An empty list of relative include directories (
) is
interpreted as Left
[][.]
.
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
dontReifyInteractionPoints :: TCM a -> TCM a
Don't reify interaction points
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. |
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
), then the state is reset (completely, except
for the include directories and Right
somethingstInteractionOutputCallback
).
An empty list is interpreted as [.]
.
setInputFile :: FilePath -> TCM ()
getInputFile :: TCM AbsolutePath
Should only be run if hasInputFile
.
hasInputFile :: TCM Bool
withShowAllArguments :: TCM a -> TCM a
Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.
typeInType :: TCM Bool
getVerbosity :: TCM (Trie String Int)
type VerboseKey = String
hasVerbosity :: VerboseKey -> Int -> TCM Bool
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