Safe Haskell | None |
---|---|
Language | Haskell98 |
- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- setCommandLineOptions' :: RelativeTo -> CommandLineOptions -> TCM ()
- libToTCM :: LibM a -> TCM a
- setLibraryPaths :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions
- setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
- addDefaultLibraries :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions
- class (Functor m, Applicative m, Monad m) => HasOptions m where
- 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 :: MonadReader TCEnv m => m Bool
- dontReifyInteractionPoints :: TCM a -> TCM a
- shouldReifyInteractionPoints :: TCM Bool
- getIncludeDirs :: TCM [AbsolutePath]
- data RelativeTo
- getProjectRoot :: RelativeTo -> TCM AbsolutePath
- setIncludeDirs :: [FilePath] -> RelativeTo -> TCM ()
- setInputFile :: FilePath -> TCM ()
- getInputFile :: TCM AbsolutePath
- getInputFile' :: TCM (Maybe AbsolutePath)
- hasInputFile :: TCM Bool
- proofIrrelevance :: TCM Bool
- hasUniversePolymorphism :: HasOptions m => m Bool
- sharedFun :: HasOptions m => m (Term -> Term)
- shared :: HasOptions m => Term -> m Term
- sharedType :: HasOptions m => Type -> m Type
- enableCaching :: TCM Bool
- showImplicitArguments :: TCM Bool
- showIrrelevantArguments :: TCM Bool
- withShowAllArguments :: TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: HasOptions m => m Bool
- etaEnabled :: TCM Bool
- getVerbosity :: HasOptions m => m (Trie String Int)
- type VerboseKey = String
- hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
- displayDebugMessage :: MonadTCM tcm => Int -> String -> tcm ()
- 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 :: 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' :: RelativeTo -> CommandLineOptions -> TCM () Source #
class (Functor m, Applicative m, Monad m) => HasOptions m where Source #
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.
HasOptions NLM Source # | |
MonadIO m => HasOptions (TCMT m) Source # | |
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.
dontEtaContractImplicit :: TCM a -> TCM a Source #
Don't eta contract implicit
doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a Source #
Do eta contract implicit
shouldEtaContractImplicit :: MonadReader TCEnv m => m Bool Source #
dontReifyInteractionPoints :: TCM a -> TCM a Source #
Don't reify interaction points
getIncludeDirs :: TCM [AbsolutePath] Source #
Gets the include directories.
Precondition: optAbsoluteIncludePaths
must be nonempty (i.e.
setCommandLineOptions
must have run).
data RelativeTo Source #
Which directory should form the base of relative include paths?
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. |
:: [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, 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 #
hasUniversePolymorphism :: HasOptions m => m Bool Source #
sharedType :: HasOptions m => Type -> m Type 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.
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 #
hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool Source #
Check whether a certain verbosity level is activated.
Precondition: The level must be non-negative.
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.