| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Trace
Contents
Synopsis
- interestingCall :: Call -> Bool
- traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a
- traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b
- traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a
- traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a
- getCurrentRange :: MonadTCEnv m => m Range
- setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a
Trace
interestingCall :: Call -> Bool Source #
traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a Source #
traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b Source #
Reset envCall to previous value in the continuation.
Caveat: if the last traceCall did not set an interestingCall,
for example, only set the Range' with Call,
we will revert to the last interesting call.
traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a Source #
Record a function call in the trace.
traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a Source #
getCurrentRange :: MonadTCEnv m => m Range Source #
setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a Source #
Sets the current range (for error messages etc.) to the range
of the given object, if it has a range (i.e., its range is not noRange).