Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Options
- 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
- 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
- withShowAllArguments' :: Bool -> TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: HasOptions m => m Bool
- etaEnabled :: TCM Bool
- maxInstanceSearchDepth :: TCM Int
- 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 () #
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
(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 () #
class (Functor m, Applicative m, Monad m) => HasOptions m where #
Minimal complete definition
Methods
pragmaOptions :: m PragmaOptions #
Returns the pragma options which are currently in effect.
commandLineOptions :: m CommandLineOptions #
Returns the command line options which are currently in effect.
Instances
HasOptions NLM # | |
MonadIO m => HasOptions (TCMT m) # | |
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.
getIncludeDirs :: TCM [AbsolutePath] #
Gets the include directories.
Precondition: optAbsoluteIncludePaths
must be nonempty (i.e.
setCommandLineOptions
must have run).
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. |
getProjectRoot :: RelativeTo -> TCM AbsolutePath #
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, then the state is reset (completely,
except for the include directories and stInteractionOutputCallback
).
An empty list is interpreted as ["."]
.
setInputFile :: FilePath -> TCM () #
getInputFile :: TCM AbsolutePath #
Should only be run if hasInputFile
.
getInputFile' :: TCM (Maybe AbsolutePath) #
Return the optInputFile
as AbsolutePath
, if any.
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 #
withShowAllArguments :: TCM a -> TCM a #
Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.
withShowAllArguments' :: Bool -> TCM a -> TCM a #
ignoreInterfaces :: TCM Bool #
typeInType :: HasOptions m => m Bool #
etaEnabled :: TCM Bool #
getVerbosity :: HasOptions m => m (Trie String Int) #
Retrieve the current verbosity level.
type VerboseKey = String #
hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool #
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 () #
Run a computation if a certain verbosity level is activated.
Precondition: The level must be non-negative.
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm () #
Conditionally println debug string.
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> TCM Doc -> tcm () #
Conditionally render debug Doc
and print it.
verboseBracket :: MonadTCM tcm => VerboseKey -> Int -> String -> TCM a -> tcm a #
Print brackets around debug messages issued by a computation.