Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
- libToTCM :: LibM a -> TCM a
- setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
- addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
- setOptionsFromPragma :: OptionsPragma -> TCM ()
- enableDisplayForms :: TCM a -> TCM a
- disableDisplayForms :: TCM a -> TCM a
- displayFormsEnabled :: TCM Bool
- getIncludeDirs :: TCM [AbsolutePath]
- setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
- setInputFile :: FilePath -> TCM ()
- getInputFile :: TCM AbsolutePath
- getInputFile' :: TCM (Maybe AbsolutePath)
- hasInputFile :: TCM Bool
- isPropEnabled :: HasOptions m => m Bool
- hasUniversePolymorphism :: HasOptions m => m Bool
- enableCaching :: TCM Bool
- showImplicitArguments :: TCM Bool
- showIrrelevantArguments :: TCM Bool
- withShowAllArguments :: TCM a -> TCM a
- withShowAllArguments' :: Bool -> TCM a -> TCM a
- withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- ignoreAllInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: HasOptions m => m Bool
- etaEnabled :: TCM Bool
- maxInstanceSearchDepth :: TCM Int
- maxInversionDepth :: TCM Int
- getVerbosity :: HasOptions m => m (Trie String Int)
- type VerboseKey = String
- parseVerboseKey :: VerboseKey -> [String]
- hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
- hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
- whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
- verboseS :: (MonadTCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m ()
- verbosity :: VerboseKey -> Lens' Int TCState
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
),
then the state is reset (completely, see setIncludeDirs) .Right
something
An empty list of relative include directories (
) is
interpreted as Left
[]["."]
.
setCommandLineOptions' Source #
:: AbsolutePath | The base directory of relative paths. |
-> CommandLineOptions | |
-> TCM () |
:: AbsolutePath | The base directory of relative paths. |
-> CommandLineOptions | |
-> TCM CommandLineOptions |
:: AbsolutePath | The base directory of relative paths. |
-> CommandLineOptions | |
-> TCM CommandLineOptions |
setOptionsFromPragma :: OptionsPragma -> TCM () Source #
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.
getIncludeDirs :: TCM [AbsolutePath] Source #
Gets the include directories.
Precondition: optAbsoluteIncludePaths
must be nonempty (i.e.
setCommandLineOptions
must have run).
:: [FilePath] | New include directories. |
-> AbsolutePath | The base directory of relative paths. |
-> TCM () |
Makes the given directories absolute and stores them as include directories.
If the include directories change, then the state is reset (completely,
except for the include directories and stInteractionOutputCallback
).
An empty list is interpreted as ["."]
.
setInputFile :: FilePath -> TCM () Source #
getInputFile :: TCM AbsolutePath Source #
Should only be run if hasInputFile
.
getInputFile' :: TCM (Maybe AbsolutePath) Source #
Return the optInputFile
as AbsolutePath
, if any.
hasInputFile :: TCM Bool Source #
isPropEnabled :: HasOptions m => m Bool Source #
hasUniversePolymorphism :: HasOptions m => m Bool Source #
enableCaching :: TCM Bool Source #
withShowAllArguments :: TCM a -> TCM a Source #
Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.
Restores all PragmaOptions
after completion.
Thus, do not attempt to make persistent PragmaOptions
changes in a withShowAllArguments
bracket.
withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM a -> TCM a Source #
Change PragmaOptions
for a computation and restore afterwards.
typeInType :: HasOptions m => m Bool Source #
etaEnabled :: TCM Bool Source #
getVerbosity :: HasOptions m => m (Trie String Int) Source #
Retrieve the current verbosity level.
type VerboseKey = String Source #
parseVerboseKey :: VerboseKey -> [String] Source #
hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool Source #
Check whether a certain verbosity level is activated.
Precondition: The level must be non-negative.
hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool Source #
Check whether a certain verbosity level is activated (exact match).
whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm () Source #
Run a computation if a certain verbosity level is activated (exact match).
verboseS :: (MonadTCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m () Source #
Run a computation if a certain verbosity level is activated.
Precondition: The level must be non-negative.