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.
hasUniversePolymorphism :: HasOptions m => m Bool Source
sharedFun :: HasOptions m => m (Term -> Term) Source
shared :: HasOptions m => Term -> m Term Source
sharedType :: HasOptions m => Type -> m Type 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.